The P and Q Example in Resolution

Claus-Peter Wirth Max Planck Institute for Informatics,

D–66123 Saarbrücken, Germany

   wirth@logic.at

SEKI Working-Paper SWP–2009–03

SEKI Working-Paperhttp://www.dfki.de/seki ISSN 1860-5931

SEKI is published by the following institutions:

German Research Center for Artificial Intelligence (DFKI GmbH), Germany

• Robert Hooke Str. 5, D–28359 Bremen
• Trippstadter Str. 122, D–67663 Kaiserslautern
• Campus D 3 2, D–66123 Saarbrücken

International University of Germany, Campus 1, D–76646 Bruchsal, Germany

Jacobs University Bremen, School of Engineering & Science, Campus Ring 1, D–28759 Bremen, Germany

Universität des Saarlandes, FR 6.2 Informatik, Campus, D–66123 Saarbrücken, Germany

SEKI Editor:

Claus-Peter Wirth

E-mail: wirth@logic.at
WWW: http://www.ags.uni-sb.de/~cp

Please send surface mail exclusively to:

DFKI Bremen GmbH Safe and Secure Cognitive Systems Cartesium Enrique Schmidt Str. 5 D–28359 Bremen Germany

This SEKI Working-Paper was internally reviewed by:

Erica Melis FR Informatik, Universität des Saarlandes, D–66123 Saarbrücken, Germany

E-mail: melis@activemath.org
WWW: http://www.activemath.org/~melis

The P and Q Example in Resolution

Claus-Peter Wirth

Max Planck Institute for Informatics, D–66123 Saarbrücken, Germany

                        wirth@logic.at

July 28, 2009

Abstract

Keywords: Automated Mathematical Induction, Descente Infinie, Resolution Theorem Proving, Higher-Order Logic, Simple Type Theory

1 Introduction

We want to improve the arithmetical power of the higher-order resolution theorem prover Leo-II. Adding the second-order axioms of the specification of the natural numbers either by Peano or by Pieri leads to an explosion of the search space which guarantees that even the most trivial theorems cannot be proved automatically. Thus it is wise to proceed in way that is similar to the one of the first-order inductive theorem provers. As the full strength of the heuristics of the school of explicit induction is available in the descente infinie framework of the inductive theorem prover QuodLibet [Avenhaus &al., 2003], but the historical restrictions of the explicit induction approach are overcome, we want to start by finding out how the fully automated part of QuodLibet can be reimplemented in a framework of refutational resolution and paramodulation.

The P & Q example of [Wirth, 2004, § 3.2.2] is a challenge for the power of mutual induction. Moreover, as it is a toy example, it serves well as a first test case.

2 Why we cannot automate inductive proofs in Leo-II via second-order induction axioms

The straightforward idea on how to realize inductive theorem proving in the arithmetic of natural numbers within a higher-order theorem prover such as Leo-II is just to include the second-order axioms of Guiseppe Peano (1858–1932) or of Mario Pieri (1860–1913) into the specification. Both axioms, however, are not suited for automation because — after eliminating the second-order quantifiers — they result in clauses with a flexible second-order head variable, unifiable with everything of its type.

Peano’s second-order axiom, namely the Axiom of Structural Induction, is pretty useless in practice if we go beyond most trivial structural inductions. This is the case because the required instantiation terms become so complicated, that we do not have any chance to find them, neither by human semantical analysis, nor by automatic generation (unless we use a different calculus for inductive proof search and then translate the results, in which case we had better exchange the calculus right from the start).

Thus, let us have a closer look on Pieri’s second-order axiom, which is more closely related to searching for proofs by mathematical induction. Roughly speaking, in addition to the axiom (nat1) of § 4, Pieri states that the successor relation is well-founded. What we actually need instead of this single relation is the possibility to use a plenitude of wellfounded relations as induction orderings. This means that we will have to apply the Theorem of Noetherian Induction (N):

(N)  ∀P. ( ∀x. P (x) ⇐ ∃<. \binom{∀v. ( P (v) ⇐ ∀u<v. P (u) )}{∧ Wellf(<)} )
(Wellf(<)) ∀Q. ( ∃x. Q(x) ⇒ ∃m. ( Q(m) ∧ ¬∃w<m. Q(w) ) )

