A Decision Procedure for Herbrand Formulas without Skolemization


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.



External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

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

237 (#81,239)

6 months
59 (#70,568)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Timm Lampert
Humboldt-University, Berlin

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references