Seduct — A Proof Compiler for First Order Logic

Karl Stroetmann

Siemens AG

Abstract. In this paper we present Seduct, which is a theorem prover for many–sorted first order logic. Seduct has been specially tailored to economically discharge proof obligations arising during the process of software verification. We will mainly describe those features of Seduct which distinguish this theorem prover from other theorem provers and which make it especially suited for software verification.

1 Introduction

One of the main reasons formal methods have not, up to now, been established on a broad base in the industrial software development process is the as yet insufficient support for the discharge of proof obligations. Although there are a lot of high performance automatic theorem provers around, in practice these tools prove to be of limited value when used for software verification. This is mainly due to three reasons:

– Automatic theorem provers lack a user friendly command language which could be used by programmers not already acquainted with formal methods.

– Automatic theorem provers are not well suited for the kind of proof obligations arising during software verification. Normally, they have been trimmed to prove open conjectures in, for example, group theory.

– If an automatic theorem prover fails to prove a theorem, the prover usually does not provide the user with easy–to–understand information explaining the failure of the proof.

Concerning the problems just mentioned interactive theorem provers do a far better job. However, in order to make the process of software verification economically viable, interactive theorem provers have to be coupled with automatic theorem provers in order to protect the user from having to prove large numbers of trivialities by hand.

Seduct has been developed as a theorem prover especially tailored for software verification. It has been designed as a so called proof compiler, i.e., it compiles abstract proofs provided by the user into concrete mathematical proofs. An abstract proof of a theorem is intended to contain just the coarse structure of the proof, i.e., the lemmata and the logical connections between these lemmata. The concept of abstract proofs allows breaking a proof into sufficiently small chunks which are in the reach of an automatic theorem prover. If on a first run of the proof compiler these chunks turn out to be too big, then they can still be dealt with interactively.

The automatic theorem prover embedded in Seduct differs from other automatic theorem provers in a number of ways. The most important differences are the following:

– Seduct is a theorem prover for many–sorted first order logic with equality and inequality, (i.e., the symbol ≤ is given the same status as the equality symbol =). This is possible because the axioms describing a linear order have been hard–wired into the proof engine of Seduct.

– Seduct offers shorthands for certain axioms occurring frequently during software verification like, for example, axioms stating that a sort is freely generated by a set of constructors.

Seduct consists mainly of two modules, the first of which is an automatic theorem prover or, as we prefer to call it, a proof engine. The second is a command interpreter used to drive this engine. The proof engine processes formulae in two steps. In the first step, an extended sequent calculus is used to deal with the logical structure of the formulae, i.e., with connectors like ∧, ∨, → and quantifiers like ∀, ∃. The second step then deals with the equality symbol = and the inequality symbol ≤ by means of rewrite techniques.

The rest of this paper is organized as follows. Section 2 presents the sequent calculus, Section 3 describes the rewrite techniques employed, and in Section 4 the reader is introduced to the command language of Seduct through an example proof. Section 5 contains some concluding remarks.

2 The Sequent Calculus

The proof engine of Seduct consists of two parts, the first of which is an implementation of a sequent calculus. This section describes the sequent calculus, while the next section is devoted to a description of the rewrite techniques on which the second part of the proof engine is based.

To begin with we discuss the input language. This is just ordinary many– sorted first order predicate logic where we have added the “if ⋯ then ⋯ else ⋯ fi” operator both on the level of terms and on the level of formulae; if F, G, H, are formulae and s, t are terms, then

        if F then G else H fi

is a formula, while “if F then s else t fi” is a term. Furthermore, not only is s = t a formula, but s ≤ t also is. Thus the concept of inequality is dealt with on the same footing as the concept of equality.

The sequents on which our sequent calculus is based are pairs of finite multisets of formulae. These multisets will be written as lists using the square brackets “[” and “]”, while the sequent consisting of the two multisets Γ and Δ will be written as Γ ⊢ Δ. If Γ = [A_{1}, …, A_{m}] and Δ = [B_{1}, …, B_{n}] , then we regard the sequent Γ ⊢ Δ as representing the formula

A_{1} ∧ ⋯ ∧ A_{m} → B_{1} ∨ ⋯ ∨ B_{n}.

Notation: In this section we will use the following notation: Upper case Greek letters (e.g., Γ, Δ, …) will be used to designate finite multisets of formulae. Single formulae will be written using upper case Latin letters in italics (e.g., A, B, …, F, G, …). Terms will be denoted by lower case Latin letters printed in italics (e.g., a, b, c, …, r, s, t, ⋯). If Γ and Δ are multisets while A is a formula, then Γ, Δ is a shorthand notation for Γ ∪ Δ, while Γ, A will be interpreted as Γ ∪ [A]. If A is a formula, t a term and x a variable, then A[x ← t] denotes the formula obtained from A by replacing every occurrence of x by t, where care is taken that no free variables are captured.

The sequent calculus embodied in Seduct is quite similar to the one given in Gallier [Gal86], but there are some important differences. We will concentrate our discussion on these differences.