Note that the latter line actually contains the definition of its label (Wellf(<)), i.e. of the well-foundedness of the relation <.

If we put (N) into clausal form in an intelligent way,^{1} we get the following two clauses whose conjunction is logically equivalent to (N):

(N′1) P^{δ} (x^{δ} ), ¬Wellf(<^{δ} ), ¬P^{δ} (v^{δ^{+}})
(N′2) P^{δ} (x^{δ} ), ¬Wellf(<^{δ} ), ¬(u^{δ} <^{δ} v^{δ^{+}}), P^{δ} (u^{δ} )

with variable-condition R given by

1First, an equivalence transformation by a δ^{−}-, an α-, two δ^{−}-, an α-step results in the following sequent:

P^{δ} (x^{δ} ), ¬∀v. ( P^{δ} (v) ⇐ ∀u<^{δ} v. P^{δ} (u) ), ¬Wellf(<^{δ} )

Second, the introduction of the fresh free δ^{+}-variable v^{δ^{+}} for the bound γ-variable v results in the sequent

P^{δ} (x^{δ} ), ¬( P^{δ} (v^{δ^{+}}) ⇐ ∀u<^{δ} v^{δ^{+}}. P^{δ} (u) ), ¬Wellf(<^{δ} ), which is equivalent to (N) when we add the variable-condition {P^{δ} , <^{δ} } × {v^{δ^{+}}} and the choice-condition on v^{δ^{+}} mentioned in the text.

Third, a β-step results in the first clause (N′1). Moreover, a δ^{−}-step can introduce the fresh free δ^{−}-vari-able u^{δ} for the bound δ-variable u of the second clause of this β-step; and, followed by an α-step, this results in the clause (N′2).

P^{δ}  _{R}  v^{δ^{+}}_{R} <^{δ}  _{R} u^{δ}

and with choice-condition C given by

C(v^{δ^{+}}) := ¬( P^{δ} (v^{δ^{+}}) ⇐ ∀u<^{δ} v^{δ^{+}}. P^{δ} (u) ).

These clauses say that for showing P^{δ} to be a universal property it suffices (1) to find a well-founded relation <^{δ} , and (2) then there is an object v^{δ^{+}} that is a <^{δ} -minimal counterexample for P^{δ} if such an object exists at all, and it suffices to show that either

(N′1): v^{δ^{+}} is not a counterexample, or

(N′2): there is some u^{δ} <^{δ} v^{δ^{+}} which is a counterexample.

Note that this is not a contradictio in eo ipso: It simply says that P^{δ} is a universal property if there is no <^{δ} -minimal counterexample.

The two clauses can be more easily understood if we consider the case that P^{δ} is not a universal property. Then, for a well-founded ordering <^{δ} , clause (N′1) says that v^{δ^{+}} is indeed a counterexample and clause (N′2) says that it is indeed minimal in this aspect; i.e. that the choice-condition can be actually met.

Though the choice-condition may be beneficial in theorem proving (cf. [Wirth, 2008]), it is actually redundant. Let us forget it and switch to a raised (i.e. dually Skolemized, cf. [Miller, 1992]) version of the clauses:

(N′′1) P^{δ} (x^{δ} ), ¬Wellf(<^{δ} ), ¬P^{δ} (v(P^{δ} , <^{δ} ))
(N′′2) P^{δ} (x^{δ} ), ¬Wellf(<^{δ} ), ¬(u^{δ} <^{δ} v(P^{δ} , <^{δ} )), P^{δ} (u^{δ} )

For a successful resolution proof we will have to instantiate P^{δ} and <^{δ} with the same terms in both clauses, respectively. The term P^{δ} (x^{δ} ), however, admits unification with any predicate of the language, so any straightforward automation gets lost in intractability.

3 The P & Q Example in QuodLibet

