Full First-Order Free Variable Sequents and Tableaux in Implicit Induction

Claus-Peter Wirth

FR Informatik, Saarland Univ., D–66041 Saarbrücken, Germany

                             cp@ags.uni-sb.de

Abstract. We show how to integrate implicit inductive theorem proving into free variable sequent and tableau calculi and compare the appropriateness of tableau calculi for this integration with that of sequent calculi.

When first-order validity is introduced to students it comes with some complete calculus. If this calculus happens to be an analytic calculus augmented with a Cut rule like a sequent or tableau calculus the students can compare the formal proofs with the informal ones they are hopefully acquainted with. This is because these calculi can mirror the human proof search process better than others. While knowing a complete calculus does not mean to know much about first-order theorem proving, the interrelation of a human-oriented calculus and the informal proof search of the students will turn out to be fruitful for their later mathematical work. It is a pity that—while nearly all proofs of a working mathematician include induction—nothing comparable for inductive first-order validity is offered to the students. Some may argue that this is generally impossible because not even the theory of the Peano algebra of natural numbers is recursively enumerable, cf. e.g. Enderton (1973). Nevertheless, there really is some general way a working mathematician searches for an informal proof, may it be inductive or not. The inductive version of this proof search method goes back to the ancient Greeks and was rediscovered under the name “descente infinie” by Pierre de Fermat (1601-1665). If you want to prove a conjecture, this method requires that you show, for each assumed counterexample of the conjecture, the existence of another counterexample of the conjecture that is strictly smaller in some wellfounded ordering. The working mathematician applies it in the following fashion. He (who may be female!) starts with the conjecture and simplifies it in case analyses which can be described as steps in a sequent or tableau calculus with Cut. When he realizes that the goals become similar to a different instance of the conjecture, he applies the conjecture just like a lemma, but keeps in mind that he actually has applied some induction hypothesis. Finally, he searches for some wellfounded ordering in which all the instances of the conjecture that he has applied as induction hypotheses are smaller than the original conjecture itself. Looking for a formal inductive calculus for mirroring this style of human inductive theorem proving (ITP), the “implicit induction” of Bachmair (1988) was a starting point because it included hypothesis application, although it was restricted to universally quantified pure equations and was not human-oriented. In Wirth (1997) we have presented a human-oriented inductive calculus for universally quantified clausal logic. In Kühler (1999)—implemented as the QuodLibet system—this calculus is extended with some necessary and important concretion for reasoning on the induction ordering and with a tacticbased concept for proof guidance that is intended to partially automate the construction of proofs. Extending this approach to full first-order logic turned out to be more difficult than expected (cf., however, Padawitz (1996) for the extension to another interesting sub-class): The state-of-the-art free variable analytic first-order calculi were not suited for the integration of “implicit induction” because they confused the Herbrand universes with their Skolem functions and did not preserve solutions (i.e. closing substitutions) (like Prolog does), thereby destroying the wellfoundedness of “descente infinie”. In Wirth (1998) we have developed sequent and tableau calculi for full first-order formulas that do not Skolemize but do preserve solutions. These new calculi come in two versions. The weak version is simple, but cannot model liberalized versions of the δ-rule, which the strong version can. Since the strong version is much more complicated, the space is limited here, and many researchers today are quite unacquainted with “descente infinie”, in this paper we will use the weak version only and concentrate on the inductive aspects (i.e. induction hypothesis application) and not on the deductive ones (i.e. α-, β-, γ-, and δ-steps, cf. Smullyan (1968)). Even for the experts in implicit ITP each of the following aspects will be new: Tableau presentation, full first-order formulas, and free variables.

We use ‘⊎’ for the union of disjoint classes and ‘id’ for the identity function. For a class R we define domain, range, restriction to, image and reverse-image of a class A by dom(R) := { a | ∃b. (a, b) ∈ R }; ran(R) := { b | ∃a. (a, b) ∈ R }; A↿R := { (a, b) ∈ R | a ∈ A}; ⟨A⟩R := { b | ∃a ∈ A. (a, b) ∈ R}; R⟨B⟩ := { a | ∃b ∈ B. (a, b) ∈ R}. ‘N’ denotes the set of and ‘≺’ the ordering on natural numbers. We use ‘∅’ to denote the empty set as well as the empty function or empty word. A quasi-ordering ‘≲’ on A is an A-reflexive and transitive (binary) relation on A. As with all our asymmetric relation symbols we define a≳b if b≲a. By an (irreflexive) ordering ‘<’ (on A) we mean an irreflexive and transitive relation (on A). The ordering < of a quasi-ordering ≲ is ≲\≳. A quasi-ordering ≲ is called total on C if C×C ⊆ ≲ ∪ ≳. A ≲-chain is some subclass C ⊆ A such that ≲ is total on C. ≲ is called wellfounded if each ≲-chain C has a least element, i.e. ∃a ∈ C. ∀b ∈ C. a≲b. The class of total functions from A to B is denoted with A → B. The class of (possibly) partial functions from A to B is denoted with A ⇝ B.

We define a sequent to be a list of formulas. The conjugate of a formula A (written: \overline{A} ) is the formula B if A is of the form ¬B, and the formula ¬A otherwise. In the tradition of Gentzen (1935) we assume the symbols for free existential variables (i.e. the free variables of Fitting (1996)), free universal variables (i.e. nullary parameters), bound variables (i.e. variables for quantified use only), and the constants (i.e. the function (and predicate) symbols from the signature) to come from four disjoint sets V_{∃}, V_{∀}, V_{bound}, and Σ. We assume each of V_{∃}, V_{∀}, V_{bound} to be infinite (for each sort) and set V_{free} := V_{∃}⊎V_{∀}. For a term, formula, sequent Γ &c., ‘V_{∃}(Γ)’, ‘V_{∀}(Γ)’, ‘V_{bound}(Γ)’, ‘V_{free}(Γ)’ denote the sets of variables from V_{∃}, V_{∀}, V_{bound}, V_{free} occurring in Γ, resp.. For a substitution σ we denote with ‘Γ σ’ the result of replacing in Γ each variable x in dom(σ) with σ(x). We tacitly assume that each substitution σ satisfies V_{bound}(dom(σ) ∪ ran(σ))

= ∅, such that no bound variables can be replaced and no additional variables become bound (i.e. captured) when applying σ.

A variable-condition R is a subset of V_{∃}×V_{∀}. Roughly speaking, (x^{∃}, y^{∀}) ∈ R says that x^{∃} is older than y^{∀}, so that we must not instantiate the free existential variable x^{∃} with a term containing y^{∀}.

