A Decision Procedure for Herbrand Formulae without Skolemization

arXiv1709.00191MaRDI QIDQ6290760

Timm Lampert

Publication date: 1 September 2017

Abstract: 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 $vee$ 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 $AdashvvdashAwedgeA$ (= $wedge$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 $wedge$I to a minimum in the NNF-calculus. In the case of Herbrand formulae, it is even possible to entirely abstain from applying $wedge$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 $wedge$I-minimal proof strategy in the case of a general search for proofs of contradiction.

Mathematics Subject Classification ID

Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03)

This page was built for publication: A Decision Procedure for Herbrand Formulae without Skolemization