The toy example of this § 3 illustrates how mutual induction works in the descente infinie framework of QuodLibet. As the proof requires mutual induction with non-trivial weights, it cannot be performed in many inductive theorem proving systems, nor in the lean induction calculus of [Baaz &al., 1997].

In this § 3, it is not our aim to explain the good reasons for the design decisions and features of the QuodLibet system, but just to present the ones relevant here ad hoc. Moreover, we will hide those of the representational improvements of the QuodLibet system aiming at user interaction which will not be part of the first step of the realization of induction in Leo-II, which is the only subject of this paper. This is especially the case for the special constructor variables of the QuodLibet system. For a more human-oriented presentation of the P & Q Example including constructor variables cf. [Wirth, 2004, § 3.2].

We use zero 0 : nat and successor s : nat → nat as constructors for the type nat. In Quod-Libet we would declare the two symbols as the only constructors of the sort nat. In our more less specialized context here, however, we explicitly have to provide the definition of the definedness predicate that singles out those elements of the sort nat that actually are natural numbers and no error elements.

(Defnat1)  Def(0)
(Defnat2) ∀X. ( Def(s(X)) ⇐ Def(X) )
(nat1)  ∀X. ( (X=0 ∨ ∃Y. (X=s(Y) ∧ Def(Y))) ⇐ Def(X) )

This basic signature is enriched with the predicates P : nat → bool, Q : nat → nat → bool.

We have the following axioms, defining the special predicates of our example.

(P1)  P(0)
(P2) ∀X. ( P(s(X)) ⇐ ( P(X) ∧ Q(X, s(X)) ∧ Def(X) ) )

(Q1)  ∀X. ( Q(X, 0) ⇐ Def(X) )
(Q2) ∀X, Y. ( Q(X, s(Y)) ⇐ ( Q(X, Y) ∧ P(X) ∧ Def(X) ∧ Def(Y) ) )

A sequent is a disjunctive list of formulas; in concrete examples we will write the list separated by commas. In its most simple form to be considered here, a weighted sequent is a pair of a sequent and a weight term; we will always separate the weight from the sequent with a semicolon.

We now want to show that both predicates are tautological on the actual natural numbers. In the form of a weighted sequent (actually a weighted clause because all listed formulas are literals) this reads:

(1)  P(X0^{δ} ), ¬Def(X0^{δ} ); w1^{γ}(X0^{δ} )
(2)  Q(Y0^{δ} , Z0^{δ} ), ¬Def(Y0^{δ} ), ¬Def(Z0^{δ} ); w2^{γ}(Y0^{δ} , Z0^{δ} )

Note that our weights here consist only of weight terms (such as w1^{γ}(X0^{δ} ) in (1)), but not of additional induction orderings and quasi-orderings, because we fix these orderings to be the single one of the QuodLibet system, as discussed in [Wirth, 2004, § 3.2.1].^{2}

In the Hypothesizing steps for (1) and (2) we introduce the variable-condition

R := \binom{V_{γδ^{+}}((1)) × V_{δ} ((1))}{∪ V_{γδ^{+}}((2)) × V_{δ} ((2))} = \binom{\{w1^{γ}\} × \{X0^{δ} \}}{∪ \{w3^{γ}\} × \{Y0^{δ} , Z0^{δ} \}}

to have all free δ^{−}-variables of (1) or (2) in the set Y of Theorem 2.51 of [Wirth, 2004], so that we can locally instantiate all of them with whatever we want in each application of (1) or (2) as a lemma or as an induction hypothesis.

After several inference steps, QuodLibet presents a sequent tree for (1), which is — mutatis mutandis — similar to following:

2Therefore — as discussed in [Wirth, 2004, § 2.5] — the items (3)–(6) of Theorem 2.51 of [Wirth, 2004] can be omitted in all lemma and hypothesis applications in the following.

(1) P(X0^{δ} ), ¬Def(X0^{δ} ); w1^{γ}(X0^{δ} )

(nat1), γ, β, δ^{−}, Rewrite^{+}

(1.1) P(0), ¬Def(0); w1^{γ}(0)

(1.2) P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

(P1) (P2), γ, β, β

(1.2.1) P(X1^{δ} ), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