Validity is expected to be given with respect to some Σ-structure (Σ-algebra) A, assigning a universe (to each sort) and an appropriate function to each symbol in Σ. For X ⊆ V_{free} we denote the set of total A-valuations of X (i.e. functions mapping free variables to objects of the universe of A (respecting sorts)) with X → A and the set of (possibly) partial A-valuations of X with X ⇝ A. For π ∈ X → A we denote with ‘A⊎π’ the extension of A to the variables of X which are then treated as nullary constants. More precisely, we assume the existence of some evaluation function ‘eval’ such that eval(A⊎π) maps any term over Σ⊎X into the universe of A (respecting sorts) such that for all x ∈ X: eval(A⊎π)(x) = π(x). Moreover, eval(A⊎π) maps any formula B over Σ⊎X to TRUE or FALSE, such that B is valid in A⊎π iff eval(A⊎π)(B) = TRUE. We assume that the Substitution-Lemma holds in the sense that, for any substitution σ, Σ-structure A, valuation π ∈ V_{free} → A, and term or formula B: eval(A⊎π)(Bσ) = eval( A ⊎ ( ( σ ⊎ _{V_{free}\dom(σ)}↿id ) ∘ eval(A⊎π) ) )( B ). Finally, we assume that the value of the evaluation function on a term or formula B does not depend on the free variables that do not occur in B:

eval(A⊎π)(B) = eval(A ⊎ _{V_{free}(B)}↿π)(B).

Further properties of validity or evaluation are definitely not needed.

We are now going to briefly recapitulate the notions from the weak version of Wirth (1998) which we need in what follows. Several binary relations on free variables will be introduced. The overall idea is that when (x, y) occurs in such a relation this means something like “x is older than y” or “the value of y depends on or is described in terms of x”.

Definition 0.1 (E_{σ}, U_{σ}, Existential R-Substitution, σ-Update) For a substitution σ with dom(σ) = V_{∃} we define the existential relation to be E_{σ} := { (x′, x) | x′ ∈ V_{∃}(σ(x)) ∧ x ∈ V_{∃} } and the universal relation to be U_{σ} := { (y, x) | y ∈ V_{∀}(σ(x)) ∧ x ∈ V_{∃} }. Let R be a variable-condition. σ is an existential R-substitution if σ is a substitution with dom(σ) = V_{∃} for which U_{σ} ∘ R is irreflexive. Let σ be an existential R-substitution. The σ-update of R is E_{σ} ∘ R.

Note that, regarding syntax, (x^{∃}, y^{∀}) ∈ R is intended to mean that an existential R-substitution σ may not replace x^{∃} with a term in which y^{∀} occurs, i.e. (y^{∀}, x^{∃}) ∈ U_{σ} must be disallowed, i.e. U_{σ}∘R must be irreflexive.

After application of an existential R-substitution σ, in case of (x^{∃}, y^{∀}) ∈ R, we have to ensure that x^{∃} is not replaced with y^{∀} via a future application of another existential R-substitution that replaces a free existential variable u^{∃} occurring in σ(x^{∃}) with y^{∀}. In this case, the new variable-condition has to contain (u^{∃}, y^{∀}). This means that E_{σ}∘R must be a subset of the updated variablecondition.

Let A be some Σ-structure. We now define a semantic counterpart of our existential R-substitutions, which we will call “existential (A, R)-valuation”. Suppose that e maps each free existential variable not directly to an object of A (of the same sort), but can additionally read the values of some free universal variables under an A-valuation π ∈ V_{∀} → A, i.e. e gets some π′ ∈ V_{∀} ⇝ A with π′⊆π as a second argument; short: e : V_{∃} → ((V_{∀} ⇝ A) → A). Moreover, for each free existential variable x, we require the set of read free universal variables (i.e. dom(π′)) to be identical for all π; i.e. there has to be some “semantic relation” S_{e} ⊆ V_{∀}×V_{∃} such that for all x ∈ V_{∃}: e(x) : (S_{e}⟨{x}⟩ → A) → A. Note that, for each e, at most one semantic relation exists, namely

S_{e} := { (y, x) | y ∈ dom(⋃ (dom(e(x)))) ∧ x ∈ V_{∃} }.

Definition 0.2 (S_{e}, Existential (A, R)-Valuation, ϵ) Let R be a variable-condition, A a Σ-structure, and e : V_{∃} → ((V_{∀} ⇝ A) → A). The semantic relation of e is S_{e} := { (y, x) | y ∈ dom(⋃ (dom(e(x)))) ∧ x ∈ V_{∃} }. e is an existential (A, R)-valuation if S_{e} ∘ R is irreflexive and, for all x ∈ V_{∃},

e(x) : (S_{e}⟨{x}⟩ → A) → A.

Finally, for applying existential (A, R)-valuations in a uniform manner, we define the function ϵ : (V_{∃} → ((V_{∀} ⇝ A) → A)) → ((V_{∀} → A) → (V_{∃} → A)) by ( e ∈ V_{∃} → ((V_{∀} ⇝ A) → A), π ∈ V_{∀} → A, x ∈ V_{∃} )

ϵ(e)(π)(x) := e(x)(_{S_{e}⟨{x}⟩}↿π).

Lemma 0.3 Let R be a variable-condition.

1. Let R′ be a variable-condition with R⊆R′.

For each existential (A, R′)-valuation e′ there is some existential (A, R)-valuation e such that ϵ(e) = ϵ(e′).

2. Let σ be an existential R-substitution and R′ the σ-update of R. For each existential (A, R′)-valuation e′ there is some existential (A, R)-valuation e such that for all π ∈ V_{∀} → A:

ϵ(e)(π) = σ ∘ eval(A ⊎ ϵ(e′)(π) ⊎ π).

We now define R-validity of a set of sequents with free variables, in terms of validity of a formula (where the free variables are treated as nullary constants).

Definition 0.4 (Validity) Let R be a variable-condition, A a Σ-structure, and G a set of sequents. G is R-valid in A if there is an existential (A, R)-valuation e such that G is (e, A)-valid. G is (e, A)-valid if G is (π, e, A)-valid for all π ∈ V_{∀} → A. G is (π, e, A)-valid if G is valid in A ⊎ ϵ(e)(π) ⊎ π. G is valid in A if for all Γ ∈ G: Γ is valid in A. A sequent Γ is valid in A if there is some formula listed in Γ that is valid in A. Validity in a class of Σ-structures is understood as validity in each of the Σstructures of that class. If we omit the reference to a special Σ-structure we mean validity in some fixed class K of Σ-structures, e.g. the class of all Σstructures (Σ-algebras) or the class of Herbrand Σ-structures (term-generated Σalgebras), cf. Wirth (1997), Wirth & Gramlich (1994) for more interesting classes for establishing inductive validities.

Lemma 0.5 (Anti-Monotonicity of Validity in R) Let G be a set of sequents and R and R′ variable-conditions with R⊆R′. Now: If G is R′-valid in A, then G is R-valid in A.

