A Decision Procedure for Herbrand Formulae without Skolemization

TL;DR

This paper introduces a novel decision procedure for Herbrand formulae in first-order logic that avoids skolemization and unification, relying solely on equivalence transformations and a specialized calculus.

Contribution

It presents a new algorithm for Herbrand formulae that operates without skolemization or unification, using equivalence transformations and a minimal proof search strategy.

Findings

The procedure can decide Herbrand formulae without skolemization.

It allows for proof searches that minimize the use of the  rule.

The method can be integrated into optimized proof search algorithms.

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 $A \dashv\vdash A \wedge A$ (= $\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.