(1.2.2) Q(X1^{δ} , s(X1^{δ} )), ¬P(X1^{δ} ), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

induction-hypothesis appl. of

(1){X0^{δ} ↦X1^{δ} }

induction hypothesis application of

(2){Y0^{δ} ↦X1^{δ} , Z0^{δ} ↦s(X1^{δ} )}

(1.2.1.1) w1^{γ}(X1^{δ} )<w1^{γ}(s(X1^{δ} )), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

(1.2.2.1) w2^{γ}(X1^{δ} , s(X1^{δ} ))<w1^{γ}(s(X1^{δ} )), Q(X1^{δ} , s(X1^{δ} )), ¬P(X1^{δ} ), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

The square boxes are the nodes of the proof tree, whereas the round-edged boxes show applications of inference rules of Theorems 2.49 and 2.51 of [Wirth, 2004], which are more elementary than the inference rules in QuodLibet. We can check whether the tree is closed simply by checking whether all leaves are round-edged nodes. This is not only useful for implementation purposes (where we have to record why a branch is closed) but also immediately realizes the explicit representation of leaves required by Definition 2.42 of [Wirth, 2004].

For example, “ (nat1), γ, β, δ^{−}, Rewrite^{+} ” in the first round-edged box means that we use the axiom (nat1) as a lemma in Theorem 2.51 of [Wirth, 2004], and then apply a γ-, a β-, a δ^{−}-step, and several Rewrite-steps of Theorem 2.49 of [Wirth, 2004] to get the nodes (1.1) and (1.2). This means that, by application of (nat1),

(1) P(X0^{δ} ), ¬Def(X0^{δ} ); w1^{γ}(X0^{δ} )

reduces to the following two sequences^{3}

(1.1) P(0), ¬Def(0); w1^{γ}(0)

(1.2) P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

with the additional variable-condition of {(X0^{δ} , X1^{δ} )}.

Now (1.1) is subsumed by (P1).

Moreover, applying (P2) to (1.2) we get the following two clauses:

(1.2.1) P(X1^{δ} ), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} )) (1.2.2) Q(X1^{δ} , s(X1^{δ} )), ¬P(X1^{δ} ), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

Applying (1) to (1.2.1) as an induction hypothesis, instantiated via {X0^{δ} ↦X1^{δ} }, results in

(1.2.1.1) w1^{γ}(X1^{δ} )<w1^{γ}(s(X1^{δ} )), P(X1^{δ} ), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

Applying (2) to (1.2.2) as an induction hypothesis, instantiated via {Y0^{δ^{+}}↦X1^{δ^{+}}, Z0^{δ^{+}}↦s(X1^{δ^{+}})}, results in^{4}

(1.2.2.1) w2^{γ}(X1^{δ} , s(X1^{δ} ))<w1^{γ}(s(X1^{δ} )),

Q(X1^{δ} , s(X1^{δ} )), ¬P(X1^{δ} ), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

(1.1′) X0^{δ} ≠ 0, P(X0^{δ} ), ¬Def(X0^{δ} ); w1^{γ}(X0^{δ} )

(1.2′) X0^{δ} ≠ s(X1^{δ} ), P(X0^{δ} ), ¬Def(X1^{δ} ), ¬Def(X0^{δ} ); w1^{γ}(X0^{δ} )

(1.1′′) X0^{δ} ≠ 0, P(0), ¬Def(0); w1^{γ}(0)

Φ := Q(Y0^{δ} , Z0^{δ} )
ℸ := w2^{γ}(Y0^{δ} , Z0^{δ} )
Y := {Y0^{δ} , Z0^{δ} }
ϱ := {Y0^{δ} ↦X1^{δ} , Z0^{δ} ↦s(X1^{δ} )}
M := {¬Q(X1^{δ} , s(X1^{δ} )), Def(X1^{δ} ), Def(s(X1^{δ} )), w2^{γ}(X1^{δ} , s(X1^{δ} ))<w1^{γ}(s(X1^{δ} ))}