Example 0.6 (Validity) For x^{∃} ∈ V_{∃}, y^{∀} ∈ V_{∀}, the sequent x^{∃}=y^{∀} is ∅-valid in any A because we can choose S_{e} := V_{∀}×V_{∃} and e(x^{∃})(π) := π(y^{∀}) resulting in ϵ(e)(π)(x^{∃}) = e(x^{∃})(_{S_{e}⟨{x^{∃}}⟩}↿π) = e(x^{∃})(_{V_{∀}}↿π) = π(y^{∀}). This means that ∅-validity of x^{∃}=y^{∀} is the same as validity of ∀y. ∃x. x=y. Moreover, note that ϵ(e)(π) has access to the π-value of y^{∀} just as a raising function f for x in the raised (i.e. dually Skolemized) version f(y^{∀})=y^{∀} of ∀y. ∃x. x=y.

Contrary to this, for R := V_{∃}×V_{∀}, the same formula x^{∃}=y^{∀} is not R-valid in general because then the required irreflexivity of S_{e}∘R implies S_{e} = ∅ and e(x^{∃})(_{S_{e}⟨{x^{∃}}⟩}↿π) = e(x^{∃})(_{∅}↿π) = e(x^{∃})(∅) cannot depend on π(y^{∀}) anymore. This means that (V_{∃}×V_{∀})-validity of x^{∃}=y^{∀} is the same as validity of ∃x. ∀y. x=y. Moreover, note that ϵ(e)(π) has no access to the π-value of y^{∀} just as a raising function c for x in the raised version c=y^{∀} of ∃x. ∀y. x=y.

For a more general example let G = { A_{i,0} … A_{i,n_{i}−1} | i ∈ I }, where for j ≺ n_{i} and i ∈ I the A_{i,j} are formulas with free existential variables from x⃗ and free universal variables from y⃗. Then (V_{∃}×V_{∀})-validity of G means validity of ∃x⃗. ∀y⃗. ∀i ∈ I. ∃j ≺ n_{i}. A_{i,j}; whereas ∅-validity of G means validity of ∀y⃗. ∃x⃗. ∀i ∈ I. ∃j ≺ n_{i}. A_{i,j}.

1 Weights, Syntactic Constructs, and Counterexamples

A proposition Γ can be proved by induction as follows:

Show that for each counterexample of Γ there is another counterexample of Γ that is strictly smaller in a quasi-ordering ≲ in that each ≲ -chain [of counterexamples] has a least element!

Now by the Principle of Dependent Choice (cf. Rubin & Rubin (1985)) a class without minimal elements contains a chain without a least element. Thus, if we can show the above, we know that Γ cannot have any counterexamples at all and must be valid.

This paradigm of ITP was already used by the ancient Greeks, rediscovered by Pierre de Fermat under the name “descente infinie”, and is in our time sometimes called “implicit induction”, cf. Wirth & Becker (1995). Moreover note that theoretically it is also possible to use the strictly stronger Axiom of Choice instead but require only that each ≲ -chain [of counterexamples] has a lower bound [being a counterexample], cf. Geser (1995).

In order to measure our sequents in our induction ordering (i.e. the above quasi-ordering for avoiding non-termination in the inductive argumentation), we supply them with weights from some set ‘Weight’. Why these explicit weights are so important in implicit induction is explained in Wirth & Becker (1995) and more detailed in Wirth (1997), Sect. 12. A weight ℵ together with a sequent Γ forms a syntactic construct (Γ, ℵ). For practical purposes a weight initially is a term w(y_{0}, …, y_{n−1}) where the y_{i} are the free universal variables of Γ and w is similar to a global (rigid) free existential variable in that it can be chosen during the induction proof appropriately, e.g. when the goal is w(t_{1}, t_{2}) < w(t_{2}, s(t_{1})) for natural number terms t_{i} a good idea might be to choose w to be the addition on natural numbers, or when in another proof we have the goals w(t_{1}, (t_{1} + t_{2})) < w(s(t_{1}), t_{1}) and w(t_{1}, t_{2}) < w(t_{1}, s(t_{2})) a good idea might be to choose w to be the lexicographic combination of length up to 2. While in principle also the induction ordering could be chosen for each proof differently, in practice it has shown to be sufficient and adequate to use a fixed wellfounded quasi-ordering (depending on the Σ-structures). E.g. in QuodLibet, a tactic-based ITP system for clausal logic, we essentially use the size of a uniquely denoting constructor ground term in the standard ordering on natural numbers, cf. Kühler (1999). Therefore, we assume that for each Σ-structure A ∈ K there is some wellfounded quasi-ordering ≲_{A}. Furthermore, we assume that Σ contains the binary constant predicate symbol ‘<’ which is interpreted by A as <_{A}, i.e. the ordering of ≲_{A}. Furthermore, A should be able to interpret the functions constructing the weight terms (lexicographic combination &c.) as functions into dom( ≲_{A}).

Syntactic constructs are the basic data structure for ITP, just like sequents or formulas are for the deductive case. The set of all syntactic constructs is denoted by ‘SynCons’. The function ‘logic’ extracts the logic part (here: the sequents) of a set G of syntactic constructs: logic(G) := dom(G).

For powerful ITP we have to be able to restrict the test of whether the weight of a hypothesis is smaller than the weight of a goal (which has to be satisfied for the permission to apply the hypothesis to the goal) to the special case semantically described by their logic parts. This can be achieved by considering only such instances of their weights that result from those valuations that describe invalid instances of their logic parts. A syntactic construct augmented with such a valuation providing extra information on the invalidity of its logic part in some Σ-structure A is called a “counterexample”. More precisely, for an existential (A, R)-valuation e we define: (S, π) is an (e, A)-counterexample (for S) if S is a syntactic construct, π ∈ V_{∀} → A, and logic({S}) is not (π, e, A)-valid. Thus, the logic part of a syntactic construct S is (e, A)-valid iff S has no (e, A)-counterexamples. Furthermore, our induction ordering is not simply a wellfounded quasi-ordering on ‘Weight’ but actually the function mapping each (e, A), where A is a Σ-structure from K and e an existential (A, R)- valuation, to the wellfounded quasi-ordering on Weight × (V_{∀} → A) given by (ℵ, π) ≲_{(e,A)} (ℶ, π′) if eval(A ⊎ ϵ(e)(π) ⊎ π)(ℵ) ≲_{A} eval(A ⊎ ϵ(e)(π′) ⊎ π′)(ℶ). Finally, we extend the induction ordering to SynCons × (V_{∀} → A) by defining

((Γ, ℵ), π) ≲_{(e,A)} ((Δ, ℶ), π′) if (ℵ, π) ≲_{(e,A)} (ℶ, π′).