2.1 Preprocessing

Prior to applying the sequent calculus we have to do some preprocessing of the input formulae. This is due to the fact that we have to remove the “if ⋯ then ⋯ else ⋯ fi” construct from the term level in order to make the rewrite techniques work.

To eliminate if–operators we need two transformation rules for formulae. The first transformation rule takes terms of the form

f( s_{1}, ⋯, s_{i−1}, if B then t_{1} else t_{2} fi, s_{i+1}, ⋯, s_{n} )

and replaces these terms by terms of the form

if B then f( s_{1}, ⋯, t_{1}, ⋯, s_{n}) else f( s_{1}, ⋯, t_{2}, ⋯, s_{n}) fi.

Here f stands for an arbitrary function symbol. This rule moves the if–operators from subterms to superterms. To eliminate the if–operators altogether from the term level, we have a similar rule which replaces the if–operators from atomic formulae of the form “p( ⋯, if B then t_{1} else t_{2} fi, ⋯)”.

2.2 Axioms and rules of the sequent calculus

The sequent calculus we have implemented in Seduct contains five different axiom schemes:

1. Γ, false ⊢ Δ is an axiom.

2. Γ ⊢ Δ, true is an axiom.

3. Γ, ∀x_{1}, ⋯, x_{n}.P ⊢ Δ, ∃x_{1}, ⋯, x_{n}.Q is an axiom provided that P and Q are unifiable.

4. Γ ⊢ Δ, ∃x_{1}, ⋯, x_{n}.P = Q is an axiom provided that P and Q are unifiable.

5. Γ ⊢ Δ is an axiom provided it can be established as valid using the rewrite techniques described in the next section.

Following Smullyan [Smu68] we divide the rules into α, β, γ and δ rules. However, for reasons which will become clear later, we have added some distribution rules for quantifiers. Furthermore, in order to deal with inequalities efficiently we need an additional type of rules which we have called ι rules. We now describe each of these classes of rules in turn. However, in order to save space, we will not present the complete set of rules. This set is quite extensive since Seduct supports true, false, ¬, ∧, ∨, →, ↔, if then else fi, ∀, and ∃ as primitives. In the following, we present only a selection of rules and we concentrate our discussions on those rules which are not present in other formulations (e.g., [Gal86]) of the sequent calculus.

We start with a description of the α rules. These are propositional rules which cause no branching in the proof tree. A typical α rule is the introduction of ∧ in the antecedent:

\frac{Γ, A, B ⊢ Δ}{Γ, A ∧ B ⊢ Δ} (∧A)

The β rules are the rules responsible for the branching of proof trees. The rule for the introduction of ∧ in the succedent reads:

\frac{Γ ⊢ Δ, A Γ ⊢ Δ, B}{Γ ⊢ Δ, A ∧ B} (∧S)

We proceed by describing the δ rules. A typical δ rule is the introduction of ∀ in the succedent:

\frac{Γ ⊢ Δ, P [x ← c]}{Γ ⊢ Δ, ∀x.P} (∀S)

The application of this rule is subject to the variable condition that the constant c does not occur in the conclusion Γ ⊢ Δ, ∀x.P.

Finally, we discuss the γ rules. A typical γ rule is the rule for the introduction of ∀ in the antecedent:

\frac{Γ, P [x ← t] ⊢ Δ}{Γ, ∀x.P ⊢ Δ} (∀A)

You will notice that the t appearing in this rules is printed in boldface. This reflects the fact that t is not a term but rather a dummy variable. In the course of the proof, this variable will be instantiated to a term of our object language. Due to the variable conditions of the δ rules, special care has to be taken when instantiating dummy variables.

Unfortunately, if we use the γ rule given above, then we will sacrifice completeness. This is due to the fact that our version of the γ rule is not analytical. A rule is called analytical if the conclusion is true if and only if the premise is true. In order to compensate for the lack of completeness of γ rules we present distribution rules which can be used to distribute quantifiers over connectors. The application of these rules sometimes makes the application of γ rules unnecessary. There are some rules describing distribution relations between quantifiers and propositional symbols. For example, the rule for distributing ∀ over ∧ is the following:

\frac{Γ, ∀x̄.A, ∀x̄.B ⊢ Δ}{Γ, ∀x̄.A ∧ B ⊢ Δ} (∀∧A)

Here and later x̄ denotes a tuple of variables. There are similar distribution rules for the distribution of quantifiers over quantifiers.

Of course, the distribution laws do not eliminate quantifiers, they only push them into the formulae. They would be useless if we would use the sequent calculus to eliminate all quantifiers. However, it turns out that we do not have to eliminate universal quantifiers quantifying conditional equations in the antecedent, nor do we have to eliminate existential quantifiers quantifying targets. These notions will be explained in the next section.

2.3 How to handle totality of ≤ in the sequent calculus

Finally, we present the rules we have added in order to be able to deal efficiently with inequalities. The rule for the introduction of ≤ in the succedent reads:

\frac{Γ, s ≥ t ⊢ Δ, s = t}{Γ ⊢ Δ, s ≤ t}

Rules of this kind, which we have termed ι rules, are used in order to reflect the totality of the relation ≤ in our calculus, i.e., they hard–wire the axiom

x ≤ y ∨ y ≤ x.

The other properties of ≤, namely reflexivity, antisymmetry, and transitivity will be taken care of by the rewrite techniques described in the next section.

We also have versions of the ι–rules dealing with the combination of quantifiers and inequalities. For example:

\frac{Γ, ∀x̄.t ≤ s ⊢ Δ, ∃x̄.s = t}{Γ ⊢ Δ, ∃x̄.s ≤ t}

2.4 Proof search

Now that we have presented the sequent calculus of Seduct it remains to be explained how Seduct searches for a proof. The basic idea is the following: In order to prove a formula F, we start with the sequent [ ] ⊢ [F] and try to construct a sequent proof for this sequent. This proof is constructed backwards by recursively applying rules to reduce the as yet open leaves in the proof tree. The process stops when either all leaves are established as axioms or else there is a leaf such that no more rule can be applied to it. However, in order to minimize the lack of completeness inherent in the γ rules implemented in Seduct, the order in which the rules are applied is crucial. We use the following order:

– α rules, δ rules, distribution rules, and ι rules,

– β rules,

– γ rules.

The γ rules have to come last, since their application might destroy the completeness of the search strategy. This is due to the fact that for a γ rule the premise is not equivalent to the conclusion. β rules come second last since they are responsible for the branching in the proof tree. A premature application of a β rule can result in a considerable increase in the complexity of the resulting proof. The order of application of the other rules is not important from the point of view of automatic theorem proving. However, in order for sequent proofs to be readable to humans it is useful to apply the rules in a fashion that the intuitionistic character of a sequent is preserved as long as possible. A sequent Γ ⊢ Δ is called intuitionistic if Δ contains at most one element.

As we have already mentioned, we restrict the application of γ rules so that these rules need only be applied in circumstances occurring very rarely in the practice of software verification. Furthermore, the user has the option to instantiate universally quantified axioms directly in order to prevent a proof attempt from failing.

3 Term Rewriting Techniques

The capabilities of the sequent calculus to recognize a sequent as an axiom are rather limited. Therefore we have connected the sequent calculus to a rewrite tool in order to facilitate this task. This rewrite tool is called when a sequent can not be processed any further by the sequent calculus. Since rewriting techniques are only useful when dealing with equations, we have to do some preprocessing of the formulae of these sequents.

3.1 Preprocessing

There are three preprocessing steps that have to be carried out before a sequent can be offered to the rewrite tool:

1. Every negated prime formula ¬P is replaced by the equation P = false.

2. Every prime formula P is replaced by the equation P = true.

3. Every inequality s ≤ t is replaced with the equation min(s, t) = s.

(Here a prime formula is a formula of the form p(t_{1}, ⋯, t_{n}) where the predicate symbol p is neither equal to “=” nor to “≤”.) Only the last of these preprocessing steps requires an explanation, which will be given in the subsection dealing with the handling of inequalities.

If Γ ⊢ Δ is a sequent to be proved by the rewrite tool, then we know that no rule from the sequent calculus is applicable to this sequent. Therefore, after the preprocessing, the resulting sequents have a certain normal form:

– The succedent Δ consists solely of, possibly existentially quantified, conjunctions of equations. These will be called targets in the following.

– The antecedent Γ consists solely of, possibly universally quantified, conditional equations.

Here, a conditional equation has the form^{1} ∀(E_{1} ∧ ⋯ E_{n} ⇒ l = r),

1 For a formula F, we denote the universal closure of F with ∀(F), the existential closure is written ∃(F).

where for all i ∈ {1, ⋯, n} the formula E_{i} is an equation.

We want to turn these conditional equations into conditional rewrite rules. A conditional equation C ⇒ l = r is called a conditional rewrite rule or, for short, a rewrite rule, iff the following is satisfied:

– The condition C is a conjunction of equations.

– Every variable appearing in the condition C also appears in l, i.e., we have FV (C) ⊆ FV (l).

– Every variable appearing on the right hand side r also appears in l, i.e. we

have,

FV (r) ⊆ FV (l).

– We do not have l <_{lex} r.^{2}

If we want to emphasize that a conditional equation C ⇒ l = r is a rewrite rule we will use the notation C ⇒ l → r. In order to turn a conditional equation C ⇒ s = t into a rewrite rule, we first inspect, whether s <_{lex} t or t <_{lex} s holds. In the first case, we take C ⇒ t → s as rewrite rule, in the second we take C ⇒ s → t, and if neither s <_{lex} t nor t <_{lex} s holds, we will take both. However, in this case we have to be aware that C ⇒ s → t and C ⇒ t → s may fail to be rewrite rules due to the requirements on free variables. If a conditional equation C ⇒ s = t satisfies neither FV (t) ⊆ FV (s) nor FV (s) ⊆ FV (t) but if still FV (C) ⊆ FV (s) ∩ FV (t) holds, then there is no problem since then we are able to split this conditional equation by first defining {x_{1}, ⋯, x_{k}} := FV (s)∩FV (t), choosing a new function symbol f_{split} of appropriate arity, and finally taking