3Let us have a look at this step in more detail. After applying the substitution {X↦X0^{δ} } in a γ-step, a β-step and a δ^{−}-step (introducing X1^{δ} ) leave us with the following two cases:

and the additional variable-condition of {(X0^{δ} , X1^{δ} )}. Contextual rewriting with the head literals results in (1.2′′) X0^{δ} ≠ s(X1^{δ} ), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

Now X0^{δ} is in solved form (cf. Definition 3.1) in both clauses, so removing the literal containing it is an equivalence transformation.

Definition 3.1 (Solved Form)

x^{δ} ∈ V_{δ} is in solved form in the weighted sequent Γ (x^{δ} ≠t) Π; ℶ if x^{δ} ∉ V(t, Γ Π, ℶ) and V_{γδ^{+}}(t, Γ Π, ℶ) ⊆ R^{+}⟨{x^{δ} }⟩.

4Let us have a closer look on what happens below (1.2.2). We instantiate the meta-variables of Theorem 2.51 of [Wirth, 2004] as follows:

For (2) we get a sequent tree very similar to that of (1):

(2) \begin{matrix}Q(Y0^{δ} , Z0^{δ} ), ¬Def(Y0^{δ} ), \\ ¬Def(Z0^{δ} ); w2^{γ}(Y0^{δ} , Z0^{δ} ) \end{matrix} (nat1), γ, β, δ^{−}, Rewrite^{+}_{(2.1) \begin{matrix}Q(Y0^{δ} , 0), ¬Def(Y0^{δ} ), \\ ¬Def(0); w2^{γ}(Y0^{δ} , 0) \end{matrix}}  _{(2.2) Q(Y0^{δ} , s(Z1^{δ} )), ¬Def(Z1^{δ} ), ¬Def(Y0^{δ} ), ¬Def(s(Z1^{δ} )); w2^{γ}(Y0^{δ} , s(Z1^{δ} ))} (Q1)  (Q2), γ, β, β, β_{(2.2.1) Q(Y0^{δ} , Z1^{δ} ), Q(Y0^{δ} , s(Z1^{δ} )), ¬Def(Z1^{δ} ), ¬Def(Y0^{δ} ), ¬Def(s(Z1^{δ} )); w2^{γ}(Y0^{δ} , s(Z1^{δ} ))}  _{(2.2.2) P(Y0^{δ} ), ¬Q(Y0^{δ} , Z1^{δ} ), Q(Y0^{δ} , s(Z1^{δ} )), ¬Def(Z1^{δ} ), ¬Def(Y0^{δ} ), ¬Def(s(Z1^{δ} )); w2^{γ}(Y0^{δ} , s(Z1^{δ} ))} ind.-hyp. appl. of (2)\{Z0^{δ} ↦Z1^{δ} \}  ind.-hyp. appl. of (1)\{X0^{δ} ↦Y0^{δ} \}_{(2.2.1.1) w2^{γ}(Y0^{δ} , Z1^{δ} )<w2^{γ}(Y0^{δ} , s(Z1^{δ} )), Q(Y0^{δ} , Z1^{δ} ), Q(Y0^{δ} , s(Z1^{δ} )), ¬Def(Z1^{δ} ), ¬Def(Y0^{δ} ), ¬Def(s(Z1^{δ} )); w2^{γ}(Y0^{δ} , s(Z1^{δ} ))}  _{(2.2.2.1) w2^{γ}(Y0^{δ} )<w2^{γ}(Y0^{δ} , s(Z1^{δ} )), P(Y0^{δ} ), ¬Q(Y0^{δ} , Z1^{δ} ), Q(Y0^{δ} , s(Z1^{δ} )), ¬Def(Z1^{δ} ), ¬Def(Y0^{δ} ), ¬Def(s(Z1^{δ} )); w2^{γ}(Y0^{δ} , s(Z1^{δ} ))}