Note that our induction ordering ≲_{(e,A)} is semantic in the sense of Definition 13.7 of Wirth (1997) because it cannot depend on the syntactic term structure of a weight ℵ but only on the value of ℵ under the evaluation function. In Wirth (1997) we have rigorously investigated the price one has to pay for the possibility to have induction orderings also depending on the syntax of weights. For powerful concrete inference systems this price is surprisingly high. Furthermore, after improving the ordering information in implicit induction by our introduction of explicit weights, the former necessity of sophisticated induction orderings that exploit the term structure does not seem to exist anymore.

Definition 1.1 (Foundedness) (Cf. Wirth & Becker (1995)) Let R be a variable-condition. Let ‘ ↘/↷_{R}’ be a symbol for a single relation. Let G_{0}, G_{1}, H ⊆ SynCons. Now G_{0} is R-strict/quasi-founded on (H, G_{1}) (denoted by G_{0} ↘/↷_{R} (H, G_{1}) ) if ∀A ∈ K. ∀e existential (A, R)-valuation. ∀S ∈ G_{0}. ∀π.

((S, π) is an (e, A)-counterexample) ⇒

∃S′. ∃π′. ( \begin{matrix}& ((S′, π′) is an (e, A)-counterexample) \\ ∧ & ( \begin{matrix}( & \begin{aligned}& S′ ∈ H \\ ∧ & (S′, π′) <_{(e,A)} (S, π) \end{aligned} & ) \\ ∨ & \binom{S′ ∈ G_{1}}{∧ (S′, π′) ≲_{(e,A)} (S, π)} \end{matrix} ) \end{matrix} )

G_{0} is strictly R-founded on H (denoted by G_{0}↘_{R}H) if G_{0} ↘/↷_{R} (H, ∅). G_{0} is (quasi-) R-founded on G_{1} (denoted by G_{0}↷_{R}G_{1}) if G_{0} ↘/↷_{R} (∅, G_{1}).

Note that the expressive power of ↘/↷_{R} is higher than that of ↘_{R} and ↷_{R} together: ( {S}↘_{R}H ∨ {S}↷_{R}G_{1} ) implies {S} ↘/↷_{R} (H, G_{1}) for S ∈ SynCons, but the converse does not hold in general. For an informal but quite imaginative introduction to foundedness cf. Wirth (1997).

Lemma 1.2 Let R, R′ be variable-conditions; G_{0}, G_{1}, G_{2}, G_{3}, H_{1}, H_{2}, H_{3} ⊆ SynCons.

1. If G_{0}↷_{R}G_{1} and logic(G_{1}) is R-valid, then logic(G_{0}) is R-valid, too.

2. If G_{0}⊆G_{1}, then G_{0}↷_{R}G_{1}.

3. If G_{0}↷_{R}G_{1} ↘/↷_{R} (H_{2}, G_{2}), then G_{0} ↘/↷_{R} (H_{2}, G_{2}).

4. If G_{0} ↘/↷_{R} (H_{2}, G_{2}) and G_{1} ↘/↷_{R} (H_{3}, G_{3}), then G_{0}∪G_{1} ↘/↷_{R} (H_{2}∪H_{3}, G_{2}∪G_{3}).

5. In case of R⊆R′ : If G_{0}↷_{R}G_{1}, then G_{0}↷_{R′}G_{1}.

6. In case of R′ being the σ-update of R for an existential R-substitution σ: If G_{0}↷_{R}G_{1}, then G_{0}σ↷_{R′}G_{1}σ.

7. If H_{1} ↘/↷_{R} (H_{1}, G_{1}), then H_{1}↷_{R}G_{1}.

Proof of Lemma 1.2: (1), (2), (3), and (4) are trivial. (5) follows from part (1) of Lemma 0.3, (6) follows from part (2) of Lemma 0.3. (7) relies on the wellfoundedness of ≲_{(e,A)} . □

2 Abstract Inductive Calculi

Now we are going to abstractly describe inductive sequent and tableau calculi. In Wirth (1998) we have shown that the usual deductive first-order calculi are instances of the deductive version of our abstract calculi. This will still be the case for the abstract calculi below, but in this paper we have to concentrate on the inductive part. The main difference to the deductive case is that the sequents are replaced with syntactic constructs, i.e. to each sequent a weight is added for controlling the loops in ITP. The benefit of the abstract version is that every instance is automatically sound. Due to the small number of inference rules in deductive first-order calculi and the locality of soundness, this abstract version is not really necessary for deductive calculi. For inductive calculi, however, due to a bigger number of inference rules (which usually have to be improved now and then) and the globality of soundness, such an abstract version is very helpful, cf. Wirth & Becker (1995), Wirth (1997).

Definition 2.1 (Inductive Proof Forest) An inductive proof forest in a sequent (or else: tableau) calculus is a pair (F, R) where R is a variable-condition and F is a set of pairs (S, t), where S is a syntactic construct and t is a tree whose nodes are labeled with syntactic constructs (or else: whose root is labeled with a weight and whose other nodes are labeled with formulas).

Note that the tree t is intended to represent a proof attempt for S. In case of a tableau calculus the nodes of t are labeled with formulas (the root, however, with a weight). In case of a sequent calculus the nodes are labeled with syntactic constructs. While the syntactic constructs at the nodes of a tree in a sequent calculus stand for themselves, in a tableau calculus all the ancestors have to be included to make up a syntactic construct and, moreover, the formulas at the labels are in negated form:

Definition 2.2 (Goals(), AX, Closedness) ‘Goals(T)’ denotes the set of syntactic constructs labeling the leaves of the trees in the set T (or else: the set of syntactic constructs (Δ, ℶ) with Δ resulting from listing the conjugates of the formulas labeling a branch from a leaf to the root (exclusively) in a tree t in T and ℶ being the label of the root of the tree t). In what follows, we assume AX to be some set of axioms. By this we mean that AX is V_{∃}×V_{∀}-valid. (Cf. the last sentence in Def. 0.4.) The tree t is closed if logic(Goals({t})) ⊆ AX .

The readers may ask themselves why we consider a forest instead of a single tree only. If we have two trees (S, t), (S′, t′) ∈ F we can apply S as a lemma or induction hypothesis in the tree t′ of S′, provided that the lemma application relation is acyclic and the application of the hypothesis produces a goal that expresses that the instance of the hypothesis is smaller than S′ in the induction ordering.

Definition 2.3 (Inductive Invariant Condition) The inductive invariant condition on (F, R) is H↷_{R}Goals(ran(F)) for the set of hypotheses H := dom(F).

From Lemma 0.5 and Lemma 1.2(1) we immediately get: Theorem 2.4 Let the inductive proof forest (F, R) satisfy the above inductive invariant condition and set H := dom(F). If all trees in ran(F) are closed, then logic(H) is R-valid.

