Timm Lampert
Humboldt-University, Berlin
This 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.
Keywords Predicate Logic  decision procedure  anti-prenex normal forms  proof search  Herbrand formulae
Categories (categorize this paper)
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

 PhilArchive page | Other versions
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

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.
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.
Remarks on Herbrand Normal Forms and Herbrand Realizations.Ulrich Kohlenbach - 1992 - Archive for Mathematical Logic 31 (5):305-317.
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 index

Total views
102 ( #107,235 of 2,455,762 )

Recent downloads (6 months)
5 ( #143,415 of 2,455,762 )

How can I increase my downloads?


My notes