We have applied each of the two weighted sequents (1) and (2) in each of their two proof trees. Luckily we used induction hypothesis application instead of lemma application: The latter would have resulted in a lemma application relation of {1, 2} × {1, 2} which is not well-founded and our proof trees would have been useless because we would never be able to apply Theorem 2.45 of [Wirth, 2004]. As we have used induction hypothesis application instead of lemma application, we have produced the four additional leaves (1.2.1.1), (1.2.2.1), (2.2.1.1), and (2.2.2.1), which are still open. We choose our 2^{nd} order weight functions according to w1^{γ}(X) := (X) and w2^{γ}(X, Y) := (X, Y), or — more precisely — by applying the substitution { w1^{γ}↦λX. (X), w2^{γ}↦λX, Y. (X, Y) } and by λβ-reduction, using the lexicographic combination of [Wirth, 2004, § 3.2.1], explained below.

Now the proof attempt can be successfully completed: For example, the weighted sequent (1.2.1.1) turns into

(1.2.1.1′) (X1^{δ} )<(s(X1^{δ} )), P(X1^{δ} ), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

which is equivalent to

(1.2.1.1′.1) X1^{δ} <s(X1^{δ} ), P(X1^{δ} ), P(s(X1^{δ} )), ¬Def(X1^{δ} ), ¬Def(s(X1^{δ} )); w1^{γ}(s(X1^{δ} ))

which again is subsumed by one of QuodLibet’s ordering axioms.

QuodLibet realizes a version of the semantic length ordering, cf. e.g. [Kühler & Wirth, 1996]. Thus, any clause of the form

t<t′, Γ

is a valid axiom provided that each of the following items holds:

1. Each constant symbol occurring in t, t′ is a constructor symbol.

2. Each variable X occurring in t, t′ satisfies the following:

(a) X is of a basic type inductively defined via constructors, and

(b) Γ contains a literal of the form ¬Def(X).

3. No variable occurs more often in t than in t′.

4. The number of symbol occurrences in t is strictly less than the number of symbol occurrences in t′.

Besides that, QuodLibet has an additional sort for the lexicographic combination of this ordering into an ordering over tuples of its domain of arbitrary length. Note that, as any completed proof will be a finite object, there is a maximum length m of the tuples of this additinal sort occurring in it. And the lexicographic combination up to the length m of well-founded orderings (such as the semantic length ordering in our context) is well-founded again. Also note, that this is not generally the case:

(s(0)) > (0, s(0)) > (0, 0, s(0)) > . . ..

All in all, as the induction orderings of our proofs must be well-founded, this means that term formation over the additional sort for the lexicographic combination must be restricted; for instance, the formation of a term representing the 0^{n} s(0) of the above example must be excluded.

The axioms of the lexicographic combination can then easily be formalized, although special heuristic treatment might be necessary for efficiency of automation: Let () denote the empty tuple, let X denote an element of the basic types defined via constructors, and let L be an element of the additional type for tuples.

()<(X, L)
(X, L)<(X′, L′) ⇔ if X=X′ then L<L′ else X<X′ fi
L≮()

Which steps in this proof were typical for inductive theorem proving in the sense that their soundness relies on notions of inductive validity instead of the stronger notion of validity in all models?

Besides the four induction hypothesis applications, the final branch closure rules for <-literals are typical for induction because they require that, in all models in the class K of models to be considered for inductive validity, the successor of each natural number is different from that natural number and each natural number is built-up from zero by a finite number of successor steps (i.e. there are neither cycles nor Z-chains in the models, cf. [Enderton, 1972]).

4 How we hope to automate such proofs in Leo-II

Let us see whether we have a chance to automate the proof of § 3 in Leo-II.

Note that both

• the generative proof style (performing deduction steps) of resolution (instead of the primarily analytic style of QuodLibet; performing reduction steps similar to tableau, sequent, or matrix calculi) as well as

• the refutational aspect of refutational resolution (used in Leo-II as in practically all resolution theorem provers for the sake of goal-directedness)

render Leo-II — on the first sight at least — less suited for inductive theorem proving than QuodLibet.

As a first step for our proof in Leo-II, just as in QuodLibet, we have to apply a heuristics called recursion analysis, going back to the school of explicit induction, cf. [Boyer & Moore, 1979], [Walther, 1994], [Bundy, 1999]. We will take the code for this out of the code for recursion analysis in Qml (QuodLibet Meta Language). In our concrete example, recursion analysis will tell us that