Note that, contrary to the deductive case, local argumentation on a single tree is not possible: If (S, t) ∈ F, (F, R) satisfies the inductive invariant condition, and t is closed, we do not know that logic({S}) is R-valid because we may have applied some induction hypothesis S′ ∈ H\{S} when constructing the proof tree t of S and the proof tree of S′ is not closed. In other words, all trees in the forest must be closed before we know that any hypothesis in logic(H) is R-valid.

Theorem 2.5 The inductive invariant condition is always satisfied when we start with an empty inductive proof forest (F, R) := (∅, ∅) and then iterate only the following kinds of modifications of (F, R) (resulting in (F′, R′)):

Hypothesizing: Let R′ be a variable-condition with R⊆R′. Let Let (Γ, ℵ) be a syntactic construct. Let t be the tree with a single node only, which is labeled with (Γ, ℵ) (or else: with a single branch only, such that Γ is the list of the conjugates of the formulas labeling the branch from the leaf to the root (exclusively) and ℵ is the label of the root). Then we may set F′ := F ∪ {((Γ, ℵ), t)}.

Expansion: Let R′ be a variable-condition with R⊆R′. Let (S, t) ∈ F and H := dom(F). Let l be a leaf in t. Let (Δ, ℶ) be the label of l (or else: Δ result from listing the conjugates of the formulas labeling the branch from l to the root (exclusively) and ℶ be the label of the root of t). Let G be a finite set of syntactic constructs (or else: let M be a finite set of sequents and set G := { (ΠΔ, ℶ) | Π ∈ M }). Now if {(Δ, ℶ)} ↘/↷_{R′} (H, G) then we may set F′ := (F \{(S, t)}) ∪ {(S, t′)} where t′ results from t by adding to the former leaf l, exactly for each syntactic construct S′ in G, a new child node labeled with S′ (or else: exactly for each sequent Π in M a new child branch such that Π is the list of the conjugates of the formulas labeling the branch from the leaf to the new child node of l).

Instantiation: Let σ be an existential R-substitution. Let R′ be the σ-update of R. Then we may set F′ := F σ.

Proof of Theor. 2.5: The empty proof forest satisfies the inductive invariant condition by Lemma 1.2(2). \underline{Hypothesizing:} From H↷_{R}Goals(ran(F)) we get H↷_{R′}Goals(ran(F)) by Lemma 1.2(5) for H := dom(F). Thus, from {(Γ, ℵ)}↷_{R′}{(Γ, ℵ)} (by Lemma 1.2(2)) we get H ∪ {(Γ, ℵ)} ↷_{R′} Goals(ran(F))∪{(Γ, ℵ)} by Lemma 1.2(4), i.e. H′↷_{R′}Goals(ran(F′)) for H′ := dom(F′). \underline{Expansion:} \{(Δ, ℶ)\} ↘/↷_{R′} (H, G) and (Goals(ran(F))) \ \{(Δ, ℶ)\} ↷_{R′} (Goals(ran(F))) \ {(Δ, ℶ)} (by Lemma 1.2(2)) give Goals(ran(F)) ↘/↷_{R′} (H, G′) for G′ := (Goals(ran(F))\{(Δ, ℶ)})∪G by Lemma 1.2(4). From the old invariant condition H↷_{R}Goals(ran(F)) we get H↷_{R′}Goals(ran(F)) by Lemma 1.2(5), and then by Lemma 1.2(3) conclude H ↘/↷_{R′} (H, G′). Thus, by Lemma 1.2(7) we have H↷_{R′}G′, and then from G′↷_{R′}Goals(ran(F′)) (due to Lemma 1.2(2)) we get H↷_{R′}Goals(ran(F′)) due to Lemma 1.2(3), which is the new invariant condition on (F′, R′) due to H = dom(F) = dom(F′). \underline{Instantiation:} From the old invariant condition H↷_{R}Goals(ran(F)) for H := dom(F) we get Hσ↷_{R′}Goals(ran(F σ)) by Lemma 1.2(6), which is the new invariant condition on (F′, R′) due to dom(F′) = dom(F)σ = Hσ. □

Now the crucial step of implicit induction (i.e. the application of an induction hypothesis (Γ, ℵ) instantiated with a substitution ϱ to expand a goal (Δ, ℶ)) can be formulated as an Expansion step in the tableau calculus (sequent calculus analogously) as follows. Theorem 2.6 Let (F, R) be an inductive proof forest in a tableau calculus. We want to apply (Γ, ℵ) ∈ H := dom(F) as an induction hypothesis to expand the goal (Δ, ℶ) that results from listing the conjugates of the formulas and the weight labeling the branch from a leaf l to the root of a tree t ∈ ran(F). Set X := V_{∃}((Γ, ℵ)) and Y := { y ∈ V_{∀}((Γ, ℵ)) | X×{y} ⊆ R }. Let ϱ ∈ Y → (V_{∃}\V_{∃}(F)) be an injective substitution. Now the following instantiation of R′ and M describes a sub-rule of the Expansion rule of the tableau calculus of Theor. 2.5: Set R′ := R and set M to be the set containing the sequents ℵϱ<ℶ and \overline{Bϱ} for each formula B listed in the sequent Γ.

Note that Y contains exactly those free universal variables of (Γ, ℵ) that have no free existential variables in their scopes when imagining any list of quantifiers for all free variables of (Γ, ℵ) that represents (a superset of) R. The variables in Y are those on which no solution for the free existential variables in X depends. Therefore, the variables in Y are those which we can instantiate when applying the induction hypothesis (Γ, ℵ). Although it does not seem impossible to use more variables for induction, this does not seem to be necessary; especially because we can extend R with X×{y} in order to instantiate y when applying the induction hypothesis. Moreover, I do not known any more general approach in the literature. E.g., in Baaz &al. (1997), the inductive part of theorem proving is triggered by application of a δ-rule and the variable y of the quantifier removed by the δ-rule becomes the induction variable. In our approach, the δ-rule application would replace y with a new free universal variable y^{∀} and extend the variable-condition with X×{y^{∀}} such that y^{∀} ∈ Y would hold.

Proof of Theor. 2.6: According to the definition of an Expansion step in the tableau calculus of Theor. 2.5 we have to show {(Δ, ℶ)} ↘/↷_{R} (H, { (AΔ, ℶ) | A ∈ M }). Thus, for A ∈ K, e an existential (A, R)-valuation, π ∈ V_{∀} → A, assume ((Δ, ℶ), π) to be an (e, A)-counterexample. If some formula A ∈ M is not (π, e, A)-valid then also ((AΔ, ℶ), π) is an (e, A)-counterexample with ((AΔ, ℶ), π) ≲_{(e,A)} ((Δ, ℶ), π). Otherwise, ℵϱ<ℶ is but Γ ϱ is not (π, e, A)-valid. Define π′ ∈ V_{∀} → A by

