ar X iv :s ub m it/ 19 94 07 4 [ cs .L O ] 1 S ep 2 01 7 A DECISION PROCEDURE FOR HERBRAND FORMULAE WITHOUT SKOLEMIZATION TIMM LAMPERT Humboldt University Berlin, Unter den Linden 6, D-10099 Berlin e-mail address: lampertt@staff.hu-berlin.de 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 ∨ 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: first-order logic; decision procedure; Herbrand formulae; proof search; antiprenex normal forms. 1. Introduction Definition 1.1. A Herbrand formula is a formula in prenex normal form whose matrix is a conjunction of atomic or negated atomic formulae. [Boerger et al.], section 8.2.2, describe a decision procedure for the contradictoriness of Herbrand formulae that reduces the decision problem for such formulae to the unification problem, which is decidable; cf. [Boerger et al.], Theorem 8.2.1. This reduction presumes skolemization. Consequently, the unification algorithm concerns not only bound variables but also function symbols. The reduction of the decision procedure to the unification problem is based on the condition that no variable occurs in two literals after skolemization and subsequent equivalence transformations. This condition is satisfiable in the case of Herbrand formulae. However, it is very specific. For this reason, it is difficult to transfer strategies related to such a decision procedure to other types of first-order formulae. As an alternative to this approach, I will describe in the following how the contradictoriness of Herbrand formulae can be decided without skolemization. I will refer to nothing c© Lampert 1 2 LAMPERT but equivalence transformations of negative normal forms (NNFs) of pure first-order logic (FOL), without names, free variables, function symbols or identity. The decision problem for contradictoriness of Herbrand formulae will also be reduced to a problem of unifying literals. However, unifying literals through a logically valid proof procedure within FOL amounts to answering the question of to what extent universally quantified variables can be replaced with existentially quantified variables in NNFs. There is no need to refer to function symbols and, thus, to go beyond pure FOL for deciding the contradictoriness of Herbrand formulae. Consequently, there is also no need to refer to the axiom of choice for justifying skolemization; cf. the proof of Lemma 2.1.9 in [Boerger et al.], p. 26. Instead, the decision procedure presented in this paper rests on considerations concerning pure FOL proofs and nothing else. I begin from FOL formulae expressed as NNFs. Definition 1.2. Negative normal forms (NNFs) are formulae that contain only ¬, ∧ and ∨ as sentential connectives, with ¬ occurring only directly in front of atomic expressions. Any formula of FOL can be converted into an NNF through equivalence transformations.1 Herbrand formulae are NNFs in prenex normal form. There is no need to presume prenex normal forms as long as ∨ does not occur in the NNFs of interest. Definition 1.3. ∧-NNFs are NNFs without ∨. Any disjunction is contradictory iff each disjunct is contradictory. Therefore, a disjunction is decidable if each disjunct is decidable. Consequently, the greatest profit in applying a decision procedure for ∧-NNFs arises from driving ∨ outward as far as possible by generating FOLDNFs, i.e., disjunctions of conjunctions of anti-prenex normal forms, which are expressed as NNFs. For a convenient algorithm for converting any FOL formula into a FOLDNF of minimal length 1, cf. [Lampert(2017a)]. The procedure described within this paper enables a decision regarding whether a FOLDNF A is contradictory if each disjunct of A is a ∧-NNF. The decision problem for Herbrand formulae or ∧-NNFs can be reduced to a decision problem for ∧-NNFs ψ with only two literals.2 Definition 1.4. The subformulae ψ of a ∧-NNF φ are formulae that are generated by deleting all but two literals, L1 and L2, in φ and retaining only those quantifiers that bind variables in L1 and L2. Theorem 1.5. A ∧-NNF φ is contradictory iff at least one of its subformulae ψ is contradictory. Proof. Any proof of the contradictoriness of a ∧-NNF φ in the tree calculus (tableaux) can be reduced to a proof of the contradictoriness of ψ; all that must be done is to eliminate quantifiers in the same manner as in the proof of the contradictoriness of ψ. 1Cf., e.g., [Nonnengart & Weidenbach], section 3.2. 2 I refer to two occurrences of literals and not to an arbitrary number of occurrences of two types of literals. A DECISION PROCEDURE FOR HERBRAND FORMULAE 3 I will describe in sections 6 to 11 how one can decide whether a subformula ψ is contradictory by considering whether the pair {L1, L2} is unifiable. In the preceding sections 2 to 5, I will establish general presuppositions for proofs of contradiction for NNFs. In sections 12 to 13, I will explain how to make use of the decision regarding the possibility of unifying {L1, L2} to optimize the search for general proofs of contradiction. Finally, in section 14, I will consider what questions arise when generalizing the strategy of the described decision procedure. 2. Unification Proofs of contradiction depend on the unification of pairs of connected literals. This section explains what that means. I will use subscripted x variables ('x variables' for short) to represent variables in NNFs that are bound by universal quantifiers and subscripted y variables ('y variables' for short) to represent those bound by existential quantifiers. Furthermore, I assume that the NNFs are maximally subscripted. Definition 2.1. Maximally subscripted NNFs are NNFs in which any two quantifiers bind different variables. Any NNF can be transformed into a maximally subscripted NNF with universally quantified x variables and existentially quantified y variables. To do so, the variables must be renamed by means of SUB1 and SUB2; cf. table 1. ∃μA(μ) ⊣⊢ ∃νA(ν/μ) Restriction: ν does not occur in A(μ) SUB1 ∀μA(μ) ⊣⊢ ∀νA(ν/μ) Restriction: ν does not occur in A(μ) SUB2 Table 1: Laws of Substitution The question of unifiability is whether x variables can be replaced with y variables in a maximally subscripted NNF such that identical y variables occupy identical positions3 in connected literals. A pair of connected literals of a maximally subscripted NNF is defined as follows: Definition 2.2. Two literals L1 and L2 of a maximally subscripted NNF with universally quantified x variables and existentially quantified y variables constitute a pair of connected literals iff (1) L1 is not negated, whereas L2 is negated. (2) L1 and L2 contain the same predicate letter φ. (3) The same number of positions succeed φ. (4) If position n in L1 is occupied by yi, then position n in L2 is not occupied by yj for i 6= j. Manifestly, these conditions are necessary for L1 and L2 to constitute a unifiable pair of literals that might contribute to a proof of contradiction. A maximally subscripted NNF that does not contain any pair of connected literals cannot be contradictory. Thus, the decision problem for subformulae ψ is reduced to the corresponding problem for those 3'Identical positions in two literals L1 and L2' means 'the same position in the propositional functions involved'. Thus, I ignore the negation sign that might occur in a literal. In {Fx1y2,¬Fy1y2}, for example, x1 and y1 are in identical positions, as are the two occurrences of y2. 4 LAMPERT subformulae ψ that contain a pair of connected literals L1 and L2. In sections 6 to 11, I will consider only subformulae ψ of this kind. I adopt the following narrow understanding of unification. Definition 2.3. The unification of a pair of connected literals in an NNF is the logically valid procedure of replacing x variables such that identical positions in a pair of connected literals are occupied by identical y variables. A pair of connected literals is unified if all of its positions are occupied by identical y variables. A pair of connected literals is unifiable if it is possible to unify it through unification. It is presumed that during unification, all universally quantified x variables are ultimately eliminated, even in cases such as {Fx,¬Fx}. Unification in the sense of Definition 2.3 is independent of skolemization. In the context of maximally subscripted NNFs, nothing matters for unification but the replacement of x variables with y variables. Unification must obey logical laws. The problem of unification concerns the replacement of x variables with y variables by means of universal quantifier elimination within a correct and complete calculus for NNFs. Before explaining a procedure for solving this problem, I will first establish the calculus that I will adopt for proofs of contradiction for NNFs. I refer to a calculus that applies not only to ∧-NNFs but to NNFs in general because it is desired that it should be possible to extend the considered proof strategies to NNFs in general. 3. NNF-Calculus This section establishes a correct and complete calculus for NNFs that I call the 'NNFcalculus'. As in the tree calculus, proofs in the NNF-calculus are proofs of contradiction: what is to be proven is not that a formula is a theorem but that a formula is a contradiction. Unlike in the tree calculus, however, neither free variables nor names are used. Instead, any proof operates within the realm of pure FOL. Also, in contrast to the tree calculus, the NNFs are not decomposed within proofs in the NNF-calculus. Before universal quantifiers are eliminated for unification, equivalence transformations are applied. Universal quantifier elimination is the last step in a proof of contradiction for the sake of unification in the case that a formula is contradictory; cf. section 4. The rule for universal quantifier elimination is as follows: ∃μ . . .∀νA(μ, ν) ⊢ ∃μA(μ, ν/μ) ∀E Table 2: Universal Quantifier Elimination If ∀ν is within the scope of ∃μ, then the universal quantifier ∀ν is eliminated, and all occurrences of ν in the scope of ∀ν are replaced with μ. It is also allowed to replace ν with μ when ∃μ is a new existential quantifier preceding the resulting formula. I subsume this case under ∀E. I arbitrarily choose the variable y0 as a new y variable and require that y0 does not occur in the expression to the left of ⊢ in ∀E. In addition to ∀E, the following rule is crucial for proofs of contradiction in the NNFcalculus: A ⊣⊢ A ∧A ∧I Table 3: Conjunct Multiplication A DECISION PROCEDURE FOR HERBRAND FORMULAE 5 In proofs of contradiction in the NNF-calculus, ∧I is used to multiply universally quantified expressions to the effect that x variables of different conjuncts are replaced with different y variables following the generation of suitable maximally subscripted prenex normal forms; cf. Example 4.1, p. 7. By virtue of this multiplication of universally quantified expressions, one can avoid the need for a rule for existential quantifier elimination and the need to decompose the NNFs. The ability to solve decision problems involving NNFs within the NNF-calculus depends on the extent to which it is possible to define criteria that can be used to decide which universally quantified expressions must be multiplied how often in order to prove that a formula is a contradiction through the ultimate application of ∀E. As we will see, the establishment of such criteria depends on equivalence transformations that include the application of ∧I. Proving a contradiction by means of unification within the NNF-calculus results in a DNF matrix in which each disjunct contains a literal and its negation. Definition 3.1. The DNF matrix of a formula φ is the scope that one obtains if φ is transformed into a prenex normal form and the resulting scope of that prenex normal form is then transformed into a disjunctive normal form (DNF). Definition 3.2. An explicit contradiction is a formula without universal quantifiers and with a DNF matrix in which any disjunct contains a literal and its negation. In proofs of contradiction in the NNF-calculus, the aim is to derive explicit contradictions by unifying connected literals through the application of ∀E subsequent to equivalence transformations that include the application of ∧I. In addition to ∀E and ∧I, the NNF-calculus comprises well-known rules for generating diverse normal forms, such as (i) definitions of sentential connectives and quantifiers as well as De Morgan's laws for generating NNFs, (ii) distributive laws for generating disjunctive and conjunctive normal forms (DNFs and CNFs), and (iii) PN laws (cf. table 5) for generating prenex and anti-prenex normal forms. Finally, we presume the laws of substitution for renaming variables (cf. table 1), associative and commutative laws for ∧ and ∨, and commutative laws for sequences of universal or existential quantifiers. With the exception of ∀E, all rules are well-known logical equivalence rules. Theorem 3.3. The NNF-calculus is correct and complete. Proof. The correctness of the NNF-calculus follows from the fact that all of its rules are well-known correct derivation rules. Its completeness can be proven by showing that any proof within the correct and complete tree calculus can be transformed into a proof in the NNF-calculus. Each quantified expression that is decomposed n times in a proof within the tree calculus is multiplied by applying ∧I n− 1 times in the corresponding proof within the NNF-calculus. Subsequently, one generates a prenex normal form in which any quantifier Y that is eliminated later than a quantifier X on the same proof path in the tree calculus is in the scope of X. Finally, ∀E is applied such that the same literals are unified. The resulting DNF matrix is contradictory iff all proof paths within the tree calculus are closed. In section 5, a further rule, ∃M (cf. table 4), will be added to the NNF-calculus, but only to avoid applications of ∧I in proofs of subformulae ψ. We will prove that any number of applications of ∃M can always be replaced with one application of ∧I when proving that a subformulae ψ is contradictory; cf. Theorem 8.4. 6 LAMPERT NNF φ ❄ FOLDNF φ ′ D1 ∨ . . . ∨Dn ❄ anti-prenex, ∧I-optimized D∗i ❄ optimal prenex normal form D∗∗i with DNF matrix ❄ explicit contradiction D∗∗∗i after the application of ∀E Figure 1: Steps of proof in the NNF-calculus 4. Proofs in the NNF-Calculus This section provides a brief general overview of the essential steps of proofs of contradiction in the NNF-calculus. The general strategy for such proofs also underlies the specific decision procedure for subformulae ψ described in the following sections. The specific steps of the proof procedure cannot be explained or justified in detail for the general case of NNFs at this point. In the following sections, the principles of the proof strategy are explained and justified in detail with respect to the special case of subformulae ψ. Terms such as 'anti-prenex, optimized FOLDNFs', '∧I-optimized proof', '∧I-minimal proof' and 'optimal prenex normal forms' are explained in this section only to the extent that is necessary for a rough understanding. An NNF φ is first transformed into a sat-equivalent, anti-prenex, optimized FOLDNF φ ′ (= D1 ∨ . . . ∨ Dn). An effective procedure for transforming a FOL formula φ into a logically equivalent FOLDNF φ′ is described in [Lampert(2017a)], section 2. A procedure for optimizing a FOLDNF is introduced in section 12 below. It consists of deleting literals from Di that are not part of any unifiable pair of literals in Di. This first step of generating an anti-prenex, optimized FOLDNF drives quantifiers inward to the greatest possible extent by applying PN-laws (= anti-prenex, cf. Definition 6.1). This is essential for the desired proof strategy; cf. section 6. By contrast, ∨ is driven outward as far as possible, which makes it possible to reduce the decision problem for φ to a decision problem concerning single disjuncts of the resulting FOLDNF. The second step is to compute, for each single disjunct Di, whether a sat-equivalent, anti-prenex, ∧I-optimized formula D∗i can be generated. ∧I-optimized means that ∧I is applied no more than is necessary in the case that a proof of contradiction can be identified. I refer to the corresponding proofs as ∧I-minimal proofs and to the corresponding proof strategy as the ∧I-minimal proof strategy. This step is the most crucial and problematic one. Section 14 briefly summarizes the questions that arise when computing the applications of A DECISION PROCEDURE FOR HERBRAND FORMULAE 7 ∧I in the general case of FOL formulae. This paper avoids answering these questions by restricting all consideration to ∧-NNFs. It can be shown that in the case of this fragment of FOL, ∧I must be applied no more than once (or even not at all, if one allows for ∃M) to prove that a ∧-NNF is contradictory; cf. Theorems 8.4 and 12.3. As the third step, each D∗i is transformed into an optimal prenex normal form D ∗∗ i with a DNF matrix. A prenex is optimal iff the universal quantifier ∀ν is within the scope of the existential quantifier ∃μ if ν is to be replaced with μ to derive an explicit contradiction through the application of ∀E; cf. also Definition 10.6, p. 23. As the last step, ∀E is applied to derive an explicit contradiction D∗∗∗i . Each step of the proof is an equivalence transformation with respect to satisfiability. This is also true in the case of this last, non-essential step because the decision-making is independent of this last step and ∀E is applied only if Di is contradictory. Figure 1 schematizes proofs in the NNF-calculus in accordance with this proof strategy. Example 4.1 illustrates a ∧I-minimal proof of contradiction in the NNF-calculus that requires the application of ∧I. Example 4.1. ∀x1(∀x2∀x6Fx1x2x6 ∨ ∀x3∀x7¬Fx3x1x7) ∧ ∃y1∀x4∃y3¬Fy1x4y3 ∧ ∃y2∀x5∃y4Fx5y2y4 (4.1) This is a FOLDNF with only one contradictory disjunct Di that contains ∨. The proof depends on the unification of the two pairs of connected literals {Fx1x2x6,¬Fy1x4y3} and {Fx5y2y4,¬Fx3x1x7}. To unify these pairs, x1 must be replaced with y1 in the first pair and with y2 in the second pair. To do so, ∧I must be applied once to duplicate the first conjunct of (4.1). We prescribe that the variables of quantifiers occurring within the conjuncts resulting from the application of ∧I are to be maximally subscripted by increasing the depth of their indices by one. This results in the following formula D∗i : ∀x11(∀x21∀x61Fx11x21x61 ∨ ∀x31∀x71¬Fx31x11x71) ∧ ∀x12(∀x22∀x62Fx12x22x62 ∨ ∀x32∀x72¬Fx32x12x72) ∧ (4.2) ∃y1∀x4∃y3¬Fy1x4y3 ∧ ∃y2∀x5∃y4Fx5y2y4 I refer to the number of levels of indices of a variable as its depth. Variables of Di such as x1 have a depth of one. Each application of ∧I increases the level of any variables that are bound by quantifiers occurring in the multiplied conjunct by one. For example, x11 and x12 each have a depth of 2. Definition 4.2. A derivate of a variable μ of depth 1 is any variable that is identical to μ if one deletes all indices at levels > 1. A derivate of a pair of literals {L1, L2} with variables of depth 1 is a pair of literals that is identical to {L1, L2} if one deletes all indices at levels > 1. In formula (4.2), x11 and x12 can be replaced with y1 and y2, respectively, to unify derivates of the original pairs of literals. However, the application of ∧I and the intended substitutions x11/y1 and x12/y2 cause the proof to now also depend on the unification of the pair of literals {Fx12x22x62 , ¬Fx31x11x71}. This results in the following set of pairs of 8 LAMPERT literals: {{Fx11x21x61 ,¬Fy1x4y3}, {Fx5y2y4,¬Fx32x12x72}, (4.3) {Fx12x22x62 ,¬Fx31x11x71}} The unification of this set of unifiable pairs of literals is sufficient to prove that (4.1) is contradictory. To unify all pairs of literals in (4.3), the x variables must be replaced with y variables in accordance with the following list of substitutions: {{x11 , y1}, {x12 , y2}, {x21 , y0}, {x22 , y1}, {x31 , y2, }, {x32 , y0}, {x4, y0}, {x5, y0}, {x61 , y3}, {x62 , y0}, {x71 , y0}, {x72 , y4}} (4.4) A prenex normal form D∗∗i with an optimal prenex must be generated from (4.2). We specify one possible optimal prenex in the form of an ordered list that contains only the x and y variables: {y0, y1, y2, x4, y3, x5, y4, x11 , x12 , x21 , x22 , x31 , x32 , x61 , x62 , x71 , x72} (4.5) Formulae (4.1), (4.2), (4.3), (4.4), and (4.5) serve as a recipe that shows how ∧I is to be applied to the Di (4.1) in order to generate the D ∗ i (4.2) that is to be transformed into a D∗∗i with the optimal prenex (4.5) in order to unify the literals in (4.3) by applying ∀E such that an explicit contradiction D∗∗∗i is obtained. The crucial question for the application of the ∧I-minimal proof strategy is in which cases a decision can be made based on computing the minimal necessary applications of ∧I within a finite number of steps. The proof strategy ultimately serves the purpose of restricting the number of applications of ∧I to the minimum necessary. This makes it possible to terminate a proof path when it is recognized that no more applications of ∧I can be found on that path that may contribute to a ∧I-minimal proof. Of course, all alternative proof paths that may result in ∧I-minimal proofs must be generated.4 Decidability depends on whether the search tree can be restricted to a finite number of proof paths of finite depth. According to the ∧I-minimal proof strategy, the computation of the necessary applications of ∧I must be related to purely syntactic criteria. In this paper, we will study this proof strategy only in the rather simple case of subformulae ψ or, consequently, the case of FOLDNFs in which all disjuncts are ∧-NNFs; cf. p. 2 above. I will abstain from considering FOLDNFs in the following sections 6 to 11; instead, I will consider only subformulae ψ. As we will see, one can decide the contradictoriness of subformulae ψ without any application of ∧I. I call the resulting sat-equivalent formulae ∃M-optimized formulae. This terminology and the generation of ∃M-optimized formulae are explained in section 7. Figure 2 schematizes proofs for subformulae ψ using ∃M in the NNF-calculus. 4Unlike in the tree calculus, different proof paths search for different ∧I-minimal proofs. Therefore, it is proven that Di is contradictory as soon as a ∧I-minimal proof is found on any proof path. By contrast, in the case that all proof paths terminate without the identification of any ∧I-minimal proof, it is proven that Di is not contradictory. The question lies in the extent to which such termination can be achieved based on correct criteria for termination; cf. section 14. A DECISION PROCEDURE FOR HERBRAND FORMULAE 9 NNF ψ ❄ anti-prenex ψ ′ ❄ anti-prenex, ∃M-optimized ψ ′′ ❄ optimal prenex normal form ψ∗ with a DNF matrix ❄ explicit contradiction ψ∗∗ after the application of ∀E Figure 2: Steps of proof for a subformula ψ 5. ∧I-Minimal Proofs We are looking for an intelligent algorithm to decide whether explicit contradictions can be derived in the NNF-calculus and, if so, how. The proof strategy that will be exemplified in the following for the case of subformulae ψ consists of a systematic search for ∧I-minimal proofs by means of equivalence transformations. Definition 5.1. A proof in the NNF-calculus is ∧I-minimal iff each application of ∧I in the proof is necessary. An application of ∧I is necessary iff no explicit contradiction could be derived any longer if one of the conjuncts resulting from the application of ∧I were to be eliminated and all remaining x variables were substituted as before. Example 5.2. Consider the elimination of the second conjunct in formula (4.2) of Example 4.1, p. 7. Replacing the remaining x variables in accordance with the substitution list given in (4.4) does not result in an explicit contradiction. Therefore, the described proof is ∧minimal. Note that ∧I-minimal proofs are defined with respect to given proofs of contradiction. It is possible for two different ∧I-minimal proofs for the same Di to exist that differ in their numbers of applications of ∧I. A ∧I-minimal proof is therefore not necessarily the proof with the smallest number of applications of ∧I necessary to prove some Di contradictory. In a ∧I-minimal proof search, ∧I is applied only to unify pairs of literals by means of ∀E. To avoid unnecessary applications of ∧I, one needs to consider only the minimal sets of unifiable pairs that are necessary for proving a contradiction. Likewise, the unification of such a set with substitution list σ1 must be minimal ; i.e., no substitution list σ2 (σ1 6= σ2) that unifies the same minimal set of unifiable pairs of literals may exist such that any member of σ2 is a part of a member of σ1. A ∧I-minimal proof is also incompatible with an application of ∧I that, in turn, induces another application of ∧I for the purpose of replacing x variables with y variables in two similar conjuncts of D∗i by means of similar 10 LAMPERT substitutions to unify similar pairs of literals; here, conjuncts, substitutions and pairs of literals are considered similar iff they are identical after indices at levels > 1 are deleted (cf. the discussion in section 14 on the 'loop criterion'). ∧I-minimal proofs are very elegant; any application of ∧I is the result of a systematic proof search. I will restrict the following discussion to subformulae ψ. Deciding upon these formulae allows one to identify unifiable pairs of literals. This capability can be utilized for an optimized search for proofs of contradiction; cf. sections 12 and 13. Furthermore, subformulae ψ serve as a simple example to illustrate how the ∧I-minimal proof strategy can be used to define a decision procedure. This proof strategy is also interesting because the justification of such a decision procedure does not depend on any model theory or semantics; it is sufficient to refer to syntactic considerations concerning the unification of pairs of literals within the NNF-calculus. Finally, a ∧I-minimal proof strategy is also interesting because it is efficient, in a certain sense. Proofs of contradiction within the tree calculus become inefficient when quantified expressions are decomposed several times without each decomposition being necessary for the proof. In the NNF-calculus, the same applies to applications of ∧I for the replacement of x variables with y variables that do not contribute to a proof of contradiction. ∧I-minimal proofs restrict the elimination of universal quantifiers to the minimum extent necessary for unifying the members of a minimal set of pairs of literals. I will not discuss questions of efficiency any further in this paper because from here on, I will consider only simple subformulae ψ to show that a decision procedure for these formulae is optimally ∧I-minimal. Definition 5.3. A decision procedure for formulae φ is optimally ∧I-minimal if it is possible to decide whether the formulae φ are contradictory without applying ∧I. In a certain respect, optimally ∧I-minimal decision procedures correspond to decision procedures with blocking in the tree calculus.5 In general, ∧I is necessary to prove that formulae are contradictory, as illustrated by Example 4.1. In the case of subformulae ψ, however, one can abstain from the application of ∧I altogether. If ψ is contradictory, then an optimally ∧I-minimal decision procedure for ψ will find a sat-equivalent formula ψ∗ that allows one to unify the pair of literals in ψ∗ by applying ∀E without applying ∧I at all. If ψ is not contradictory, then computation of the minimal applications of ∧I prior to any actual application of either ∧I or ∀E will reveal that no such sat-equivalent formula ψ∗ can be found. In the following, I will define such an equivalence transformation that will result in a formula ψ∗ without the need to apply ∧I in the case of a contradictory formula ψ. The ability to avoid the application of ∧I is a significant feature of subformulae ψ. The ideal of an optimally ∧I-minimal decision procedure can be realized in the case of such formulae. To make this possible, however, one must use the following rule under certain conditions: ∃μ(φ(μ) ∧ ψ(μ)) ⊢ ∃μ1φ(μ/μ1) ∧ ∃μ2ψ(μ/μ2) ∃M Table 4: Existential Quantifier Multiplication We allow for indices of y variables at levels > 1 subsequent to the application of ∃M. When an existential quantifier is multiplied by ∃M, the variable bound by the multiplied quantifier is 'separated' within the scope of the quantifier. 5Blocking restricts the introduction of new variables due to existential quantifier elimination in the tree calculus. A DECISION PROCEDURE FOR HERBRAND FORMULAE 11 Definition 5.4. A variable is separated if it is subscripted with different indices at different positions subsequent to the application of ∃M or other logical rules. Hence, the application of ∃M separates μ in the scope of ∃μ(φ(μ)∧ψ(μ)) such that the occurrences of μ are subscripted with an index of 1 in the first conjunct and with an index of 2 in the second conjunct. ∃M can be applied at any level of the logical hierarchy of NNFs, like all other rules of the NNF-calculus. This rule must be applied in an optimally ∧I-minimal decision procedure for subformulae ψ. Such applications, however, must be restricted to those that are satequivalent. Section 7 specifies under what conditions this is the case. Section 8 proves that the contradictoriness of subformulae ψ can be decided within a ∧I-minimal proof strategy without ∃M by applying ∧I no more than once. First, however, the following section 6 explains why and how the scopes in ψ must be minimized in the ∧I-minimal proof strategy. 6. Minimizing Scopes Given a subformula ψ in prenex normal form, the following conditions make it impossible to unify a pair of connected literals {L1, L2} in ψ through the direct application of ∀E without first applying equivalence transformations (that include ∧I or ∃M): suboptimal prenex: An x variable ν must be replaced with a y variable μ to unify {L1, L2}, but ∃μ is in the scope of ∀ν in ψ. x ambiguity: An x variable ν must be replaced with (at least) two existential y variables to unify {L1, L2}. One cannot straightforwardly infer whether ψ is contradictory under these conditions. However, this situation changes if one considers equivalence transformations, in which minimizing scopes as much as possible is crucial. ∀ν(A ∧ B(ν)) ⊣⊢ A ∧ ∀νB(ν) PN1 ∀ν(B(ν) ∧ A) ⊣⊢ ∀νB(ν) ∧ A PN2 ∀ν(A ∨ B(ν)) ⊣⊢ A ∨ ∀νB(ν) PN3 ∀ν(B(ν) ∨ A) ⊣⊢ ∀νB(ν) ∨ A PN4 ∃ν(A ∧ B(ν)) ⊣⊢ A ∧ ∃νB(ν) PN5 ∃ν(B(ν) ∧ A) ⊣⊢ ∃νB(ν) ∧ A PN6 ∃ν(A ∨ B(ν)) ⊣⊢ A ∨ ∃νB(ν) PN7 ∃ν(B(ν) ∨ A) ⊣⊢ ∃νB(ν) ∨ A PN8 ∀ν(A(ν) ∧ B(ν)) ⊣⊢ ∀νA(ν) ∧ ∀νB(ν) PN9 ∃ν(A(ν) ∨B(ν)) ⊣⊢ ∃νA(ν) ∨ ∃νB(ν) PN10 Table 5: PN Laws Definition 6.1. Anti-prenex normal forms are NNFs with quantifiers that have been driven inward as far as possible through the application of PN laws; cf. table 5.6 Anti-prenex normal forms are a crucial part of a ∧I-minimal proof strategy to enable the computation of all possible optimized prenex normal forms; cf. section 10. 6 Cf. [Lampert(2017a)], section 2, for the history of anti-prenex normal forms and various algorithms for minimizing the scopes of quantifiers. 12 LAMPERT Definition 6.2. An optimized prenex normal form of NNF φ is a prenex normal form of φ in which the universal quantifiers have been brought within the scope of the existential quantifiers to the greatest possible extent by applying PN laws to generate prenex normal forms from an anti-prenex normal form of φ. Optimized prenex normal forms are important for deciding whether there exists some optimal prenex, in which a universal quantifier ∀ν is within the scope of an existential quantifier ∃μ if ν is to be replaced with μ for unification; cf. p. 7 above and Definition 10.6 below. Furthermore, within the ∧I-minimal proof strategy, generating anti-prenex normal forms is important for multiplying universal quantifiers by applying PN9 to the maximal extent.7 This avoids the need to apply ∧I in the case that x variables must be replaced with different y variables in different literals for unification. Minimizing scopes is a strategy for computing how many applications of ∧I, if any, are necessary to generate optimal prenexes and to replace x variables in different literals with different y variables. Applications of ∧I are at most necessary if, after transformation into anti-prenex normal forms, no optimal prenex can be generated or an x variable must be replaced with more than one y variable for unification. Because ψ does not contain ∨, it is sufficient to apply PN1, PN2, PN5, PN6 and PN9 to generate the anti-prenex normal form ψ′ from ψ by means of the following algorithm: Algorithm 6.3. (1) ψ = ψ′. (2) If ψ′ contains a subformula ρ in the form of ∀ν(A ∧ B(ν)), apply PN1 and replace ρ in ψ′ with A ∧ ∀νB(ν). The new result becomes ψ′. Go to (2) if the new result ψ′ is different from the initial formula ψ′; otherwise, go to (3). (3) If ψ′ contains a subformula ρ in the form of ∀ν(B(ν) ∧ A), apply PN2 and replace ρ in ψ′ with ∀ν(B(ν) ∧ A). The new result becomes ψ′. Go to (2) if the new result ψ′ is different from the initial formula ψ′; otherwise, go to (4). (4) If ψ′ contains a subformula ρ in the form of ∃ν(A ∧ B(ν)), apply PN5 and replace ρ in ψ′ with A ∧ ∃νB(ν). The new result becomes ψ′. Go to (2) if the new result ψ′ is different from the initial formula ψ′; otherwise, go to (5). (5) If ψ′ contains a subformula ρ in the form of ∃ν(B(ν) ∧ A), apply PN6 and replace ρ in ψ′ with ∃νB(ν) ∧ A. The new result becomes ψ′. Go to (2) if the new result ψ′ is different from the initial formula ψ′; otherwise, go to (6). (6) If ψ′ contains a subformula ρ in the form of ∀ν(A(ν) ∧ B(ν)), apply PN9 and replace ρ in ψ′ with ∀νA(ν) ∧ ∀νB(ν). The new result becomes ψ′. Go to (2) if the new result ψ′ is different from the initial formula ψ′; otherwise, go to (7). (7) Maximally subscript ψ′, return the maximally subscripted result ψ′, and terminate. When Algorithm 6.3 reaches (7), either no quantifier is present above ∧ in ψ′ or ψ′ contains a subformula ρ in the form of ∃ν(B(ν) ∧ A(ν)). 7In the case of anti-prenex forms that contain ∨, the scope of universal quantifiers must be transformed into a CNF, and the scope of existential quantifiers must be transformed into a DNF under certain conditions. This results in further multiplications of quantifiers; cf. [Lampert(2017a)], section 2. In the case of a decision procedure for ∧-NNFs, however, we can avoid such transformations. A DECISION PROCEDURE FOR HERBRAND FORMULAE 13 Theorem 6.4. Algorithm 6.3 is a logical equivalence transformation. Proof. Algorithm 6.3 involves nothing but the application of PN laws (cf. table 5) and laws of substitution (cf. table 1). These laws are all logical equivalence rules. Since Algorithm 6.3 is a logical equivalence transformation, ψ′ is a forteriori satequivalent to ψ. Theorem 6.5. Algorithm 6.3 terminates. Proof. This theorem follows from the fact that each rule reduces the depth of the formula, starting with a quantifier. If ψ contains n quantifiers, the algorithm will terminate after no more than n applications of one of the PN laws and 2 * n subsequent applications of SUB1 or SUB2. Let ψ′ contain a sequence of existential quantifiers of length > 1 above ∧, let the innermost existential quantifier of that sequence bind a variable that occurs in both conjuncts, and let the same not hold for all existential quantifiers of that sequence. In this case, sorting the quantifiers of the sequence such that all existential quantifiers that bind a variable occurring in only one conjunct are to the right of all other existential quantifiers in the sequence makes it possible to drive those quantifiers farther inward by applying PN5 or PN6. However, there is no need to consider such quantifier sorting here because it does not allow for any further application of PN1, PN2 or PN9, and it is only the application of these rules that leads to the intended effect of universal quantifiers either no longer being in the scope of certain existential quantifiers or being multiplied. Example 6.6. No. Formula Rule (1) ∃y1∀x1∃y2∀x2∃y3(Fx1x2y1y1 ∧ ¬Fy2y3x1y1) ψ (2) ∃y1∀x1∃y2∀x2(Fx1x2y1y1 ∧ ∃y3¬Fy2y3x1y1) PN5 (3) ∃y1∀x1∃y2(∀x2Fx1x2y1y1 ∧ ∃y3¬Fy2y3x1y1) PN2 (4) ∃y1∀x1(∀x2Fx1x2y1y1 ∧ ∃y2∃y3¬Fy2y3x1y1) PN5 (5) ∃y1(∀x1∀x2Fx1x2y1y1 ∧ ∀x1∃y2∃y3¬Fy2y3x12y1) PN9 (6) ∃y1(∀x1∀x2Fx1x2y1y1 ∧ ∀x3∃y2∃y3¬Fy2y3x3y1) SUB2 Table 6: Transformation in Accordance with Algorithm 6.3 In step 1 of the sat-equivalence transformation that makes it possible to decide the contradictoriness of ψ, the subformula ψ is transformed into an anti-prenex formula ψ′. However, this is not sufficient to define a sat-equivalence transformation that drives quantifiers inward to the maximal extent. For this purpose, ∃Mmust be applied to drive quantifiers above ∧ inward if they bind variables in both conjuncts and if such an application is satequivalent. The following section specifies the conditions for a sat-equivalent application of ∃M. 7. ∃M-Optimization Applying ∃M enables one to apply PN laws to further minimize the scopes of quantifiers. 14 LAMPERT Definition 7.1. ∃M-optimization is a sat-equivalent application of ∃M to an anti-prenex, maximally subscripted formula ψ′ followed by the application of Algorithm 6.3. The initial formula ψ must be transformed into a sat-equivalent, anti-prenex and ∃Moptimized formula ψ′′ to achieve proofs of contradiction without the need to apply ∧I. In the following, I will first identify two cases in which the application of ∃M is not sat-equivalent. Then, I will prove that these are the only two cases in which the application of ∃M is not sat-equivalent. In doing so, I will refer to nothing but the question of the unifiability of {L1, L2} in ψ′. Thus, the sat-equivalent applications of ∃M will be specified without referring to model theory or semantics. What I call the 'direct case' of the violation of the requirements for a sat-equivalent application of ∃M is defined below. Definition 7.2. Direct Case: The y variable μ that is to be multiplied and, thus, separated by applying ∃M occurs in identical positions in L1 and L2 before ∃M is applied. In this case, separating a y variable that occurs in identical positions before the application of ∃M transforms a pair of connected literals into a pair of unconnected literals, which is no longer unifiable. This is already true in the simplest case of ∃y1(Fy1 ∧ ¬Fy1). This formula is contradictory. Applying ∃M leads to the satisfiable (non-contradictory) formula ∃y11Fy11 ∧ ∃y12¬Fy12 . Therefore, the application of ∃M is manifestly not sat-equivalent in the direct case. In this case, 'y unambiguity' is lost: the same y variable occurs in identical positions before the application of ∃M, whereas different y variables occupy these positions after the application of ∃M. Hence, we exclude such cases from among the valid applications of ∃M. The second case in which the requirements for a sat-equivalent application of ∃M are violated is what I call the 'indirect case'. To define it, let us introduce the concept of an 'xx list', which we define recursively: Definition 7.3. The xx lists of a pair of connected literals {L1, L2} are generated as follows: (1) If an x variable ν1 and an x variable ν2 occur in identical positions in L1 and L2, then ν1 and ν2 are members of the same xx list. (2) If the x variables ν1 and ν2 are members of the same xx list and if ν2 and the x variable ν3 are also members of the same xx list, then ν1, ν2 and ν3 are all members of the same xx list. (3) (1) and (2) are the only conditions that determine members of the same xx list. All x variables of an xx list must be replaced with the same y variable to unify {L1, L2}. Example 7.4. Let ψ′ be the following formula: ∃y1(∀x1∀x2Fy1x1x1x2x2 ∧ ∀x3∀x4¬Fx3x3x4x4y1) (7.1) The following pair of connected literals {L1, L2} must be unified: {Fy1x1x1x2x2,¬Fx3x3x4x4y1}. (7.2) x1 occurs in the same positions as x3 and x4. Therefore, x1 and x3 as well as x1 and x4 are members of the same xx list, according to Definition 7.3(1). Hence, x1, x3 and x4 are also members of the same xx list, according to Definition 7.3(2). x2 is in the same position as x4. Therefore, x2 and x4 are members of the same xx list, according to Definition 7.3(1). Since x4 is also a member of the xx list {x1, x3, x4}, x2 is a member of this list as well, A DECISION PROCEDURE FOR HERBRAND FORMULAE 15 according to Definition 7.3(2). This results in the following xx list, which is the only xx list of (7.2): {x1, x2, x3, x4} (7.3) Furthermore, we define xy and yx pairs as follows: Definition 7.5. An xy pair is an ordered list {xvar, yvar} consisting of an x variable xvar and a y variable yvar, where xvar occurs in L1 in a position n and yvar occurs in L2 in the same position n. A yx pair is an ordered list {yvar, xvar} consisting of a y variable yvar and an x variable xvar, where yvar occurs in L1 in a position n and xvar occurs in L2 in the same position n. An x variable xvar must be replaced with the y variable yvar if xvar and yvar occur in the same xy or yx pair. Example 7.6. (7.4) is the only xy pair of (7.2), and (7.5) is the only yx-pair of (7.2). {x2, y1} (7.4) {y1, x3} (7.5) (7.1) is contradictory: (7.2) can be unified by replacing all x variables with y1, which is possible because {y1, x1, x2, x3, x4} represents an optimal prenex that can be generated by applying PN laws to (7.1). The application of ∃M to (7.1), however, is not sat-equivalent because this would separate y1 into y11 in the first conjunct and y12 in the second conjunct. Consequently, x3 must be replaced with y11 because of (7.5), and x2 must be replaced with y12 because of (7.4). However, according to (7.3), x1, x2, x3 and x4 all must be replaced with the same y variable to unify (7.2). Based on the above discussion, the indirect case of the violation of the requirements for a sat-equivalent application of ∃M can be defined as follows: Definition 7.7. Indirect case: {L1, L2} has an xx list A such that at least one x variable xvar1 from A is a member of an xy list {xvar1, yvar}, at least one x variable xvar2 from A (xvar1 6= xvar2) is a member of a yx list {yvar, xvar2}, and all universal quantifiers binding the x variables in A are within the scope of ∃yvar in ψ, where yvar is the y variable multiplied by ∃M. On p. 17 below, I will justify why this case is restricted to x variables that are bound by quantifiers in the scope of the existential quantifier that is multiplied by ∃M (Case 3(β) below). In contrast to the direct case, one might say that 'x unambiguity' is lost in the indirect case: whereas all x variables of an xx list must be replaced with one and the same y variable before the application of ∃M, they must be replaced with different y variables after the application of ∃M. Hence, we exclude not only the direct case but also the indirect case from among the valid applications of ∃M. In the following, I justify why the direct and indirect cases are the only two cases that must be excluded to restrict ∃M to sat-equivalent applications. In doing so, we consider nothing but logically valid equivalence transformations to unify positions of a pair of connected literals within a subformula ψ′. The syntactic properties that determine the unifiability of a pair of connected literals are (i) the order of the quantifiers and (ii) the identity or difference of the variables at certain positions of the literals. The order of the quantifiers, however, is not adversely affected by the application of ∃M because any ∃M-optimization results in a minimized scope. This can 16 LAMPERT only increase the possibility of generating optimal prenexes. In addition to the changes to quantifier order, ∃M separates the multiplied y variable as well as those x variables that (i) are bound by a universal quantifier that is to the left of the multiplied existential quantifier before ∃M is applied and (ii) occur in both literals, L1 and L2. The separation of x variables subsequent to the separation of the multiplied y variable is due to the application of PN9 in ∃M-optimization. This separation cannot have a negative effect on unifiability because it enables the coverage of positions in different literals with different y variables. Therefore, the unifiability of a pair of literals can only be adversely affected by the separation of the multiplied y variable, which is subscripted differently in the two conjuncts subsequent to ∃M-optimization. To identify the cases in which the separation of the multiplied y variable μ transforms a unifiable pair of connected literals into a pair of literals that is no longer unifiable, we distinguish three cases: Case 1: μ occurs in identical positions in L1 and L2. Case 2: μ occurs in identical positions to those of x variables that are not members of an xx list. Case 3: μ occurs in identical positions to those of x variables that are members of an xx list. Note that there is no need to distinguish a case in which μ occurs in the same position as some y variable that is not identical to μ because this violates condition (4) of the definition of a pair of connected literals; cf. Definition 2.2, p. 3. Therefore, these three cases are exhaustive. It may happen that the conditions for more than one of the three cases are satisfied for one and the same pair of connected literals. However, the three cases can be considered separately because the application of ∃M is not sat-equivalent iff the multiplication of μ does not preserve unifiability in regard to at least one case. Case 1 is the direct case. Case 2 cannot induce applications of ∃M that are not satequivalent, as illustrated by the following reasoning: The x variables need to be replaced with μ either (α) in only one of the two literals or (β) in both. In the first case (α), separation of the y variable cannot adversely affect the possibility of unifying the positions in which the x variables occur because the number of y variables with which those x variables need to be replaced for unification does not change. The second case (β) requires that the universal quantifiers that bind x variables that occur in identical positions to those of μ must be to the left of ∃μ before the application of ∃M because otherwise, the x variables will not occur in both L1 and L2 due to the presumed maximal subscription. However, given that (a) ∃μ is in the scope of a universal quantifier ∀ν in the maximally subscripted formula ψ′ and (b) ν and μ occur in both L1 and L2 in identical positions (and ν, therefore, must be replaced with μ in both literals), L1 and L2 are not unifiable anyway, and consequently, ψ′ is not contradictory. ψ′ is not contradictory because it is impossible in case (β) to generate an optimal prenex that would permit the necessary substitutions, even after the minimization of scopes through ∃M-optimization or the application of ∧I (which of the two is done makes no difference; cf. section 8). In any case, at least one universal quantifier ∀νi (νi = ν with an additional subscript of 1 or 2) remains that is necessarily not in the scope of ∃μj (μi = μ with an additional subscript of 1 or 2) in any optimized prenex. The indirect case is a special case of case 3. Again, one can ignore a case (α) in which there is either no xy pair that contains both an x variable from an xx list and μ as members or no yx pair that contains both an x variable from an xx list and μ as members. In such a case, the number of necessary substitutions in regard to the x variables of the xx list would A DECISION PROCEDURE FOR HERBRAND FORMULAE 17 again not be increased by applying ∃M. However, in a case (β) in which some x variable xvar1 in an xx list occurs together with μ in an xy pair and some x variable xvar2 in the same xx list occurs together with μ in a yx pair, the situation is different. Nevertheless, we can identify several conditions under which the application of ∃M is still sat-equivalent. First of all, we can assert that xvar1 6= xvar2 because otherwise the case reduces to case 2. Furthermore, if one universal quantifier ∀ν that binds an x variable ν from the xx list is to the left of ∃μ in ψ′, then {L1, L2} is not unifiable, and ψ′ is not contradictory. This is so because in this case, minimizing scopes through ∃M-optimization or the application of ∧I is necessary. However, minimizing scopes or applying ∧I, where both include maximal subscription, makes it necessary for at least one x variable from the xx list to be replaced with both μ1 and μ2 for unification in one and the same literal, which is logically impossible. Therefore, the only subcase of case 3 is the indirect case, in which xvar1 6= xvar2 and all universal quantifiers binding x variables from an xx list are in the scope of ∃μ in ψ′. Thus, the direct and indirect cases are the only cases that must be excluded to restrict the application of ∃M to sat-equivalent transformations. Definition 7.8. ∃MB is the rule stating that ∃M is applied unless the conditions for either the direct or the indirect case are satisfied. Theorem 7.9. The application of ∃MB is sat-equivalent. Proof. This theorem follows from the above distinction of cases, which shows that the direct and indirect cases are the only cases that imply an application of ∃M that is not sat-equivalent. The proof is based on nothing but proof-theoretic considerations concerning the unification of the pair of connected literals in ψ′ in the NNF-calculus. The following algorithm transforms the initial subformula ψ into a sat-equivalent, antiprenex and ∃M-optimized subformula ψ′′: Algorithm 7.10. (1) Apply Algorithm 6.3 to ψ. The result is ψ′. (2) If an existential quantifier exists above ∧, apply ∃MB to multiply this quantifier if possible. The result is ψ′′. (3) If ψ′ = ψ′′, return ψ′′ and terminate; otherwise, go back to (1). Theorem 7.11. Algorithm 7.10 is a sat-equivalence transformation. Proof. This theorem follows from Theorems 6.4 and 7.9. Theorem 7.12. Algorithm 7.10 terminates. Proof. This theorem follows from Theorem 6.5 and the fact that there can be only a finite number of existential quantifiers in the logical hierarchy above ∧ in ψ. Theorem 7.13. Algorithm 7.10 minimizes the scope of universal quantifiers in ψ to a maximal extent under equivalence transformations and thus maximizes the number of universal quantifiers binding the variables occurring in a pair of connected literals to a maximal extent under equivalence transformations. Proof. The scope of universal quantifiers is not minimized any further by Algorithm 7.10 only if an existential quantifier exists that is in their scope and above ∧ and if the multiplication of this quantifier is not sat-equivalent. Minimizing scopes maximizes the number of applications of PN9 and, therefore, the number of universal quantifiers. 18 LAMPERT Either the resulting formula ψ′′ is a conjunction of two quantified expressions, each one containing exactly one literal, or ψ′′ is a quantified expression with an outermost sequence of quantifiers ending with an existential quantifier ∃μ above ∧, where each conjunct contains exactly one literal and the conditions for either the direct or the indirect case are satisfied. 8. ∃M-Optimization and the Application of ∧I ∃M-optimization minimizes scopes and separates variables. This makes applications of ∧I superfluous in the case of subformulae ψ′. This section demonstrates this claim, first by example and then in general. Example 8.1. Let ψ′ be the following formula: ∀x1∃y1(∀x3Fy1x1x3 ∧ ∀x2¬Fx2y1y1) (8.1) x1 must be replaced with y1 to unify {Fy1x1x3,¬Fx2y1y1}. However, ∀E cannot be applied to (8.1) to achieve this because ∃y1 is in the scope of ∀x1. Independent of ∃Moptimization, one must apply ∧I to replace a derivate of x1 with a derivate of y1; cf. Definition 4.2. Applying ∧I once to multiply ∀x1 results in the following formula: ∀x11∃y11(∀x31Fy11x11x31 ∧ ∀x21¬Fx21y11y11) ∧ (8.2a) ∀x12∃y12(∀x32Fy12x12x32 ∧ ∀x22¬Fx22y12y12) (8.2b) This formula allows one to derive an explicit contradiction by unifying the pair {Fy11x11x31 , ¬Fx22y12y12} through the application of ∀E to a corresponding optimal prenex normal form. Since unifying the stated pair of literals is sufficient to derive an explicit contradiction, we delete the other two literals: ∀x11∃y11∀x31Fy11x11x31 ∧ ∃y12∀x22¬Fx22y12y12 (8.3) Applying PN laws allows one to generate the following optimal prenex normal form from (8.3): ∃y12∀x11∃y11∀x31∀x22(Fy11x11x31 ∧ ¬Fx22y12y12) (8.4) This makes it possible to apply ∀E such that the pair of literals in (8.4) is unified by the following substitutions: {{x11 , y12}, {x22 , y11}, {x31 , y12}}. (8.5) However, the application of ∧I that is involved in this proof is apparently only a cumbersome surrogate for a corresponding ∃M-optimization. This is so because ∃M-optimization directly leads to the following formula, which is identical to (8.3) despite the naming of the x variables: ∀x1∃y11∀x3Fy11x1x3 ∧ ∃y12∀x2¬Fx2y12y12 (8.6) Theorem 8.2. ∃M-optimization makes the application of ∧I superfluous in proofs of contradiction for subformulae ψ. Proof. Applications of ∧I are necessary for unification as long as one does not refer to ∃M-optimized formulae ψ′′ in the following cases: (1) to replace a universal variable ν with an existential variable μ, where ∃μ is in the scope of ∀ν in ψ (case 1; cf. 'suboptimal prenex', p. 11), or A DECISION PROCEDURE FOR HERBRAND FORMULAE 19 (2) to separate a universal variable ν in ψ such that the different variables ν1 and ν2 can be replaced with different y variables (case 2; cf. 'x ambiguity', p. 11). However, these substitutions can be achieved through ∃M-optimization as long as the substitutions are logically valid. The conditions for case 1 or case 2 only hold in ∃M-optimized expressions ψ′′ if ∃ρ is in the scope of ∀ν and above ∧ and if multiplying ∃μ is incompatible with unifying the pair of literals in ψ′. Any application of ∧I to ∀ν would necessarily also multiply ∃ρ. Therefore, applications of ∧I cannot enable unifications that cannot be achieved through ∃M-optimization. Example 8.3. The following formulae exemplify the two cases described above: ∀x1∃y1(∃y2Fy1y2 ∧ ¬Fy1x1) (8.7) ∃y1∃y2∀x1∃y3(∃y2Fy3y1x1 ∧ ¬Fy3x1y2) (8.8) In (8.7), ν = x1, ρ = y1, and μ = y2; in (8.8), ν = x1, μ1 = y1, μ2 = y2, and ρ = y3. To replace x1 in (8.7) with y1, or to replace x1 in L1 of (8.8) with x11 and in L2 of (8.8) with x12 such that x11 can be replaced with y2 and x12 with y1, one must multiply ∃y1 in (8.7) and ∃y3 in (8.8). This applies to both ∃M-optimization and the application of ∧I. However, in both cases, this is incompatible with unifying the first position of both literals. Theorem 8.4. One can generate ψ′′ from ψ without applying ∃M by applying ∧I once. Proof. Let ∃μ be the outermost existential quantifier that is multiplied in Algorithm 7.10. Then, one can obtain ψ′′ from ψ by applying the following algorithm: (1) Apply Algorithm 6.3 to minimize scopes and rename variables. (2) Multiply ∃μA(μ) by applying ∧I once. (3) Delete L2 from the first conjunct along with all quantifiers binding variables that occur only in L2. (4) Delete L1 from the second conjunct along with all quantifiers binding variables that occur only in L1. (5) Apply Algorithm 6.3 to minimize scopes and rename variables. Thus, in a ∧I-minimal proof strategy for subformulae ψ in the NNF-calculus without ∃M, ∧I will be applied at most once. To decide whether ψ is contradictory, it is sufficient to transform ψ into a sat-equivalent, ∃M-optimized formula ψ′′; cf. section 13. In the following, I will first describe how to compute the substitutions that are necessary for unifying the pairs of literals in ψ′′ (section 9). Afterward, I will describe how to generate all optimized prenex normal forms ψ′′′ from ψ′′ (section 10). 9. Substitution List σ To decide whether ψ is contradictory, a substitution list σ is generated. For each x variable, the list specifies the y variables with which it must be replaced to unify the pair of connected literals {L1, L2} in ψ′′. Such a list does not imply that {L1, L2} is unifiable. It may well be that some x variables would need to be replaced with several y variables to unify {L1, L2}. The following algorithm generates σ for a given pair of literals {L1, L2}: 20 LAMPERT Algorithm 9.1. (1) Generate a list σ1 of all pairs of variables {v1, v2} with v1 in position n in L1 and v2 in the same position n in L2, where v1 or v2 (or both) is an x variable. (2) To each level-1 list that contains an x variable ν1 and exactly one y variable μ, recursively add those x variables ν2 (ν1 6= ν2) that occur in some other level-1 list together with ν1. Delete any level-1 list that contains only x variables if all of those x variables also occur in some level-1 list that contains a y variable. Repeat this procedure until no further changes occur. The resulting list is denoted by σ2. (3) Generate a list σ3 consisting of level-1 lists that each contain one x variable ν and all y variables that occur together with ν in some level-1 list in σ2. To generate the level-1 lists in σ3, traverse all x variables ν that occur in σ2 and take all y variables that are members of lists in σ2 of which ν is also a member. If ν is not a member of any list in σ2 that contains a y variable, add {ν, y0} to σ3. Per its definition, y0 does not occur in ψ, ψ ′ or ψ′′. The resulting list is the substitution list σ that specifies how each x variable is to be substituted such that {L1, L2} is unified. Example 9.2. Let {L1, L2} be the following pair: {Fx1x2x2x4,¬Fy2x1x3x4} (9.1) σ1: {{x1, y2}, {x2, x1}, {x2, x3}, {x4, x4}}. σ2: {{x1, x2, x3, y2}, {x4, x4}}. σ3 (=σ(9.1)): {{x1, y2}, {x2, y2}, {x3, y2}, {x4, y0}}. Definition 9.3. x lists are the members (= level-1 lists) of the substitution list σ. Definition 9.4. An x list is unambiguous iff it contains exactly one y variable. σ is unambiguous iff all x lists in σ are unambiguous. Example 9.5. The x lists of σ3 in Example 9.2 and, therefore, σ(9.1) are unambiguous. Definition 9.6. A substitution list σ is maximally separated iff the number of members in σ cannot be increased any further by separating x variables through equivalence transformations. Since Algorithm 7.10 minimizes the scopes of universal quantifiers to the maximal extent under equivalence transformation and, thus, increases the number of universal quantifiers to the maximal extent (cf. Theorem 7.13), the substitution list of ψ′′ is maximally separated. Unlike the substitution list of ψ, the substitution list of ψ′′ is necessarily maximally separated but is not necessarily unambiguous. Example 9.7. Let ψ′′ be as follows: ∃y1∃y2∀x1∃y3(Fy1x1y3 ∧ ¬Fx1y2y3) (9.2) The corresponding substitution list is σ(9.2) = {{x1, y1, y2}}. This substitution list is not unambiguous. However, ∃M cannot be applied to (9.2) because the conditions for the direct case are satisfied. Hence, σ(9.2) is maximally separated but not unambiguous. A decision on the unifiability of a pair of connected literals refers to a maximally separated substitution list. A proof of contradiction according to the ∧I-minimal proof strategy in the NNF-calculus, however, requires an unambiguous substitution list. A DECISION PROCEDURE FOR HERBRAND FORMULAE 21 Algorithm 9.1 generates not minimal but maximal substitution lists. In {Fx1x1y1, ¬Fx2y2x2}, for example, σ = {{x1, y1, y2}, {x2, y1, y2}}: both x lists contain both y1 and y2, which is not necessary. It is only necessary that x1 be substituted with y2 in position 2 of L1, that x2 be substituted with y1 in position 3 of L2, and that x1 and x2 be substituted with one and the same y variable in position 1 of both L1 and L2. This last condition is compatible with two different minimal substitution lists: {{x1, y1, y2}, {x2, y1}} or, alternatively, {{x1, y2}, {x2, y1, y2}}. However, when deciding whether subformulae ψ are contradictory, one can abstain from generating alternative minimal substitution lists. It is sufficient to refer to a maximal substitution list σ because – as proven in section 11 – a necessary condition for the contradiction of a subformula ψ is that the σ of ψ′′ be unambiguous, which implies that there is only one minimal substitution list in this case. If the maximal substitution list σ is not unambiguous, this implies that at least one x variable must be replaced with more than one y variable to unify the pair of literals in ψ′′. This is sufficient to conclude that ψ′′ and, therefore, ψ are not contradictory; cf. Theorem 11.1, condition C1, p. 24. Section 13 will explain how it can be decided whether the pair of literals contained in ψ′′ is unifiable by referring to the syntactic properties of ψ′′ (without any further equivalence transformation). In the following section, however, I will describe a costlier algorithm for such decision-making. This algorithm generates the set of all optimized prenex normal forms ψ′′′ from the anti-prenex, ∃M-optimized normal form ψ′′. I present this algorithm first because it serves as the foundation for the syntactic criteria defined in section 13 that directly refer to ψ′′. 10. Optimized Prenexes This section describes an algorithm that generates all optimized prenex normal forms (cf. Definition 6.2) from an anti-prenex, ∃M-optimized and maximally subscripted formula ψ′′. Since ψ′′ does not contain ∨, only PN1, PN2, PN5 and PN6 need to be considered. To generate the set of all optimized prenex normal forms ψ′′′ from ψ′′ by applying PN laws from right to left, proceed as follows: Algorithm 10.1. (1) ψ+ = {ψ′′}. (2) ψ′′′ = {}. (3) If ψ+ 6= {}, select the first member ψ+1 from ψ + and go to (a); otherwise, return ψ′′′ and terminate. (a) Let ψ+1 be of the form Q(A∧B), where Q is a sequence of quantifiers of length m (m ≥ 0). If neither A nor B contains any quantifier, add ψ+1 to ψ ′′′, delete ψ+1 in ψ + and go to (3); otherwise, go to (b). (b) If PN6 can be applied to A ∧ B, then ψ+1 = QPN6[A ∧ B] and go to (a); otherwise, go to (c). (c) If PN5 can be applied to A ∧ B, then ψ+1 = QPN5[A ∧ B] and go to (a); otherwise, go to (d). (d) If A contains only universal quantifiers, then ψ+1 = QPN1[A∧B] and go to (a); otherwise, go to (e). (e) If B contains only universal quantifiers, then ψ+1 = QPN2[A ∧ B] and go to (a); otherwise, go to (f). 22 LAMPERT (f) Delete ψ+1 in ψ + and add QPN2[A ∧B] and QPN1[A ∧B] to ψ+. Go to (3). Example 10.2. Let ψ′′ be as follows: ∃y1∀x1∃y2∀x2Fy1x1y2x2 ∧ ∀x3∃y3∀x4∀x5¬Fx3y3x4x5 (10.1) The following schema illustrates the application of Algorithm (10.1) to generate ψ+ and ψ′′′ from (10.1). No. ψ+;ψ′′′ Rule (1) ψ+ = {∃y1∀x1∃y2∀x2Fy1x1y2x2 ∧ ∀x3∃y3∀x4∀x5¬Fx3y3x4x5}; ψ′′′ = {} 1, 2 (2) ψ+ = {∃y1(∀x1∃y2∀x2Fy1x1y2x2 ∧ ∀x3∃y3∀x4∀x5¬Fx3y3x4x5)}; ψ′′′ {} 3(b) (3) ψ+ = {∃y1∀x1(∃y2∀x2Fy1x1y2x2 ∧ ∀x3∃y3∀x4∀x5¬Fx3y3x4x5), ∃y1∀x3(∀x1∃y2∀x2Fy1x1y2x2 ∧ ∃y3∀x4∀x5¬Fx3y3x4x5)} ; ψ′′′ = {} 3(f) (4) ψ+ = {∃y1∀x1∃y2(∀x2Fy1x1y2x2 ∧ ∀x3∃y3∀x4∀x5¬Fx3y3x4x5), ∃y1∀x3(∀x1∃y2∀x2Fy1x1y2x2 ∧ ∃y3∀x4∀x5¬Fx3y3x4x5)} ; ψ′′′ = {} 3(b) (5) ψ+ = {∃y1∀x1∃y2∀x3(∀x2Fy1x1y2x2 ∧ ∃y3∀x4∀x5¬Fx3y3x4x5), ∃y1∀x3(∀x1∃y2∀x2Fy1x1y2x2 ∧ ∃y3∀x4∀x5¬Fx3y3x4x5)} ; ψ′′′ = {} 3(d) (6) ψ+ = {∃y1∀x1∃y2∀x3∃y3(∀x2Fy1x1y2x2 ∧ ∀x4∀x5¬Fx3y3x4x5), ∃y1∀x3(∀x1∃y2∀x2Fy1x1y2x2 ∧ ∃y3∀x4∀x5¬Fx3y3x4x5)} ; ψ′′′ = {} 3(c) (7) ψ+ = {∃y1∀x1∃y2∀x3∃y3∀x4(∀x2Fy1x1y2x2 ∧ ∀x5¬Fx3y3x4x5), ∃y1∀x3(∀x1∃y2∀x2Fy1x1y2x2 ∧ ∃y3∀x4∀x5¬Fx3y3x4x5)} ; ψ′′′ = {} 3(d) (8) ψ+ = {∃y1∀x1∃y2∀x3∃y3∀x4∀x5(∀x2Fy1x1y2x2 ∧ ¬Fx3y3x4x5), ∃y1∀x3(∀x1∃y2∀x2Fy1x1y2x2 ∧ ∃y3∀x4∀x5¬Fx3y3x4x5)} ; ψ′′′ = {} 3(d) (9) ψ+ = {∃y1∀x1∃y2∀x3∃y3∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5), ∃y1∀x3(∀x1∃y2∀x2Fy1x1y2x2 ∧ ∃y3∀x4∀x5¬Fx3y3x4x5)} ; ψ′′′ = {} 3(e) A DECISION PROCEDURE FOR HERBRAND FORMULAE 23 (10) ψ+ = {∃y1∀x3(∀x1∃y2∀x2Fy1x1y2x2 ∧ ∃y3∀x4∀x5¬Fx3y3x4x5)}; ψ′′′ = {∃y1∀x1∃y2∀x3∃y3∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5)} 3(a) (11) ψ+ = {∃y1∀x3∃y3(∀x1∃y2∀x2Fy1x1y2x2 ∧ ∀x4∀x5¬Fx3y3x4x5)}; ψ′′′ = {∃y1∀x1∃y2∀x3∃y3∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5)} 3(c) (12) ψ+ = {∃y1∀x3∃y3∀x1(∃y2∀x2Fy1x1y2x2 ∧ ∀x4∀x5¬Fx3y3x4x5)}; ψ′′′ = {∃y1∀x1∃y2∀x3∃y3∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5)} 3(e) (13) ψ+ = {∃y1∀x3∃y3∀x1∃y2(∀x2Fy1x1y2x2 ∧ ∀x4∀x5¬Fx3y3x4x5)}; ψ′′′ = {∃y1∀x1∃y2∀x3∃y3∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5)} 3(b) (14) ψ+ = {∃y1∀x3∃y3∀x1∃y2∀x4(∀x2Fy1x1y2x2 ∧ ∀x5¬Fx3y3x4x5)}; ψ′′′ = {∃y1∀x1∃y2∀x3∃y3∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5)} 3(d) (15) ψ+ = {∃y1∀x3∃y3∀x1∃y2∀x4∀x5(∀x2Fy1x1y2x2 ∧ ¬Fx3y3x4x5)}; ψ′′′ = {∃y1∀x1∃y2∀x3∃y3∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5)} 3(d) (16) ψ+ = {∃y1∀x3∃y3∀x1∃y2∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5)}; ψ′′′ = {∃y1∀x1∃y2∀x3∃y3∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5)} 3(e) (17) ψ+ = {}; ψ′′′ = {∃y1∀x1∃y2∀x3∃y3∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5), ∃y1∀x3∃y3∀x1∃y2∀x4∀x5∀x2(Fy1x1y2x2 ∧ ¬Fx3y3x4x5)} 3(a) Theorem 10.3. Algorithm 10.1 generates only prenex normal forms that are logically equivalent to ψ′′. Proof. This theorem follows from the fact that the PN laws are equivalence rules that are applied from right to left in Algorithm 10.1. Theorem 10.4. Algorithm 10.1 terminates. Proof. This theorem follows from the fact that only a finite number of quantifiers can exist below ∧ in the logical hierarchy of ψ′′. Theorem 10.5. Algorithm 10.1 generates the set of all possible optimized prenex normal forms ψ′′′ from ψ′′. Proof. This theorem follows from the facts that in Algorithm 10.1, PN5 and PN6 are applied prior to PN1 and PN2, and two alternative prenex forms are generated in the case of 3(g). Definition 10.6. An optimal prenex normal form ψ∗ of ψ′′ is a prenex normal form in ψ′′′ such that for all x lists {ν, . . . μj . . .} (j > 0), ∀ν is to the right of each existential quantifier ∃μj. Example 10.7. σ(10.1): {{x1, y3}, {x2, y0}, {x3, y1}, {x4, y2}, {x5, y0}}. Hence, only the second prenex normal form in ψ′′′ from line (17) in the schema above is optimal. 24 LAMPERT 11. sat-Criteria for ψ Theorem 11.1. ψ is not contradictory iff one of the two following conditions is satisfied: C1: The maximally separated substitution list σ of the pair of connected literals in ψ′′ (and, consequently, of each formula from ψ′′′) is ambiguous. C2: No optimal prenex normal form ψ∗ exists in ψ′′′. C1 concerns the substitution list σ of ψ′′, whereas C2 concerns the optimized prenexes in ψ′′′. These are the relevant features on which the unifiability of the pair of connected literals in ψ′′ depends. The unifiability of a pair of literals can be decided by generating ψ, ψ′, ψ′′, ψ′′′, and σ to determine whether C1 or C2 is satisfied. Proof. We prove that Theorem 11.1 holds in the direction from left to right by proving the contrapositive: 'If neither C1 nor C2 is satisfied, then ψ is contradictory'. This follows from the following two points: (1) If C2 is not satisfied, then some optimal prenex form ψ∗ exists, and if C1 is not satisfied, then some unambiguous substitution list σ exists. Under such conditions, the pair of connected literals in ψ∗ can be unified by applying ∀E to replace each x variable in σ with the y variable in the corresponding x list of σ. (2) The transformation of ψ into ψ∗ is a sat-equivalence transformation according to Theorems 7.11 and 10.3. In the proof of the right-to-left direction of Theorem 11.1, C1 and C2 are reduced to 'laws of invalidity' that specify syntactic properties that prevent the application of ∀E for unification. The all-important point is that one can conclude from this that unification is impossible if one refers to optimized prenex normal forms in ψ′′′. The reason for this conclusion is that the conditions for replacing x variables with y variables when applying ∀E are optimal in the case of the optimized prenex normal forms of ψ′′′. Therefore, one can conclude that no sat-equivalent prenex normal form exists that makes the substitutions that are necessary for unification according to σ logically possible if no prenex normal form exists in ψ′′′ that permits such a substitution. Proof. We prove that Theorem 11.1 holds in the direction from right to left: 'If C1 or C2 is satisfied, then ψ is not contradictory.' According to Theorems 7.11, 10.3 and 10.5, ψ′′′ contains all optimized prenex normal forms that are sat-equivalent to ψ. It is necessary to show that C1 and C2 specify the conditions for ψ to be non-contradictory. If the maximally separated substitution list σ is ambiguous, then at least one x variable in ψ′′ and in each formula in ψ′′′ must be replaced with more than one y variable. However, this is logically impossible. C1 is based on the following law of invalidity: . . . ∃μ1 . . . ∃μ2 . . . ∀νφ(μ1, μ2, ν, ν) 6⊢ . . . ∃μ1 . . . ∃μ2 . . . φ(μ1, μ2, ν/μ1, ν/μ2) C1-R. φ(μ1, μ2, ν, ν) is an expression in which ν must be replaced with μ1 and also with μ2 to unify the pair of literals contained in the expression. However, such a substitution is logically invalid because each application of ∀E can only replace ν with either μ1 or μ2 and, according to Theorems 7.13 and 8.2, the number of universal quantifiers cannot be increased any further for the purpose of unification. It is impossible to separate σ any further through sat-equivalence transformations because σ is already maximally separated. However, σ would need to be further separated to make it possible to unify the pair of literals in question by applying ∀E. A DECISION PROCEDURE FOR HERBRAND FORMULAE 25 C2 is based on the following law of invalidity for the set of optimized prenex normal forms ψ′′′: . . . ∀ν . . . ∃μφ(μ, ν) 6⊢ . . . ∃μ . . . φ(μ, ν/μ) B2-R. The application of ∀E requires that ∀ν be in the scope of ∃μ. According to Theorem 10.5, Algorithm 10.1 generates all optimized prenex normal forms (= ψ′′′). The quantifier sequences of the prenex normal forms in ψ′′′ cannot be optimized any further through satequivalence transformations, according to Theorems 7.13 and 8.2. If no optimized prenex normal form in ψ′′′ permits the application of ∀E to achieve all substitutions that are necessary according to σ, then no optimal prenex normal form ψ∗ exists that enables one to prove that ψ is contradictory. Example 11.2. The following paradigmatic examples of anti-prenex, ∃M-optimized formulae ψ′′ cannot be transformed into explicit contradictions because of condition C1: ∃y1∃y2Fy1y2 ∧ ∀x1¬Fx1x1 6⊢ ∃y1∃y2(Fy1y2 ∧ ¬Fy1y2) (11.1) ∃y1∀x1Fx1x1y1 ∧ ∃y2∀x2¬Fx2y2x2 6⊢ ∃y1∃y2(Fy2y2y1 ∧ ¬Fy2y2y1) (11.2) ∃y1∃y2∀x1∃y3(Fy1x1y3 ∧ ¬Fx1y2y3) 6⊢ ∃y1∃y2∃y3(Fy1y2y3 ∧ ¬Fy1y2y3) (11.3) Formula (8.7) and the following paradigmatic examples of non-contradictory, antiprenex, ∃M-optimized formulae ψ′′ cannot be transformed into explicit contradictions because of condition C2: ∀x1∃y1Fx1y1 ∧ ∀x2Fx2x2 6⊢ ∃y1(Fy1y1 ∧ ¬Fy1y1) (11.4) ∀x1∃y1(Fx1y1 ∧ ∃y2¬Fy2y1) 6⊢ ∃y1∃y2(Fy2y1 ∧ ¬Fy2y1) (11.5) ∀x1∃y1Fx1y1 ∧ ∀x2∃y2¬Fy2x2 6⊢ ∃y1∃y2(Fy2y1 ∧ ¬Fy2y1) (11.6) In each of these cases, no optimal prenex normal form ψ∗ can be generated from the antiprenex, ∃M-optimized formula that would permit the necessary substitutions. 12. Optimized Search for Proofs of Contradiction The decision procedure for subformulae ψ can be used to conduct an optimized search for proofs of contradiction for arbitrary NNFs φ. We presume that φ is transformed into an anti-prenex FOLDNF φ′.8 The single maximally subscripted disjuncts Di of φ ′ can be optimized by deleting literals in Di that are not members of any unifiable pair of literals from Di; for details, cf. Algorithm 13.2. To decide whether a pair of connected literals from Di is unifiable and thus capable of contributing to a proof of contradiction, subformulae ψ are generated. Let Di be an NNF that contains at least two connected literals. Subformulae ψ with exactly two connected literals, L1 and L2, can then be generated from Di as follows: Algorithm 12.1. (1) Delete all literals in φ except L1 and L2. (2) Delete all quantifiers binding variables that do not occur in L1 or L2. (3) Delete all occurrences of ∧ or ∨ except the occurrence that connects L1 and L2 in the logical hierarchy of Di. 8Further optimization is possible by transforming φ into a logically equivalent minimized FOLDNF; cf. [Lampert(2017a)]. 26 LAMPERT (4) If L1 and L2 are connected by ∨, replace ∨ with ∧. Step (4) is justified by the fact that the unification of pairs of literals in proofs of contradiction presumes that the literals are connected by conjunction. This does not imply that the literals are also connected by conjunction in Di. It may well be that proofs of contradiction depend on the multiplication of universally quantified expressions by ∧I to replace the x variables of the multiplied universal quantifier with different y variables (including y0). If the multiplied expression contains ∨, then literals that were connected by ∨ before the application of ∧I are additionally connected by ∧ after the application of ∧I. A proof of contradiction may then depend on the unification of those literals that are connected by ∧ subsequent to the application of ∧I. Example 4.1, p. 7, illustrates this: Subsequent to the application of ∧I, occurrences of Fx1x2x6 and ¬Fx3x1x7 are connected not only by ∨ but also by ∧. Consequently, the derivates Fx12x22x62 and ¬Fx31x11x71 of Fx1x2x6 and ¬Fx3x1x7 are connected not by disjunction but by conjunction subsequent to maximal subscription, and this constitutes the proof of contradiction. In general, a proof of contradiction for a formula φ in accordance with the ∧I-minimal proof strategy in the NNF-calculus is based on transforming φ into a sat-equivalent, optimized FOLDNF φ′ and then specifying, for each disjunct Di in φ ′, (i) an anti-prenex, ∧I-optimized disjunct D∗i ; (ii) a minimal set L of unifiable literals from D ∗ i that are unified in the proof; (iii) a minimal substitution list σ that specifies how each x variable must be replaced with a y variable to unify L; and (iv) an optimal prenex that permits the substitutions necessary according to σ and that can be generated from D∗i . Deciding whether a pair of connected literals in Di is unifiable is equivalent to deciding whether the corresponding subformula ψ is contradictory. Since the latter is decidable by means of Theorem 11.1, the identification of unifiable pairs of literals can be utilized to decide whether certain necessary conditions for a proof of the contradictoriness of Di are satisfied. Theorem 12.2. An NNF φ is not contradictory if the DNF matrix of a Di of the FOLDNF φ′ that is sat-equivalent to φ contains a disjunct that does not contain any unifiable pair of literals. Proof. This theorem follows from the facts that φ is contradictory iff each disjunct Di of φ ′ is contradictory and that any Di is contradictory only if an explicit contradiction can be derived, which requires that each disjunct of the DNF matrix of Di must contain at least one unifiable pair of literals. Thus, a necessary condition for contradiction can be specified with respect to satequivalence transformations to identify formulae that are not contradictory. Independent of the generation of FOLDNFs and DNF matrices, the following can be stated: Theorem 12.3. ∧-NNFs are decidable. Proof. According to Theorem 1.5, a ∧-NNF φ is contradictory iff at least one subformula ψ from φ is contradictory and its contradictoriness is decidable according to Theorem 11.1. Example 12.4. The following formula is not contradictory: ∀x1∃y1Fx1y1 ∧ ∀x2¬Fx2x2 (12.1) A DECISION PROCEDURE FOR HERBRAND FORMULAE 27 This follows from the fact that ψ′′′ contains only the following optimized prenex normal form: ∀x1∃y1∀x2(Fx1y1 ∧ ¬Fx2x2) (12.2) x1 must be replaced with y1 for unification, but C2 of Theorem 11.1 is satisfied. Example 12.5. This example demonstrates how it can be proven that a ∧-NNF is contradictory by deciding upon subformulae ψ: ∀x1∃y2(¬Gy2y2 ∧ ∃y1(∀x3Fy1x1x3 ∧ ∀x2¬Fx2y1y1) ∧Gx1y2) (12.3) Formula (12.3) contains the following two pairs of connected literals: {Gx1y2,¬Gy2y2} and {Fy1x1x3, ¬Fx2y1y1}. ∀x1∃y2(¬Gy2y2 ∧ Gx1y2) is the subformula ψ of the first pair of literals. In this case, ψ = ψ′′, ψ′′′ = {ψ}, and σ = {{x1, y2}}. Hence, C1 is not satisfied. C2, however, is satisfied since φ′′′ does not contain any optimized prenex normal form with ∀x1 in the scope of ∃y2. Therefore, {Gx1y2,¬Gy2y2} is not unifiable. Since both literals do not occur in any other pair of literals from (12.3), these literals can be deleted in formula (12.3) for efficiency in the search for proofs of contradiction. The resulting formula is the subformula ψ of the second pair of literals and is identical to (8.1). The anti-prenex, ∃Moptimized formula ψ′′ is (8.6). σ is unambiguous: {{x1, y12}, {x2, y11}, {x3, y12}} (= σ(8.6)). Therefore, C1 is not satisfied. ψ′′′ contains only one optimized prenex normal form, which is optimal: ∃y12∀x1∃y11∀x3∀x2(Fy11x1x3 ∧ ¬Fx2y12y12) (8.4) Therefore, C2 is also not satisfied. Applying ∀E in accordance with σ(8.6) results in the following explicit contradiction: ∃y11∃y12(Fy11y12y12 ∧ ¬Fy11y12y12) (12.4) Therefore, the pair of literals {Fy1x1x3,¬Fx2y1y1} in (12.3) is unifiable, and consequently, (12.3) is contradictory. 13. Efficient Identification of Unifiable Pairs of Literals The described algorithm for identifying unifiable pairs of literals is cumbersome due to the generation of ψ, ψ′, ψ′′ and ψ′′′. For the deletion of literals that are not members of any pair of unifiable literals in an NNF φ, it would be desirable to instead apply criteria that directly refer to φ, such as in the case of identifying pairs of connected literals. The intention is to specify necessary conditions for unifiable pairs of literals, although these conditions, when taken together, need not be sufficient. The following 3 criteria are necessary conditions for unifiable pairs of literals that directly refer to the syntactic properties of a maximally subscripted NNF φ. They can be justified by the fact that the syntactic properties of φ to which they refer are sufficient for C1 or C2 to be satisfied even after ∃M-optimization and the generation of all optimized prenex normal forms of ψ′′′. C1U1: This criterion checks whether condition C1 (i.e., an ambiguous substitution list σ) is satisfied if the x variables in both of a pair of literals are subscripted differently by using a subscript of -1 in L1 and a subscript of -2 in L2. If the application of Algorithm 9.1 results in an ambiguous substitution list σ under this condition, then C1 will be satisfied even after ∃M-optimization. 28 LAMPERT Example 13.1. This criterion is satisfied if, e.g., an x variable occurs in two positions in one literal and those positions are occupied by different y variables in the other literal; cf. formula (11.1). The criterion is also satisfied if two x variables occur in the same position in both literals and both x variables must be replaced with different y variables due to their occurrences in other positions; cf. formula (11.2). C2U1: This criterion checks whether (i) a universally quantified variable ν1 occurs together with an existentially quantified variable μ in L1 (resp. L2), (ii) ∃μ is in the scope of ∀ν1 in φ (or ψ), (iii) ν1 occupies the same position in L1 (resp. L2) as that of a universally quantified variable ν2 in L2 (resp. L1), and (iv) ν2 occupies the same position in L2 (resp. L1) as that of μ in L1 (resp. L2); cf. formula (11.4). In this case, C2 will be satisfied even after ∃M-optimization and the generation of all optimized prenexes. C3U1: This criterion checks whether (i) a universally quantified x variable ν1 must be replaced with an existentially quantified variable μ2, (ii) a universally quantified x variable ν2 must be replaced with an existentially quantified variable μ1, (iii) ν1 and μ1 occur in one literal while ν2 and μ2 occur in the other literal, and (iv) ∃μ1 is in the scope of ∀ν1 while ∃μ2 is in the scope of ∀ν2 in φ (or ψ); cf. formula (11.6). In this case, C2 will be satisfied even after ∃M-optimization and the generation of all optimized prenexes. Given a set of pairs of connected literals, C1U1-C3U1 enable one to identify a reduced set of pairs of connected literals that is guaranteed to contain all unifiable pairs of literals (= set 1). However, not all pairs of connected literals within this set are necessarily unifiable. To identify all and only unifiable pairs of literals, one must generate the anti-prenex, ∃M-optimized subformula ψ′′ for each pair in set 1 and apply the following criteria: C4U1: This criterion checks whether the substitution list σ of a pair of literals is ambiguous. C5U1: This criterion checks whether σ contains an x list with an x variable ν and a y variable μ such that ∃μ is in the scope of ∀ν in ψ′′. Given ψ′′, C4U1 decides whether C1 is satisfied, and C3U1 and C5U1 decide whether C2 is satisfied. The latter is true because the scopes cannot be minimized any further in ψ′′; cf. Theorem 7.13. Given maximally minimized scopes, only two conditions prevent the generation of optimal prenexes: either ∃μ is in the scope of ∀ν in ψ′′ (case 1), or ψ′′ is of the form . . . (. . . ∀ν1 . . . ∃μ1 . . . A(μ1, ν1) ∧ . . . ∀ν2 . . . ∃μ2 . . . B(μ2, ν2)) (case 2). Case 1 ensures that ∃μ will also be in the scope of ∀ν in any optimized prenex normal form. C5U1 applies to this case. In case 2, any optimized prenex will contain either ∀ν1 to the left of ∃μ2 or ∀ν2 to the left of ∃μ1. Therefore, no optimal prenex exists such that ∃ν1 is to the left of ∀ν2 and ∃ν2 is to the left of ∀ν1. C3U1 applies to this case. In all other cases, however, either ∀ν is already in the scope of the corresponding existential quantifier ∃μ in ψ′′, if ν is to be replaced with μ for unification, or the strategy applied in Algorithm 10.1 of placing existential quantifiers to the left of universal quantifiers if possible will generate an optimal prenex. Therefore, it is sufficient to refer to ψ′′ to decide the unifiability of the pairs in set 1. C3U1 can already be applied to φ or ψ independent of the generation of ψ′′ because ∃M-optimization cannot cause C3U1 to not be satisfied in ψ′′ when it is satisfied in φ or ψ. A DECISION PROCEDURE FOR HERBRAND FORMULAE 29 Hence, it is sufficient to apply criteria C4U1 and C5U1 to the pairs of literals in set 1 to identify the unifiable pairs of literals. Therefore, the following algorithm can be utilized for an optimized proof search by deleting literals in the NNF φ: Algorithm 13.2. (1) Generate the set of all pairs of connected literals from φ. (2) Apply C1U1-C3U1 to this set to minimize it. (3) For each member of this set, generate the subformula φ′′ and apply C4U1 and C5U1 to minimize it. The resulting set A contains all unifiable pairs of literals from φ. (4) Generate a set B consisting of all literals from φ that are not contained in set A. (5) Replace the literals from set B in φ with the expression 'sat'. The result is φ∗. (6) Delete all quantifiers in φ∗ that do not bind a variable that occurs in some literal. The result is φ∗∗. (7) Iteratively apply the following rules from right to left, beginning with φ∗∗, as long as the resulting expression is either 'sat' or no longer contains 'sat': sat ∧A ⊣⊢sat A SAT1 sat ∨A ⊣⊢sat sat SAT2 Table 8: sat Rules The result is φ∗∗∗: a formula that is sat-equivalent to φ and contains no literals that cannot contribute to any proof of contradiction for φ. 14. Outlook Given an anti-prenex FOLDNF with disjuncts Di resulting from Algorithm 13.2 that (i) are not decidable with regard to their contradictoriness by means of Theorem 12.3 because they contain ∨ and (ii) cannot be identified as non-contradictory by means of Theorem 12.2, the question arises of how the contradictoriness of such disjuncts Di can be decided. According to the ∧I-minimal proof strategy, this question boils down to the question of how to compute the minimal number of applications of ∧I necessary to unify a minimal set of unifiable pairs of literals in general. Simple examples such as formula (4.1) show that applications of ∧I are indispensable even if one allows for ∃M.9 However, if a disjunct Di is contradictory, then a ∧I-minimal proof of contradiction for Di in the NNF-calculus is guaranteed to exist. Therefore, it is sufficient to restrict the search for proofs of contradiction to a systematic search for ∧I-minimal proofs. According to the ∧I-minimal proof strategy, the necessary applications of ∧I depend on the following parameters: (1) a minimal set L of pairs of unifiable literals that is sufficient for a proof of contradiction given the unification of its members, (2) a minimal list σ of substitutions that specifies how to replace x variables with y variables to unify the pairs in L, and (3) optimized prenexes ℘ with respect to those quantifiers that bind variables of σ. 9Since applications of ∧I are necessary for proofs of contradiction in general, it is convenient to dispense with ∃M altogether when one is considering general ∧I-minimal proofs of Di in accordance with the ∧Iminimal proof strategy in the NNF-calculus. 30 LAMPERT All alternatives for unifying minimal sets of unifiable pairs of literals through the minimal number of substitutions in relation to all kinds of optimized prenexes must be considered in a systematic search for ∧I-minimal proofs. As soon as a minimal set L with an unambiguous substitution list σ and an optimal prenex ℘ is found, a ∧I-minimal proof for Di has been identified. However, if this does not occur, ∧I must be applied to generate optimal prenexes by stipulating that x variables must be replaced with y0 in addition to other substitutions or to separate x variables. The question is when, in the search for ∧I-minimal proofs, a search path can be abandoned because it is decidable based on purely syntactic criteria that no ∧I-minimal proof can be found along that proof path. A prominent candidate for such a criterion that can be only vaguely specified at this point is as follows: On a certain proof path, as soon as the multiplication of a universally quantified expression through the application of ∧I causes it to be necessary for the universally quantified expression resulting from this multiplication to, in turn, be multiplied by ∧I to achieve similar substitutions of similar unifiable pairs of literals, it can be concluded that such repeated applications of ∧I cannot be a necessary part of a ∧I-minimal proof, and therefore, this proof path can be abandoned. Substitutions and pairs of literals are similar if they are identical in terms of their level-1 indices. Here, we presume that variables are maximally subscripted subsequent to the application of ∧I by increasing the level of their indices by 1; cf. p. 7. The stated conditions can be identified syntactically if one keeps records of all applications of ∧I in which universally quantified expressions are multiplied to unify certain unifiable pairs of literals by means of certain substitutions. I refer to this criterion for abandoning a proof path when applications of ∧I on that proof path induce similar applications of ∧I for similar substitutions in similar unifiable pairs of literals as the 'loop criterion'. For a ∧I-minimal proof strategy, the relevant questions are how to restrict the search for proofs of contradiction to the search for ∧I-minimal proofs and at what point the search for such proofs can finally be abandoned on all proof paths in the case of non-contradictory Di due to a criterion such as the loop criterion. The specific algorithmic definition of a systematic search strategy for ∧I-minimal proofs in fragments of FOL other than ∧INNFs will require further detailed investigation and justification. The intention of this paper was to explain the underlying idea of such a proof search with respect to the most simple example, in which one can dispense with applications of ∧I altogether. This might encourage, for more general fragments of FOL, a search for decision procedures that are analogous to the presented systematic search, which is based on nothing but purely prooftheoretic reasoning, for ∧I-minimal proofs in the NNF-calculus. References [Boerger et al.] Börger, E., Grädel, E. & Gurevich, Y.: The Classical Decision Problem, Springer 2001. [Lampert(2017a)] Lampert, T. 2017: "Minimizing Disjunctive Normal Forms of Pure First-order Logic", Logic Journal of the IGPL 25.3, 325-347. [Lampert(2017b)] Lampert, T. 2017: "Wittgenstein's ab-notation: An Iconic Proof Procedure", History and Philosophy of Logic 38.3, 239-262. [Nonnengart & Weidenbach] Nonnengart, A. & Weidenbach, C.: "Computing small clausal normal forms", in: Robinson, A. & Voronkov, A. (eds.), Handbook of Automated Reasoning I, Elsevier, Amsterdam u.a., 2001, pp. 335-367.