Database and Artificial Intelligence applications are briefly discussed and it is argued that they need deduction methods that are not only refutation complete but also complete for finite satisfiability. A novel deduction method is introduced for such applications. Instead of relying on Skolemization, as most refutation methods do, the proposed method processes existential quantifiers in a special manner which makes it complete not only for refutation, but also for finite satisfiability. A main contribution of this paper is the proof of these results.
CITATION STYLE
Bry, F., & Torge, S. (1998). A deduction method complete for refutation and finite satisfiability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1489, pp. 122–138). Springer Verlag. https://doi.org/10.1007/3-540-49545-2_9
Mendeley helps you to discover research relevant for your work.