π′(y) := ϵ(e)(π)(ϱ(y)) for y ∈ Y and π′(y) := π(y) for y ∈ V_{∀}\Y. \underline{Claim 1:} For x^{∃} ∈ V_{∃}((Γ, ℵ)) we have ϵ(e)(π)(x^{∃}) = ϵ(e)(π′)(x^{∃}). \underline{Proof of Claim 1:} Otherwise there must be some y^{∀} ∈ Y with y^{∀} S_{e} x^{∃}. Since x^{∃} ∈ X we have x^{∃} R y^{∀} by definition of Y. But then S_{e} ∘ R is not irreflexive, which contradicts e being an existential (R, A)-valuation. \underline{Q.e.d. (Claim 1)} Hence, the values of Γ and ℵ under eval(A ⊎ ϵ(e)(π′) ⊎ π′) are the same as the values of Γ and ℵ under eval(A ⊎ ϵ(e)(π) ⊎ π′) which again are the same as the values of Γ ϱ and ℵϱ under eval(A ⊎ ϵ(e)(π) ⊎ π) by the Substitution-Lemma. Thus, on the one hand from the (π, e, A)-validity of ℵϱ<ℶ we get ((Γ, ℵ), π′) <_{(e,A)} ((Δ, ℶ), π), and on the other hand from Γ ϱ not being (π, e, A)- valid we know that ((Γ, ℵ), π′) is an (e, A)-counterexample. □

3 An Example

Due to limited space we are not able to show the usefulness of our integration of free existential variables and full first-order formulas into implicit induction with a sophisticated example. Instead, we will sketch a simplified toy example with mutual induction that will give the reader a concrete idea on how proofs look like. Note, however, that (due to mutual induction and non-trivial weights) even this toy example has no straightforward proofs in the ITP calculus of Baaz &al. (1997) or any known ITP system with the exception of QuodLibet, cf. Kühler (1999).

In order not to require even more prerequisites, we do not explicitly refer to our inductive specification techniques described in Kühler & Wirth (1996), but use a standard (order-sorted) first-order specification style.

Signature: Sorts: nat⊆ORD. Here nat is the sort of natural numbers and ORD the sort for the induction ordering. We use zero 0 :→ nat and successor s : nat → nat as constructors for the sort nat. Moreover, P. nat and Q. nat,nat are two defined predicates on the natural numbers. Furthermore, <. ORD,ORD is the induction ordering and lex : nat,nat,nat → ORD is the lexicographic combination of length 0, 1, or 2 as indicated by the first argument, e.g. lex(s(0), x, y) models the 1-tuple (x) while lex(0, x, y) models the 0-tuple or empty word (). We use x, y, z for variables of the sort nat where superscripts like x^{∃}, x^{∀} indicate free existential and free universal variables. Axioms:

(lex0)  ∀x_{1}, y_{0}, y_{1}, z_{0}, z_{1}. lex(0, y_{0}, z_{0})<lex(s(x_{1}), y_{1}, z_{1})
(lex1) ∀x_{0}, x_{1}, y_{0}, y_{1}, z_{0}, z_{1}. ( lex(s(x_{0}), y_{0}, z_{0})<lex(s(x_{1}), y_{1}, z_{1}) ⇐ y_{0}<y_{1} )
(lex2)  ∀x_{0}, x_{1}, y, z_{0}, z_{1}. ( \begin{matrix}lex(s(x_{0}), y, z_{0}) & < & lex(s(x_{1}), y, z_{1}) \\ ⇐ & lex(x_{0}, z_{0}, 0) & < & lex(x_{1}, z_{1}, 0) \end{matrix} )
(nat0)  ∀x. ( x=0 ∨ ∃y. x=s(y) )

(lex0) says that the empty tuple is the smallest, (lex1) implements a comparison of the first tuple elements, and (lex2) discards identical first tuple elements. (nat0) says that any natural number is zero or the successor of another natural number. The following axioms define the special predicates of our example.

(P0)  P(0)
(P1)  ∀x. ( P(s(x)) ⇐ ( P(x) ∧ Q(x, s(x)) ) )
(Q0)  ∀x. Q(x, 0)
(Q1) ∀x, y. ( Q(x, s(y)) ⇐ ( Q(x, y) ∧ P(x) ) )

We want to show ∀x. P(x) and ∀y, z. Q(y, z). We first do a tableau calculus proof. We start with the empty forest. Two Hypothesizing steps provide us with the hypotheses (P(x0^{∀}); w0^{∃}(x0^{∀})) with single-branch tree (1) w0^{∃}(x0^{∀}), (1.1) ¬P(x0^{∀}); and (Q(y0^{∀}, z0^{∀}); w1^{∃}(y0^{∀}, z0^{∀})) with single-branch tree (2) w1^{∃}(y0^{∀}, z0^{∀}), (2.1) ¬Q(y0^{∀}, z0^{∀}). Note that the first number in the preceding list is the number of the proof tree (indicating its root node) and a suffix “.i ” denotes the step to the i^{th} child node. Since the formulas of the specification are implicitly on all branches, we can use (nat0) to add to (1.1) the children x0^{∃} = 0 and x0^{∃} = s(x1^{∀}) in an Expansion step with variable restriction (x0^{∃}, x1^{∀}). An Instantiation step with {x0^{∃}↦x0^{∀}} (which a concrete inference system should do immediately together with the preceding Expansion step) gives us the new tree (1.1.1) x0^{∀} = 0, (1.1.2) x0^{∀} = s(x1^{∀}). Rewriting copies of (1.1) with these children in two Expansion steps yields (1.1.1.1) ¬P(0), (1.1.2.1) ¬P(s(x1^{∀})). By (P0) we can close the first branch with (1.1.1.1.1) P(0). By (P1) we can add (1.1.2.1.1) P(s(x1^{∀})) (closed), (1.1.2.1.2) ¬P(x1^{∀}), (1.1.2.1.3) ¬Q(x1^{∀}, s(x1^{∀})). Now, after these standard firstorder tableau steps we do an induction hypothesis application step as described in the previous section. We apply the hypothesis (P(x0^{∀}); w0^{∃}(x0^{∀})) with substitution ϱ := {x0^{∀}↦x1^{∃}} to (1.1.2.1.2), resulting in the new children P(x1^{∃}) and w0^{∃}(x1^{∃})≮w0^{∃}(x0^{∀}), where w0^{∃}(x0^{∀}) comes from the root (1) and ≮ is the negation of <. After instantiating {x1^{∃}↦x1^{∀}} we get (1.1.2.1.2.1) P(x1^{∀}) (closed) and (1.1.2.1.2.2) w0^{∃}(x1^{∀})≮w0^{∃}(x0^{∀}). Note that the only difference to an Extension step in Model Elimination tableaux (cf. Baumgartner &al. (1997)) lies with the additional child (1.1.2.1.2.2), which asks us to show that the instance of the hypothesis is smaller than the weight of our proof tree. Indeed: Hypothesis application differs from the standard lemma (or axiom) application only in producing an additional ≮-goal. This makes hypothesis application a little more expensive than lemma application. Similarly, we apply the induction hypothesis (Q(y0^{∀}, z0^{∀}); w1^{∃}(y0^{∀}, z0^{∀})) with substitution ϱ := {y0^{∀}↦y0^{∃}, z0^{∀}↦z0^{∃}} to (1.1.2.1.3), which after instantiation with {y0^{∃}↦x1^{∀}, z0^{∃}↦s(x1^{∀})} results in (1.1.2.1.3.1) Q(x1^{∀}, s(x1^{∀})) (closed) and (1.1.2.1.3.2) w1^{∃}(x1^{∀}, s(x1^{∀}))≮w0^{∃}(x0^{∀}). Rewriting the leaves of the open branches in place with (1.1.2) we get (1.1.2.1.2.2) w0^{∃}(x1^{∀})≮w0^{∃}(s(x1^{∀})) and (1.1.2.1.3.2) w1^{∃}(x1^{∀}, s(x1^{∀}))≮w0^{∃}(s(x1^{∀})). Expanding the tree (2) analogously to the tree (1) we get as leaves of the open branches