• to prove (1), it is a good idea consider the proof tasks (1.2.1) and (1.2.2); i.e. to search for a proof of (1.2.1) and (1.2.2) that is closed up to the application of induction hypotheses; and

• to prove (2), it is a good idea to consider the proof tasks (2.2.1) and (2.2.2).

In the jargon of explicit induction these four proof tasks are called induction step cases.

These four proof tasks cannot be executed successfully without (1) and (2) being available as induction hypotheses. Thus, we have to provide Leo-II with clauses such as

(1hyp) P(X0^{δ} ), ¬Def(X0^{δ} ), w1^{γ}(X0^{δ} )≮W0^{δ} ; (W0^{δ} , T0^{δ} )

and

(2hyp) Q(Y0^{δ} , Z0^{δ} ), ¬Def(Y0^{δ} ), ¬Def(Z0^{δ} ), w2^{γ}(Y0^{δ} , Z0^{δ} )≮W1^{δ} ; (W1^{δ} , T1^{δ} )

Herein any

; (Wi^{δ} , Ti^{δ} )

now does not stand for the augmentation of the clause with a weight term as in QuodLibet, but for a clausal constraint in Leo-II. More precisely:

1. Any free δ^{−}-variable Ti^{δ} stands for the proof tasks to which the clause may contribute. Note that will have to prove several proof tasks (actually induction step cases) in parallel; and we need an independent refutation proof for any of these cases, which is complete up to induction hypotheses application.

2. The free δ^{−}-variable Wi^{δ} serves to transfer the weight of such a proof task into the right-hand side of the <-condition literal of the clause and its resolvent. Thus, in any resolution or paramodulation step, where one such constraint is present, this constraint must be inherited; and in any step where several such constraints are present, these constraints must be unified and inherited.

This part of the problem solved, to prove the four open goals mentioned above, Leo-II has to negate them and to derive a refutation. Let us see, how (1.2.1) would look like after negation: Luckily, we have w1^{γ}R^{+}X1^{δ} . This means that (1.2.1) is logically equivalent to

(1.2.1)′ P(X1^{δ^{+}}) ∨ P(s(X1^{δ^{+}})) ∨ ¬Def(X1^{δ^{+}}) ∨ ¬Def(s(X1^{δ^{+}})); (w1^{γ}(s(X1^{δ^{+}})), (1.2.1)′)

with choice-condition

C(X1^{δ^{+}}) := ¬( P(X1^{δ^{+}}) ∨ P(s(X1^{δ^{+}})) ∨ ¬Def(X1^{δ^{+}}) ∨ ¬Def(s(X1^{δ^{+}})) )

Note that the free δ^{−}-variable X1^{δ} has been replaced with the fresh free δ^{+}-variable X1^{δ^{+}} in a δ^{+}-step, which can either be seen as Skolemization or better as an application of the axiom (ε_{0}) on Hilbert’s ε; cf. [Wirth, 2008].

Now, (1.2.1)′ can easily be negated, resulting in the clauses:

¬P(X1^{δ^{+}}); (w1^{γ}(s(X1^{δ^{+}})), (1.2.1)′)

¬P(s(X1^{δ^{+}})); (w1^{γ}(s(X1^{δ^{+}})), (1.2.1)′)

Def(X1^{δ^{+}}); (w1^{γ}(s(X1^{δ^{+}})), (1.2.1)′)
Def(s(X1^{δ^{+}})); (w1^{γ}(s(X1^{δ^{+}})), (1.2.1)′)

Resolving the first one with (1hyp) results in

¬Def(X0^{δ^{+}}), w1^{γ}(X0^{δ^{+}})≮w1^{γ}(s(X1^{δ^{+}})); (w1^{γ}(s(X1^{δ^{+}})), (1.2.1)′)

and resolving this with the third one results in

w1^{γ}(X0^{δ^{+}})≮w1^{γ}(s(X1^{δ^{+}})); (w1^{γ}(s(X1^{δ^{+}})), (1.2.1)′)

5 Important Aspects