C ⇒ s → f_{split}(x_{1}, ⋯, x_{k}) and C ⇒ t → f_{split}(x_{1}, ⋯, x_{k})

as new conditional rewrite rules. (A justification for this procedure can be found in, e.g., [KB70].) If FV (C) ⊆ FV (s) ∩ FV (t) does not hold, then we substitute the variables responsible for this failure by dummy variables.

To summarize, we are now left with a set R′ of universally quantified conditional rewrite rules resulting from the antecedent of the sequent to be proved and a set E′ of existentially quantified conjunctions of equations. We drop the universal and existential quantifiers and call the resulting sets R and E respectively. We will denote the elements of E as targets to be solved, since in order to prove that our original sequence is valid we have to prove that there is a target s_{1} = t_{1} ∧ ⋯ ∧ s_{n} = t_{n} such that

R ⊧ ∃x̄.s_{1} = t_{1} ∧ ⋯ ∧ s_{n} = t_{n} with x̄ = FV (s_{1}, ⋯, s_{n}, t_{1}, ⋯, t_{n}).

In order to carry out this proof we use ordered conditional rewriting. We proceed by explaining some of the basic notions of rewriting. However, in order to save space our exposition will be rather short and incomplete. For a more detailed presentation we refer the reader to the book by L. Bachmair [Bac91] or to [Der90].

2 The lexicographic path ordering <_{lex} will be discussed in the next subsection.

3.2 Basic notions of rewriting

The set of all terms is denoted by T (F, V), where F denotes the set of all function symbols used to build terms, while V is the set of all variables. Terms are denoted by lower case Latin letters like l, r, s, t, and w. The set of all variables occurring in a term t is written as F V (t). We use lower case Greek letters like σ and μ to denote substitutions. If s and t are terms and σ is a substitution such that sσ ≡ tσ, then σ is called a unifier of s and t. The most general unifier of s and t is denoted by mgu(s, t). We write s ≡ t if we want to express that s and t denote the same term.

The set of positions of a term t is denoted by O(t). A position of t is a list of natural numbers that can be interpreted as the address of a subterm of t. If s and t are terms and u ∈ O(t) is a position in t then t/u denotes the subterm of t at position u and t[u ← s] denotes the term constructed by replacing this subterm with s. A non–variable position in a term t is a position u ∈ O(t), such that t/u is not a variable.

To ensure that there are no infinite sequences of rewrite operations we have to use well–founded orderings. In our experiments we found that the lexicographic path ordering [Bac91, Der90] is the ordering most appropriate. If < is a partial order on function symbols, then <_{lex} will denote the corresponding lexicographic path ordering on terms. For a definition, we refer to the literature.

An ordered conditional rewrite system is a pair ⟨R, <⟩ where R is a set of conditional equations and < is a partial order on the set F of function symbols. A conditional rewrite system gives rise to the notion of conditional simplification.

Definition 1 Ordered conditional simplification. If ⟨R, <⟩ is an ordered conditional rewrite system then, using ⟨R, <⟩, a term s can be simplified in one step to a term t, written

s →_{R} t,

iff there exists a position u ∈ O(s), a rule (s_{1} = t_{1} ∧ ⋯ ∧ s_{n} = t_{n} ⇒ l = r) ∈ R, and a substitution σ such that

1. s/u ≡ lσ, t ≡ s[u ← rσ], rσ <_{lex} lσ, and

2. for all i ∈ {1, ⋯, n} there exists a term w_{i} such that

s_{i} →_{R}^{∗} w_{i} and t_{i} →_{R}^{∗} w_{i}.

Here →_{R}^{∗} denotes the reflexive and transitive closure of →_{R}.

Due to the well–foundedness of <_{lex} the relation →_{R} is well–founded. A set of conditional rewrite rules can be enlarged by building critical pairs.

Definition 2 Conditional critical pairs. If C_{1} ⇒ l_{1} → r_{1} and C_{2} ⇒ l_{2} → r_{2} are rewrite rules such that:

1. u ∈ O(l_{1}) is a position pointing to a non–variable subterm l_{1}/u.

2. The subterm l_{1}/u and the term l_{2} are unifiable via the most general unifier μ = mgu(l_{1}/u, l_{2}).

3. We have neither l_{1}μ <_{lex} r_{1}μ nor l_{2}μ <_{lex} r_{2}μ.

Then C_{1}μ ∧ C_{2}μ ⇒ ⟨l_{1}[u ← r_{2}]μ, r_{1}μ⟩ is called a conditional critical pair.

Since the targets in E we want to prove are implicitly existentially quantified, trying to solve them by mere rewriting is not enough, we might have to instantiate some of them. We achieve this via the concept of narrowing. However, in contrast to the classical approach we define the notion of narrowing not for equations but rather for targets.