(2.1.2.1.2.2) w1^{∃}(y0^{∀}, z1^{∀})≮w1^{∃}(y0^{∀}, s(z1^{∀})) and (2.1.2.1.3.2) w0^{∃}(y0^{∀})≮w1^{∃}(y0^{∀}, s(z1^{∀})).

Now both hypotheses have been applied in both trees. Next, we choose our weight functions in such a way that we can close both trees: w0^{∃}(x) := lex(s(0), x, 0) and w1^{∃}(y, z) := lex(s(s(0)), y, z). Applying (lex0), (lex1), (lex2) to the resulting leaves in the standard fashion results in x1^{∀}≮s(x1^{∀}) and z1^{∀}≮s(z1^{∀}) as the leaves of the only open branches. Finally, these branches are closed by comparing the size of a uniquely denoting constructor ground term: A branch containing a literal of the form t_{0}≮t_{1} is closed if the number of occurrences of each free variable in t_{0} is not bigger than the number of occurrences of that variable in t_{1}, the size of t_{0} is strictly smaller than the size of t_{1}, and t_{0}, t_{1} are pure constructor terms. Cf. Kühler & Wirth (1996) for the notion of “constructor term” and for the models where our induction ordering is wellfounded indeed.

We may ask: Which steps in this proof were typical for ITP in the sense that their soundness relies on notions of inductive validity instead of the stronger notion of deductive (first-order) validity? Besides the four induction hypothesis applications, the final branch closure rules are typical for induction because they require that, in all models in K, 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 (1973)). Other steps typical for induction but not applied in this example are narrowing steps to solve equality literals. Their soundness relies on the freeness of the models in K. (Note that narrowing in ITP relies on confluence but not on termination of the reduction relation of the specification, cf. Wirth (1997).) Moreover, ITP often is only successful when one tries to show theorems that are more general than the ones one initially intended to show. This is because an inductive theorem is not only a task (as goal) but also a tool (as induction hypothesis) for ITP. This generalization is unsafe in the sense that it may transform a valid hypothesis into an invalid one (over-generalization). Therefore, generalization should not be modeled in Expansion steps within a tree. Instead, the generalized sequent should start a new tree (Hypothesizing step) and be later applied to the original tree as an induction hypothesis or lemma. Since a valid input theorem may result in an invalid goal due to overgeneralization, the ability of an ITP system to detect invalid goals is important under a practical aspect. When all Expansion and Instantiation steps in a tree are known to be safe, the detection of an invalid goal in the tree implies invalidity of the hypothesis of this tree, which then should be completely removed from the proof forest.

Now we are going to compare the above tableau calculus proof with a corresponding sequent calculus proof of the same hypotheses. Of course, we could simply transform the tableau trees into sequent trees by bottom-up replacing the label of each node with the syntactic construct listing the conjugates of the formulas and the weight labeling the (partial) branch from this node to the root, and finally removing the root part of the tree where the nodes are ancestors of a node of the initial Hypothesizing steps (here: removing the root nodes). This, however, would mean to pay the price for sequent calculi (i.e. multiplying the number of formulas labeling each proof tree with at most nearly the depth of that tree) without using the advantages of sequent calculi. Thus, let us start again with the hypotheses (P(x0^{∀}); w0^{∃}(x0^{∀})) and (Q(y0^{∀}, z0^{∀}); w1^{∃}(y0^{∀}, z0^{∀})). The single-node tree for the former is (1) P(x0^{∀}); w0^{∃}(x0^{∀}). Note that the goal in the tree is identical to the hypothesis, contrary to the tableau version where the two differ in duality and locality. While this is not a hindrance for completely automatic ITP systems, it poses considerable practical problems in systems where user-guidance is possible: The primitive process of switching duality is a typical source of errors for human beings (or me at least). Perfectly analogous to the tableau proof we get the children x0^{∀} ≠ 0, P(x0^{∀}); w0^{∃}(x0^{∀}) and x0^{∀} ≠ s(x1^{∀}), P(x0^{∀}); w0^{∃}(x0^{∀}). Contrary to the tableau proof we are now able to rewrite the literal inherited from the parent node in place without copying it. Note that in tableau proofs an equality literal can be used to rewrite formulas of its offspring in place, whereas it must copy ancestor formulas beforehand down to its offspring because the ancestor is also part of other branches that do not include the equality literal. Moreover, the weight term can be rewritten as well, which again is not possible in the tableau version where the weight is at the root node. After rewriting we get x0^{∀} ≠ 0, P(0); w0^{∃}(0) and x0^{∀} ≠ s(x1^{∀}), P(s(x1^{∀})); w0^{∃}(s(x1^{∀})). Since the equality literals are in solved form for the variable x0^{∀} that does not occur elsewhere in the syntactic constructs, we know that validity cannot rely on this literal. This means that we can safely remove both equality literals resulting in (1.1) P(0); w0^{∃}(0) and (1.2) P(s(x1^{∀})); w0^{∃}(s(x1^{∀})). Removing redundant formulas is the most important simplification step besides contextual rewriting. It seems to be impossible in tableau trees unless the redundancy of the formula is due to the ancestor nodes only, which only is the case for useless formulas that should not have been added at all. In Wirth (1997) and in QuodLibet (cf. Kühler (1999)) the Expansion from (1) into (1.1) and (1.2) is done by a single inference step applying a so-called “covering set of substitutions”. Note that the present state of the sequent proof is much simpler than the corresponding state of the tableau proof. The former consists of the nodes (1.1) and (1.2) and has two formulas and one variable. The latter consists of a six node tree with five formulas and two variables. This is of practical importance because tactics for proof search are more easily confused with less concise proof state representations. The rest of the whole sequent proof is analogous to the tableau proof with the exception that all rewrite steps are omitted since there are no equality literals to rewrite with and the terms are already in normal form.

