3 Calculus and Proof Procedure

E is a purely equational theorem prover, based on ordered paramodulation and rewriting. As such, it implements an instance of the superposition calculus described in [BG94]. We have extended the calculus with some stronger contraction rules and more general approach to literal selection. The proof procedure is a variant of the given-clause algorithm.

3.1 Calculus

Term(F,V ) denotes the set of (first order) terms over a finite set of function symbols F (with associated arities) and an enumerable set of variables V. We write t|p to denote the subterm of t at a position p and write t[p t] to denote t with t|p replaced by t. An equation s t is an (implicitly symmetrical) pair of terms. A positive literal is an equation s t, a negative literal is a negated equation s ⁄≃t. We write s≃˙t to denote an arbitrary literal3. Literals can be represented as multi-sets of multi-sets of terms, with s t represented as {{s},{t}} and s ⁄≃t represented as {{s,t}}. A ground reduction ordering > is a Noetherian partial ordering that is stable w.r.t. the term structure and substitutions and total on ground terms. > can be extended to an ordering > l on literals by comparing the multi-set representation of literals with > >> > (the multi-set-multi-set extension of >).

Clauses are multi-sets of literals. They are usually represented as disjunctions of literals, s1˙≃t1 s2˙≃t2sn˙≃tn. We write Clauses(F,P,V ) to denote the set of all clauses with function symbols F, predicate symbols P and variable V . If C is a clause, we denote the (multi-)set of positive literals in C by C+ and the (multi-)set of negative literals in C by C

The introduction of an extended notion of literal selection has improved the performance of E significantly. The necessary concepts are explained in the following.

Definition 3.1 (Selection functions) sel : Clauses(F,P,V ) Clauses(F,P,V ) is a selection function, if it has the following properties for all clauses C:

We say that a literal L is selected (with respect to a given selection function) in a clause C if L sel(C).

We will use two kinds of restrictions on deducing new clauses: One induced by ordering constraints and the other by selection functions. We combine these in the notion of eligible literals.

Definition 3.2 (Eligible literals) Let C = LR be a clause, let σ be a substitution and let sel be a selection function.

The calculus is represented in the form of inference rules. For convenience, we distinguish two types of inference rules. For generating inference rules, written with a single line separating preconditions and results, the result is added to the set of all clauses. For contracting inference rules, written with a double line, the result clauses are substituted for the clauses in the precondition. In the following, u, v, s and t are terms, σ is a substitution and R, S and T are (partial) clauses. p is a position in a term and λ is the empty or top-position. Different clauses are assumed to not share any common variables.

Definition 3.3 (The inference system SP) Let > be a total simplification ordering (extended to orderings > L and > C on literals and clauses) and let sel be a selection function. The inference system SP consists of the following inference rules:

We write SP(N) to denote the set of all clauses that can be generated with one generating inference from I on a set of clauses N, DSP to denote the set of all SP-derivations, and DSP to denote the set of all finite SP-derivations.

As SP only removes clauses that are composite with respect to the remaining set of clauses, the calculus is complete. For the case of unit clauses, it degenerates into unfailing completion [BDP89] as implemented in DISCOUNT. E can also simulate the positive unit strategy for Horn clauses described in [Der91] using appropriate selection functions.

Contrary to e.g. SPASS, E does not implement special rules for non-equational literals or sort theories, as we expect this part to be taken care of by SETHEO in a later combined system. Instead, non-equation literals are encoded as equations and dealt with accordingly.

3.2 Proof Procedure


# Input: Axioms in U, P is empty

while U = begin

c := select(U)

U := U \ c

# Apply (RN), (RP), (NS), (PS), (CSR), (DR), (DD), (DE)

simplify(c,P)

# Apply (CS), (ES), (TD)

if c is trivial or subsumed by P then

# delete(c)

else if c is the empty clause then

# Success: Proof found

stop

else

T := # Temporary clause set

foreach p P do

if c simplifies p

P := P \ p

T := T p

done

end

T := T e-resolvents(c) # (ER)

T := T e-factors(c) # (EF)

T := T paramodulants(c,P) # (SN), (SP)

foreach p T do

# Apply efficiently implemented subset of (RN),

# (RP), (NS), (PS), (CSR), (DR), (DD), (DE)

p := cheap_simplify(p, P)

# Apply (TD) or efficient approximation of it

if p is trivial

delete(p)

else

U := U cheap_simplify(p, P)

fi

end

fi

end

# Failure: Initial U is satisfiable, P describes model


Figure 1: Main proof procedure of E

Fig. 1 shows a (slightly simplified) pseudocode sketch of the quite straightforward proof procedure of E7. The set of all clauses is split into two sets, a set P of processed clauses and a set U of unprocessed clauses. Initially, all input clauses are in in U, and P is empty. The algorithm selects a new clause from U, simplifies it w.r.t. to P, then uses it to back-simplify the clauses in P in turn. It then performs equality factoring, equality resolution and superposition between the selected clause and the set of processed clauses. The generated clauses are added to the set of unprocessed clauses. The process stops when the empty clause is derived or no further inferences are possible.

The proof search is controlled by three major parameters: The term ordering (described in section 4.2), the literal selection function, and the order in which the select operation selects the next clause to process.

E implements two different classes of term orderings, lexicographic term orderings and Knuth-Bendix orderings. A given ordering is determined by instantiating one of the classes with a variety of parameters (described in section 4.2).

Literal selection currently is done according to one of more than 50 predefined functions. Section 4.3 describes this feature.

Clause selection is determined by a heuristic evaluation function, which conceptually sets up a set of priority queues and a weighted round robin scheme that determines from which queue the next clause is to be picked. The order within each queue is determined by a priority function (which partitions the set of unprocessed clauses into one or more subsets) and a heuristic evaluation function, which assigns a numerical rating to each clause. Section 4.1 describes the user interface to this mechanism.

3Non-equational literals are encoded as equations or disequations P(t1,,tn)≃˙. In this case, we treat predicate symbols as special function symbols that can only occur at the top-most positions and demand that atoms (terms formed with a top predicate symbol) cannot be unified with a first-order variable from V , i.e. we treat normal terms and predicate terms as two disjoint types.

4A stronger version of (RP) is proven to maintain completeness for Unit and Horn problems and is generally believed to maintain completeness for the general case as well [Bac98]. However, the proof of completeness for the general case seems to be rather involved, as it requires a very different clause ordering than the one introduced [BG94], and we are not aware of any existing proof in the literature. The variant rule allows rewriting of maximal terms of maximal literals under certain circumstances:

(RP’)

s t u v R


s t u[p σ(t)] v R
if u|p = σ(s), σ(s) > σ(t) and if u v is not eligible for resolution or u > v or p = λ or σ is not a variable renaming.

This stronger rule is implemented successfully by both E and SPASS [Wei99].

5In practice, this rule is only applied if σ(s) and σ(t) are >-incomparable – in all other cases this rule is subsumed by (RN) and the deletion of resolved literals (DR).

6This rule can only be implemented approximately, as the problem of recognizing tautologies is only semi-decidable in equational logic. Current versions of E try to detect tautologies by checking if the ground-completed negative literals imply at least one of the positive literals, as suggested in [NN93].

7Note that the proof procedure has been further simplified for version 0.8 and up. The pseudo-code describes the current version.