Definition 3 Narrowing. If C_{1} ⇒ l → r is a rule from R and C_{2} ∧ s = t ∧ C_{3} is a target from E such that

1. u ∈ O(s) is a position pointing to the non–variable subterm s/u in s,

2. the subterm s/u and the term l are unifiable via the most general unifier μ = mgu(s/u, l), and

3. we do not have lμ <_{lex} rμ.

then the target C_{2} ∧ s = t ∧ C_{3} can be narrowed via R into the target C_{1}μ ∧ C_{2}μ ∧ s[u ← r]μ = tμ ∧ C_{3}μ.

The logical connection between the original target and the new target derived from this via narrowing is the following: If we are ever able to solve the new target, then we have shown the original target to be solvable also.

3.3 Description of the rewrite tool

Now we are in a position to describe the control of our rewrite tool. We will give the algorithm as a pseudo program. This program uses four different variables which are described first:

Rc: A set of conditional rewrite rules such that all critical pairs between two

rules from this set have been computed and added to the set Ru. Ru: A set of conditional rewrite rules which are not yet used for narrowing and

the building of critical pairs. Rn: A set of conditional rewrite rules used to store intermediate results. Ec: A set of targets, such that every target in it has already been narrowed with

all rules from Rc. Eu: A set of targets not yet used for narrowing. En: A set of targets used to store intermediate results.

The program is given in figure 1. It accepts as inputs a set R of conditional rewrite rules and a set E = {C_{1}, ⋯, C_{n}} of targets. The program is intended to return true if it has been able to show that

R ⊧ ∃(C_{1}) ∨ ⋯ ∨ ∃(C_{n})

holds true.

To complete the description of the program we explain the procedures which are used.

Rc := ∅; Ru := R; Ec := ∅; Eu := E; while Ru ∪ Eu ≠ ∅ do;

choose an element e ∈ Ru ∪ Eu;

if e ∈ Eu then
begin

En := narrow( {e}, Rc ); Ec := Ec ∪ {e}; Eu := (Eu −{e}) ∪ En;

end;
if e ∈ Ru then
begin
Rn := critical-pairs( e, Rc );

En := narrow( Ec, {e} ); Rc := Rc ∪ {e}; Ru := (Ru −{e}) ∪ Rn; Eu := En ∪ Eu;

end;
if check-targets( Ec ∪ Eu ) then return true;
end-while;
return false;

Fig. 1. The rewrite tool.

– The function critical-pairs( r, Rs ) builds all critical pairs between the conditional rewrite rule r and the rules from the set Rs. These critical pairs are then turned into rewrite rules.

– The function narrow( Es, Rs ) computes the set of all targets resulting from narrowing a target in Es with a rule from Rs.

– The predicate check-targets( Es ) checks, whether any of the targets from Es is trivially true. A target is trivially true if it is the empty conjunction. Furthermore, this predicate cleans up all targets by removing trivial equations of the form s = s.

As it stands, the description of the algorithm we have implemented is not complete since we have left out the simplification steps. Basically, we keep the sets Ec and Rc reduced; all targets from Ec, all right hand sides of rewrite rules from Rc, and all conditions of rewrite rules from Rc are in normal form with respect to Rc. We could also reduce everything with respect to the larger set Rc ∪ Ru, but this strategy proved to be too expensive in terms of computation time.

The algorithm described above can have three different results: It can produce either the result “true” or the result “false” or it can fail to terminate. The result “true” guarantees that the sequence in question is indeed true. The result “false” on the other hand does not necessarily imply the falseness of the sequent in question. This is due to the incompleteness of our calculus introduced by the γ rules. However, the experience gained so far shows that this incompleteness is not a problem in practice. This is explained by the fact that the axioms used in a proof carried out during program verification are more or less direct translations of the definition of functions used in the program subject to scrutiny. When using a functional programming style, these translations can always be written as conditional equations so that no γ rules need to be applied.

3.4 How to implement the freeness axioms

If a sort S is freely generated by the constructor functions f_{1}, ⋯, f_{n}, then we have three kinds of axioms. First there are the injectivity axioms stating that all constructor functions are injective: For all i ∈ {1, ⋯, n} we have

f_{i}(x_{1}, ⋯, x_{k}) = f_{i}(y_{1}, ⋯, y_{k}) ⇒ x_{1} = y_{1} ∧ ⋯ ∧ x_{k} = y_{k},

where k is the arity of f_{i}. If we happen to deduce a conditional equation of the form

C ⇒ f_{i}(s_{1}, ⋯, s_{k}) = f_{i}(t_{1}, ⋯, t_{k})

where k is the arity of f_{i}, then because of the injectivity axioms we can add the following conditional equations:

C ⇒ s_{1} = t_{1}, ⋯, C ⇒ s_{k} = t_{k}.

These equations are logically stronger than the original equation.

Secondly, we have the so called disjointness axioms, which take the form

f_{i}(x_{1}, ⋯, x_{k}) ≠ f_{j}(y_{1}, ⋯, y_{l}) if i ≠ j.

