caa a22 4500 463182758 CHVBK 20180406164844.0 cr unu---uuuuu 170326e20070401xx s 000 0 eng 10.1007/s10817-006-9045-y doi (NATIONALLICENCE)springer-10.1007/s10817-006-9045-y A Sound Framework for δ-Rule Variants in Free-Variable Semantic Tableaux [Elektronische Daten] [Domenico Cantone, Marianna Nicolosi-Asmundo] We propose a generic sound δ-rule, based on a quite general method for the construction of Skolem terms, which can be used as a common framework for proving the soundness of known variants of the δ-rule, and we compare their relative effectiveness. Attempts to instantiate some of the δ-rules present in the literature within our framework allowed us to pinpoint unsoundness problems for two of them. In both cases, we propose revised versions that are proved sound by reducing them within our framework. Springer Science+Business Media, Inc., 2006 free-variable semantic tableaux nationallicence δ-rule nationallicence Skolemization nationallicence Cantone Domenico Dipartimento di Matematica e Informatica, Università di Catania, Viale A. Doria 6, I-95125, Catania, Italy aut Nicolosi-Asmundo Marianna Dipartimento di Matematica e Informatica, Università di Catania, Viale A. Doria 6, I-95125, Catania, Italy aut Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 31-56 0168-7433 38:1-3<31 2007 38 10817 https://doi.org/10.1007/s10817-006-9045-y text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-006-9045-y text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Cantone Domenico Dipartimento di Matematica e Informatica, Università di Catania, Viale A. Doria 6, I-95125, Catania, Italy aut NATIONALLICENCE 700 1- Nicolosi-Asmundo Marianna Dipartimento di Matematica e Informatica, Università di Catania, Viale A. Doria 6, I-95125, Catania, Italy aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 31-56 0168-7433 38:1-3<31 2007 38 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer