AbstractThis paper describes a decision procedure for disjunctions of conjunctions of anti-prenex normal forms of pure first-order logic (FOLDNFs) that do not contain V within the scope of quantifiers. The disjuncts of these FOLDNFs are equivalent to prenex normal forms whose quantifier-free parts are conjunctions of atomic and negated atomic formulae (= Herbrand formulae). In contrast to the usual algorithms for Herbrand formulae, neither skolemization nor unification algorithms with function symbols are applied. Instead, a procedure is described that rests on nothing but equivalence transformations within pure first-order logic (FOL). This procedure involves the application of a calculus for negative normal forms (the NNF-calculus) with A -||- A & A (= &I) as the sole rule that increases the complexity of given FOLDNFs. The described algorithm illustrates how, in the case of Herbrand formulae, decision problems can be solved through a systematic search for proofs that reduce the number of applications of the rule &I to a minimum in the NNF-calculus. In the case of Herbrand formulae, it is even possible to entirely abstain from applying &I. Finally, it is shown how the described procedure can be used within an optimized general search for proofs of contradiction and what kind of questions arise for a &I-minimal proof strategy in the case of a general search for proofs of contradiction.
Similar books and articles
Finite and Rational Tree Constraints.Torbjorn Keisu - 1994 - Logic Journal of the IGPL 2 (2):167-204.
Herbrand E a silogística ampliada.Frank Thomas Sautter - 2015 - Philósophos - Revista de Filosofia 20 (1):125-144.
The Epsilon Calculus and Herbrand Complexity.Georg Moser & Richard Zach - 2006 - Studia Logica 82 (1):133-155.
Describing Proofs by Short Tautologies.Stefan Hetzl - 2009 - Annals of Pure and Applied Logic 159 (1-2):129-145.
Herbrand Style Proof Procedures for Modal Logic.Marta Cialdea - 1993 - Journal of Applied Non-Classical Logics 3 (2):205-223.
On Theorems of Gödel and Kreisel: Completeness and Markov's Principle.D. C. McCarty - 1994 - Notre Dame Journal of Formal Logic 35 (1):99-107.
Analog of Herbrand's Theorem for Prenex Formulas of Constructive Predicate Calculus.G. E. Mints - 1969 - Journal of Symbolic Logic 36 (3):47--51.
Remarks on Herbrand Normal Forms and Herbrand Realizations.Ulrich Kohlenbach - 1992 - Archive for Mathematical Logic 31 (5):305-317.
On Different Proof-Search Strategies for Orthologic.Uwe Egly & Hans Tompits - 2003 - Studia Logica 73 (1):131 - 152.
On Different Proof-Search Strategies for Orthologic.Uwe Egly & Hans Tompits - 2003 - Studia Logica 73 (1):131-152.
Analog of Herbrand's Theorem for [Non] Prenex Formulas of Constructive Predicate Calculus.G. E. Mints & A. O. Slisenko - 1971 - Journal of Symbolic Logic 36 (3):525-526.
Analog of Herbrand's Theorem for [Non] Prenex Formulas of Constructive Predicate Calculus.J. van Heijenoort, G. E. Mints & A. O. Slisenko - 1971 - Journal of Symbolic Logic 36 (3):525.
On the Practical Value of Herbrand Disjunctions.Uwe Petermann - 2000 - Logic and Logical Philosophy 8:153.
On the Non-Confluence of Cut-Elimination.Matthias Baaz & Stefan Hetzl - 2011 - Journal of Symbolic Logic 76 (1):313 - 340.
Added to PP
Historical graph of downloads