Here k is the arity of f_{i} while l is the arity of f_{j}. If we happen to deduce a conditional equation of the form

C ⇒ f_{i}(s̄) = f_{j}(t̄)

such that i ≠ j, then instead of transforming this conditional equation into a rewrite rule, we just add the conjunction C as a new target. This is due to the fact that f_{i}(s̄) = f_{j}(t̄) is inconsistent in the presence of the disjointness axioms. Therefore, if we find an instantiation satisfying the condition C, then we have deduced a contradiction from our set of rewrite rules. This means that the antecedent of the sequent we are trying to prove is contradictory. However, this implies that the sequent under investigation is trivially valid.

Finally, there is a completeness axiom describing the fact that all elements of the sort S can be generated by the constructors f_{1}, ⋯, f_{n}. This axiom has the form

∀x.(∃ȳ_{1}.x = f_{1}(ȳ_{1}) ∨ ⋯ ∨ ∃ȳ_{n}.x = f_{n}(ȳ_{n})).

This axiom is dealt with by an appropriate structural induction rule which has been integrated into the command language of Seduct.

3.5 How to handle reflexivity, antisymmetry, and transitivity of ≤

The inequality symbol ≤ is supposed to represent a linear order. Therefore it has to be interpreted by a binary relation which is reflexive, antisymmetric, transitive, and linear. The linearity of ≤ has already taken care of by the ι rules of the sequent calculus. We can simulate the other three properties by adding the following set of equations as axioms:

Idempotence: min(x, x) = x.
Commutativity: min(x, y) = min(y, x).
Associativity: min(min(x, y), z) = min(x, min(y, z)).

Now the reflexivity of ≤ is reflected by the idempotence of min, antisymmetry is reflected by commutativity, and transitivity by associativity. To increase the efficiency of our tool, we do not add the three equations above directly but rather compile them into a confluent set of rules by using a version of the unfailing Knuth–Bendix algorithm [HR87].

4 The Command Language of Seduct

In this section we will present some of the basic ideas of the command language [SBN94] of Seduct. This is most easily achieved by presenting an example session with Seduct. We have chosen to illustrate some features of the command language by proving part of the correctness of the merge–sort algorithm. To begin our proof, we first have to define the signature of our language. This is done via the following declare section.

    begin( declare ).
       []:          list.                       %  Empty list.
       '.':         [ element, list ] -> list.  %  Cons operator.
       merge:       [ list, list ] -> list.
       split1:      [ list ] -> list.
       split2:      [ list ] -> list.
       merge_sort:  [ list ] -> list.
       sorted:      [ list ] -> bool.
       =<< :        [ element, list ] -> bool.
    end( declare ).

We have used the dot “.” as constructor for lists since this enables us to use Prolog list notation.^{3} The function merge takes two sorted list and splices them together to produce another sorted list. split1 and split2 are used to decompose a list into two parts; if l = [ a1, a2, a3, ⋯], then

        split1( l ) = [ a2, a4, a6, · · · ], while
        split2( l ) = [ a1, a3, a5, · · · ].

merge sort is a function to sort lists, sorted is a unary predicate denoting

3 In Prolog a term of the form '.'(X,Xs) can be written as [X|Xs].

that a list is sorted. To define sorted we need the binary predicate =<<. For an element x and a list l, x =<< l holds true iff l is either empty or x is less than or equal to the first element of l. To be able to use prefix and infix notation for some of the functions and predicates defined we use the following operator declarations:

    op( 1, xfx, merge ).
    op( 5, fx, split1 ).               op( 10, fx, sorted ).
    op( 5, fx, split2 ).               op( 10, xfx, =<< ).

These declarations declare split1, split2, and sorted as prefix operators, while merge and =<< are declared infix. Furthermore, the operator merge binds stronger than the operators split1 and split2, which in turn bind stronger

than sorted and =<<.

The definition of the functions and predicates used in the merge–sort algorithm are given in figure 2. There are two properties of the merge–sort algorithm which have to be proved in order to verify its partial correctness. First, we have to show that the result of merge–sorting a list is indeed sorted and secondly we should prove that the merge–sort algorithm returns as output the same elements that have been given to it as input. We will confine ourselves to the proof of the first property. In order to carry out this proof, we have to show two lemmata. These lemmata state how the predicates sorted and =<< distribute over the function merge. These lemmata and our original theorem are introduced as goals in the following goal section:

begin( goals ).
    lemma_1: forall  x: element;
                     l1, l2: list;
             in
                  x =<< l1 merge l2  <-->  x =<< l1 & x=<< l2
             end.
    lemma_2: forall  l1, l2: list;
             in
                  sorted(l1 merge l2)  <-->  sorted l1 & sorted l2
             end.
    theorem: forall  l: list;
             in
                  sorted merge_sort( l )
             end.
end( goals ).

Now we are ready to start the proof of lemma 1. This proof is initiated by the command

    prove( lemma 1 ).

We want to perform this proof via computational induction [BM79] with respect to the definition of the function merge. This is achieved via the command

    computational induction( merge ).

begin( definitions ).
merge_1:  forall l: list;
in     [] merge l = l
end.
merge_2:  forall l: list;
in     l merge [] = l
end.
merge_3:  forall x, y: element;
       l1, l2: list;
in     [ x | l1 ] merge [ y | l2 ] =
       if  x =< y  then [ x | l1 merge [ y | l2 ] ]
                   else [ y | [ x | l1 ] merge l2 ]
       fi
end.
split1_1: split1  [] = [].
split1_2: forall  x: element, l: list;
in      split1 [ x | l ] = split2 l
end.
split2_1: split2  [] = [].
split2_2: forall  x: element; l: list;
in      split2 [ x | l ] = [ x | split1 l ]
end.
merge_sort_1:  merge_sort( [] ) = [].
merge_sort_2:  forall x: element;
  in     merge_sort( [ x ] ) = [ x ]
  end.
merge_sort_3:  forall l: list;
  in
      merge_sort( l ) =
      merge_sort(split1 l) merge merge_sort(split2 l)
  end.
'=<<_1':  forall  x: element;
in      x =<< []
end.
'=<<_2':  forall x, y: element; l: list;
in     x =<< [ y | l ]  <-->  x =< y
end.
ord_1:  sorted [].
ord_2:  forall x: element; l: list;
in     sorted [ x | l ]  <-->  x =<< l & sorted l
end.
end( definitions ).

Fig. 2. Definition of the merge–sort algorithm.

Since the definition of the function merge contains an if operator, it is first internally expanded into the following equivalent clauses:

  [] merge l = l.
  l merge [] = l.
  a =< b  ->  [a|l1] merge [b|l2] = [ a | l1 merge [b|l2] ].
  not a =< b  ->  [a|l1] merge [b|l2] = [ b | [a|l1] merge l2 ].

Proving a formula F( l1, l2, l1 merge l2 ) via computational induction along the definition of merge will generate the following subgoals:

    1. F( [], l, l ).
    2. F( l, [], l ).
    3. a =< b & F( l1, [b|l2], l1 merge [b|l2] )  ->
               F( [a|l1], [b|l2], [ a | l1 merge [b|l2] ] ).
    4. not a =< b & F( [a|l1], l2, [a|l1] merge l2 )  ->
                   F( [a|l1], [b|l2], [ b | [a|l1] merge l2 ] ).

In the case of lemma 1 the form of F( l1, l2, l1 merge l2 ) happens to be:

    x =<< l1 merge l2  <-->  x =<< l1 & x=<< l2.

This means that, in order to show lemma 1 via computational induction, we have to prove the following subgoals:

 1. x =<< l <--> x =<< [] & x =<< l
 2. x =<< l <--> x =<< l & x =<< []
 3. a =< b  &
    (x =<< l1 merge [b|l2] <--> x =<< l1 & x =<< [b|l2])  ->
    (x =<< [a | l1 merge [b|l2]] <--> x =<< [a|l1] & x =<< [b|l2])
 4. not a =< b  &
    (x =<< [a|l1] merge l2 <--> x =<< [a|l1] & x =<< l2)  ->
    (x =<< [b | [a|l1] merge l2] <--> x =<< [a|l1] & x =<< [b|l2])

Now all of these subgoals can be solved by the command expand go. This command works in two stages:

– First it expands all definitions available in the subgoal to be proved. This expansion is done using contextual rewriting. This notion is best explained via an example. If the system contains the definition

   (*)     h(x) = h(a) -> f(x) = g(x)

and the goal to be proved contains the subformula

           a = b -> p(f(b)),

then this subformula can be reduced to

           a = b -> p(g(b))

since the condition h(b) = h(a) of the definition (*) is valid in the context

   a = b.

– After the subgoal has been normalized by contextual rewriting, the simplified subgoal is relegated to the proof engine described previously.

We illustrate the expand go command with an example: Using this command, the fourth subgoal from the inductive proof of lemma 1 is first simplified into

 not a =< b & (x =<< [a|l1] merge l2  <-->  x =< a & x =<< l2)  ->
              (x =< b  <-->  x =< a & x =< b)

This formula is then easily proven by the sequent calculus of Section 2 in collaboration with the term rewriting techniques described in Section 3. The complete proof of lemma 1 looks as follows:

    prove( lemma_1 ).
        computational_induction( merge ).
            expand_go.
            expand_go.
            expand_go.
            expand_go.

We can collect the insight we have gained while proving lemma 1 in the definition of a parameterized macro:

    macro( automatic_merge_induction, name ).
        prove( name ).
            computational_induction( merge ).
                expand_go.
                expand_go.
                expand_go.
                expand_go.
    end( automatic_merge_induction ).

Our next goal, lemma 2, can be proved by this macro without further interaction. The proof looks as follows:

        automatic merge induction( lemma 2 ).

