We propose a generic sound delta-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 delta-rule, and we compare their relative effectiveness. Attempts to instantiate some of the delta-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.
|Titolo:||A Sound Framework for delta-rule Variants in Free Variable Semantic Tableaux|
|Data di pubblicazione:||2007|
|Citazione:||A Sound Framework for delta-rule Variants in Free Variable Semantic Tableaux / CANTONE D; NICOLOSI ASMUNDO M. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - 38:1-3(2007), pp. 31-56.|
|Appare nelle tipologie:||1.1 Articolo in rivista|