Why does this work? Induction always takes place only on the outermost universal variables. In the free variable framework of [Wirth, 2004; 2008], these are those free δ^{−}-variables X^{δ} of a sequent Γ that satisfy w^{γ}R^{+}X^{δ} for each w^{γ} ∈ V_{γ}(Γ), where R denotes the current variable-condition. Replacing these variables with free δ^{+}-variables with the appropriate variable-condition and choice-condition is an equivalence transformation. Assuming that no other free δ^{+}-variables occur in γ, we can negate this easily.

Note that our negation of the conjecture does not take place on top level, i.e. we do not state that the conjecture is (C, R)-invalid in all structures A ∈ K, but only that, for some A ∈ K and some (A, R)-valuation e and for some π that is (e, A)-compatible with (C, R), the conjecture is not (π, e, A)-valid. Thus, if we can derive the empty clause by resolution, we know that this cannot be the case w.r.t. to the information gathered in the meanwhile in the variable-condition R, the choice-condition C, via instantiation of rigid variables.

Thus, although it is a good idea for heuristic propagation to let the several refutations run in parallel, they communicate their results via the rigid variables.

Thus, if one refutation instantiates w1^{γ}, this will become visible to all the other refutations carrying the proof debt for our mutual induction.

References

[Avenhaus &al., 2003] Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, and Claus-Peter Wirth. How to prove inductive theorems? QuodLibet! In 19^{th} Int. Conf. on Automated Deduction, Miami Beach (FL), 2003, number 2741 in Lecture Notes in Artificial Intelligence, pages 328–333. Springer, 2003. http://www.ags.uni-sb.de/~cp/

p/quodlibet.

[Baaz &al., 1997] Matthias Baaz, Uwe Egly, and Christian G. Fermüller. Lean induction principles for tableaus. In Didier Galmiche, editor, 6^{th} Int. Conf. on Tableaus and Related Methods, Pont-à-Mousson (France), 1997, number 1227 in Lecture Notes in Artificial Intelligence, pages 62–75. Springer, 1997.

[Boyer & Moore, 1979] Robert S. Boyer and J S. Moore. A Computational Logic. Academic Press (Elsevier), 1979.

[Bundy, 1999] Alan Bundy. The Automation of Proof by Mathematical Induction. Informatics Research Report No. 2, Division of Informatics, Univ. Edinburgh, 1999. Also in [Robinson & Voronkow, 2001, Vol. 1, pp. 845–911].

[Enderton, 1972] Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press (Elsevier), 1972.

[Gabbay &al., 1994] Dov Gabbay, Christopher John Hogger, and J. Alan Robinson, editors. Handbook of Logic in Artificial Intelligence and Logic Programming. Vol. 2: Deduction Methodologies. Oxford Univ. Press, 1994.

[Kühler & Wirth, 1996] Ulrich Kühler and Claus-Peter Wirth. Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. SEKI-Report SR–1996–11 (ISSN 1437–4447). SEKI Publications, Univ. Kaiserslautern, 1996. Short version in 8^{th} RTA 1997, LNCS 1232, pp. 38–52, Springer. http:

//www.ags.uni-sb.de/~cp/p/rta97.

[Miller, 1992] Dale A. Miller. Unification under a mixed prefix. J. Symbolic Computation, 14:321–358, 1992.

[Robinson & Voronkow, 2001] Alan Robinson and Andrei Voronkow, editors. Handbook of Automated Reasoning. Elsevier, 2001.

[Walther, 1994] Christoph Walther. Mathematical induction. 1994. In [Gabbay &al., 1994, pp. 127–228].

[Wirth, 2004] Claus-Peter Wirth. Descente Infinie + Deduction. Logic J. of the IGPL,

12:1–96, 2004. http://www.ags.uni-sb.de/~cp/p/d.

[Wirth, 2008] Claus-Peter Wirth. Hilbert’s epsilon as an operator of indefinite committed choice. J. Applied Logic, 6:287–317, 2008. http://www.ags.uni-sb.de/~cp/p/epsi,

http://dx.doi.org/10.1016/j.jal.2007.07.009.