This justifies the definition of the macro. Finally, we prove our main theorem theorem via computational induction along the definition of merge sort:

        prove( correctness ).
             computational induction( merge sort ).
                   expand go. expand go. expand go.

Since the definition of merge sort contains three clauses, three subgoals are generated, which can all be proved automatically via the expand go command. The complete proof of the two lemmata and the theorem can be written as follows:

    automatic_merge_induction( lemma_1 ).
    automatic_merge_induction( lemma_2 ).
    prove( correctness ).
        computational_induction( merge_sort ).
            expand_go.  expand_go.  expand_go.

From our point of view, this is quite concise. This form of a proof is what we have termed an abstract proof. We have found these proofs to be easily communicable.

Having gained some experience in software verification our impression is that constructing abstract proofs is not very difficult or tedious, provided of course that one has a thorough understanding of the problem at hand. This “understanding” normally amounts to the ability to formulate appropriate lemmata. Often, these lemmata take the form of distribution laws: They show how one notion correlates with another notion. For example, lemma 2 shows how sorted distributes over merge.

5 Conclusion

This paper describes the proof compiler Seduct and discusses several aspects of its implementation. Seduct has been designed to economically verify proof obligations arising in software verification. Since Seduct has been finished only recently, we have only tested our approach with the verification of a few selected algorithms. The most extensive of these tests was the proof of the correctness of an algorithm for Boolean unification [Nie94, BS87] based on BDD [Bry86] techniques. During this work we made the following observations:

– Our combination of a sequent calculus with rewrite techniques is well suited for the discharge of proof obligations arising during software verification. This is due to the following facts:

• The sequent calculus possesses the subformula–property: any formula produced during the proof is a subformula of the original formula. This makes it possible to trace the origin of any formula arising in the proof.

• Our version of ordered conditional rewriting together with the slight variation on the theme of narrowing seems to be quite efficient in practice.

• It has been possible to hard–wire certain often occurring axioms like the

freeness axioms and the axioms describing a linear order.

– Although our command language is by far not as powerful as a programming language: there is no way of programming tactics in Seduct, it seems to be powerful enough to control the automatic proof engine of Seduct satisfactorily. The features most valuable proved to be:

• The expand go command which performs a context dependent conditional rewriting before relegating the proof obligation to the proof engine.

• Parameterized macros provide a very convenient way of automatizing certain parts of a proof. Inductions can often be done automatically with the help of appropriately defined parameterized macros.

• The implementation of computational induction proved to be invaluable in reducing the complexity of proofs which otherwise would become prohibitively tedious.

• Last but not least, in contrast to other interactive tactic based theorem provers our command language is very simple to comprehend and to use.

Seduct has also been used in collaboration with Kiv (Karlsruhe Interactive Verifier) [HRS90, Rei95]. Here Seduct was used for the discharge of first order proof obligations which had been generated in a proof of the correctness of an algorithm for Boolean unification with Kiv. Our experience was quite encouraging: Discharging these obligations with Seduct took only a quarter of the time than what was needed with Kiv.

Acknowledgment: Seduct has benefited from several contributions. The following people were involved in coding Seduct: Claus Bendix Nielsen, Sabine Glesner, Volkmar Lotz, Hans–Albert Schneider, and James van Welzen.

References

[Bac91] Leo Bachmair. Canonical Equational Proofs. Birkhäuser Boston, Inc., Boston, MA, 1991.

[BM79] R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, Orlando, Florida, 1979.

[Bry86] R. E. Bryant. Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 35(8):677–691, 1986.

[BS87] W. Büttner and H. Simonis. Embedding Boolean expressions into logic programming. Journal of Symbolic Computation, 4:191–205, October 1987.

[Der90] Nachum Dershowitz. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, chapter 6, pages 243–320. Elsevier Science Publishers, 1990.

[Gal86] J. Gallier. Logic for Computer Science. Harper & Row, New York, 1986.

[GG91] Stephen J. Garland and John V. Guttag. A guide to LP, the Larch Prover. Report 82, DEC Systems Research Center, Palo Alto, CA, December 1991.

[HR87] Jieh Hsiang and Michaël Rusinowitch. On word problems in equational theories. In Thomas Ottmann, editor, Automata, Languages and Programming, volume 267 of Lecture Notes in Computer Science, pages 54–71. Springer– Verlag, 1987.

[HRS90] M. Heisel, W. Reif, and W. Stephan. Tactical theorem proving in program verification. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 117–131. Springer Verlag, 1990.

[KB70] Donald E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, Oxford, 1970.

[Nie94] Claus Bendix Nielsen. Boolean unification: a case study in verification with Seduct. Technical report, Siemens AG, Corporate Research and Development, 81730 Munich, Germany, 1994.

[Rei95] W. Reif. The Kiv–approach to software verification. This volume.

[SBN94] Karl Stroetmann and Claus Bendix Nielsen. A Guide to Seduct. Siemens AG, Munich, Germany, second edition, 1994.

[Smu68] R. M. Smullyan. First Order Logic. Springer Verlag, 1968.

This article was processed using the L^{A}TEX macro package with LLNCS style