Another possibility restricted to sequent calculi is that each syntactic construct labeling a node in the trees can be applied as an induction hypothesis. We do not see a real advantage in this because splitting the tree in two above such an induction hypothesis results in a better structure of the proof forest and in more successful proofs because we can adjust the syntactic construct appropriately: Suppose we had not started a new proof tree for the hypothesis for Q but instead kept the hypothesis for Q down in the tree (1) at position (1.2.3). Several unsafe generalization steps would have been necessary before Q(x1^{∀}, s(x1^{∀})), P(s(x1^{∀})); w0^{∃}(s(x1^{∀})) would have become useful as an induction hypothesis, namely removing the second formula, generalizing s(x1^{∀}) to a new variable, and switching to a weight that measures also this new variable. Moreover, in practice one should not apply the hypothesis for Q in the tree for P before it is obvious that the tree for Q mutually needs the hypothesis for P: Most of the time a proof for Q can be completed in a proof forest not containing the tree for P. In this case, not only the number of trees in the proof forest for Q gets smaller, but also the tree for P because ∀y, z. Q(y, z) can then be applied as a lemma and not as an induction hypothesis, which cuts off the ≮-branch of the proof tree of P.

4 Conclusion

We have shown how to integrate implicit ITP into first-order sequent and tableau calculi. The following aspects are novel compared to the concrete implicit induction calculus of Wirth (1997): The tableau presentation, the possibility to use full first-order formulas instead of literals only, and the important addition of free existential variables, i.e. the “dummies” of Prawitz (1960), making the major difference between the free variable calculi of Fitting (1996) and the calculi of Smullyan (1968). Contrary to Baaz &al. (1997) we really integrate implicit induction: When we start an inductive proof we do not restrict the applicable induction hypotheses. We can do mutual induction and invent completely new induction hypotheses, which can be full first-order sequents instead of literals only. Moreover, we can also generate induction hypotheses eagerly in the style of explicit induction, which enables goal-directedness w.r.t. induction hypotheses. All this is not possible in the calculus of Baaz &al. (1997).

Furthermore, we exemplified that although tableau calculi may save repetition of formulas, sequent calculi have substantial advantages: Rewriting of formulas in place is always possible, and we can remove formulas that are redundant w.r.t. the other formulas in a sequent. Note that formulas like (nat0) make equality omnipresent in induction and that these simplification steps are even more important in inductive than in deductive theorem proving: Not only do they play a role in the generation of appropriate induction hypotheses; they are an essential part of the failure detection process that has to compensate for over-generalization of induction hypotheses in addition to the detection of invalid input theorems. Finally, the presence of two dual versions of each hypothesis in inductive tableau calculi makes proof guidance by human users more difficult.

References

Matthias Baaz, Uwe Egly, Christian G. Fermüller (1997). Lean Induction Principles for Tableaux.

6th TABLEAU 1997, LNAI 1227, pp. 62-75, Springer. Leo Bachmair (1988). Proof By Consistency in Equational Theories. 3rd IEEE symposium on Logic

In Computer Sci., pp. 228-233, IEEE Press. Peter Baumgartner, Ulrich Furbach, Frieder Stolzenburg (1997). Computing Answers with Model

Elimination. Artificial Intelligence 90, pp. 135-176. Herbert B. Enderton (1973). A Mathematical Introduction to Logic. Academic Press. Melvin C. Fitting (1996). First-Order Logic and Automated Theorem Proving. 2nd extd. ed., Sprin-

ger. Gerhard Gentzen (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift

39, pp. 176-210, 405-431. Alfons Geser (1995). A Principle of Non-Wellfounded Induction. In: Tiziana Margaria (ed.): Kol-

loquium Programmiersprachen und Grundlagen der Programmierung, MIP-9519, pp. 117-124, Univ. Passau.

Ulrich Kühler (1999). A Tactic-Based Inductive Theorem Prover for Data Types with Partial

Operations. Dissertation (Ph.D. thesis), Univ. Kaiserslautern, to appear. Ulrich Kühler, Claus-Peter Wirth (1996). Conditional Equational Specifications of Data Types with

Partial Operations for Inductive Theorem Proving. SEKI-Report SR–96–11, Univ. Kaiserslautern. Short version in: 8th RTA 1997, LNCS 1232, pp. 38-52, Springer.

Peter Padawitz (1996). Inductive Theorem Proving for Design Specifications. J. Symbolic Compu-

tation 21, pp. 41-99, Academic Press. Dag Prawitz (1960). An Improved Proof Procedure. In: Siekmann & Wrightson (1983), Vol. 1, pp.

159-199. Herman Rubin, Jean E. Rubin (1985). Equivalents of the Axiom of Choice. Elsevier. Jörg H. Siekmann, G. Wrightson (eds.) (1983). Automation of Reasoning. Springer. Raymond M. Smullyan (1968). First-Order Logic. Springer. Claus-Peter Wirth (1997). Positive/Negative-Conditional Equations: A Constructor-Based Frame-

work for Specification and Inductive Theorem Proving. Dissertation (Ph.D. thesis), Verlag Dr. Kovač, Hamburg.

Claus-Peter Wirth (1998). Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized δ-Rule but Without Skolemization. Report 698/1998, FB Informatik, Univ. Dortmund. Short version in: Gernot Salzer, Ricardo Caferra (eds.). Proc. 2nd Int. Workshop on First-Order Theorem Proving (FTP), pp. 244-255, Vienna, 1998. Also accepted for LNCS version, Springer, 1999.

Claus-Peter Wirth, Klaus Becker (1995). Abstract Notions and Inference Systems for Proofs by

Mathematical Induction. 4th CTRS 1994, LNCS 968, pp. 353-373, Springer. Claus-Peter Wirth, Bernhard Gramlich (1994). On Notions of Inductive Validity for First-Order

Equational Clauses. 12th CADE 1994, LNAI 814, pp. 162-176, Springer.

WWW-home-page: http://ags.uni-sb.de/˜ cp/welcome.html Acknowledgements: I would like to thank Ulrich Furbach and his whole group for all they taught me on tableau calculi and Paul Howard for a short private E-mail communication on the Principle of Dependent Choice that was very helpful to me.