Notes on the Otter Proofs and Searches

An Example

    1     [] x = x.
    3     [] x v (x ^ y) = x.
    6,5   [] x ^ y = c(c(x) v c(y)).
    8,7   [] c(c(x)) = x.
    10    [] A ^ (A v B) != A.
    11    [copy,10,demod,6]           c(c(A) v c(A v B)) != A.
    12    [back_demod,3,demod,6]      x v c(c(x) v c(y)) = x.
    33    [para_into,12,7]            x v c(c(x) v y) = x.
    50,49 [para_from,7,33]            c(x) v c(x v y) = c(x).
    53    [back_demod,11,demod,50,8]  A != A.
    54    [binary,53,1]               $F.

This is a trivial proof of an absorption law from its dual.

Proofs are by contradiction.
Lines 2, 3, and 4 are the hypotheses, and line 5 is the denial of the conclusion.
x and y are variables; A and B are constants.
A clause can have two identifiers, e.g., "6,5".
Justifications
- [copy,10,demod,6] -- rewrite clause 10 with clause 6.
- [back_demod,3,demod,6] -- rewrite clause 3 with clause 6.
- [para_into,12,7] -- paramodulation; that is, use (an instance of) clause 7 to make an equtional inference with (an instance of) clause 12.
- [para_from,7,33] -- this is the same as [para_into,33,7].
- [back_demod,11,demod,50,8] -- rewrite clause 11 with clauses 50 and 8.
- [binary,53,1] -- resolve the clauses 53 and 1, giving (in this case) a contradiction.
This is a bidirectional proof; that is, it goes forward from the hypotheses (clauses 12,33,50) and backward from the goal (clauses 11,53) to produce a contradiction.

Autonomous Mode

Otter can be used as a completely automatic theorem prover: the user simply gives a statement of the conjecture. This autonomous mode can be used to prove many of the easy theorems in this work, but some user control is usually necessary for more interesting theorems, and we did not use it here.

Canonicalization

Automated theorem proving with equations nearly always benefits by using equations as rewrite rules to canonicalize expressions. This process is sometimes referred to as demodulation. The user can control the process by giving an ordering on the symbols, which Otter users to determine which equations should be used as rewrite rules and the orientation in which they should be used.

The symbol ordering is especially relevant when equational definitions are present, as in this work. For example, if

    x ^ y = c(c(x) v c(y))

is used as a demodulator, should it be used to eliminate or to introduce meet operations. (As shown, it eliminates them, because Otter always applies demodulators left-to-right.)

When proving definitional equivalence, several definitions typically come into play, because each system defines operations in the other. In such situations, the user can choose the operations to be used for much of the search. The default ordering we are using is

    lex([A, B, C, D, 0, 1, x v x, c(x), x ^ x, f(x, x)]).

The least desirable operations are last in the list (heaviest), so that order will orient the definitions (when present) as follows.

    f(f(x,x),f(y,y)) = x v y.  % DEF_J
    f(f(x,y),f(x,y)) = x ^ y.  % DEF_M
    f(x,x) = c(x).             % DEF_C
    f(x,y) = c(x) v c(y).      % DEF_SS
    x ^ y = c(c(x) v c(y))     % DM

This will rewrite expressions in terms of join and complement when possible. Experience has shown that proofs are usually easier to find in terms of join and complement than in terms of the Sheffer stroke. When we wish to have proofs in terms of the Sheffer stroke, we can use the following ordering.

    lex([A, B, C, D, 0, 1, f(x,x), x v x, c(x), x ^ x]).

Forward Proofs

We usually prefer forward proofs (i.e., direct proofs, ending with the goal) rather than bidirectional proofs. Forward proofs are not only easier to understand, they are sometimes easier to find. The also simplify searches with multiple goals (see the next point).

We can force proofs to be forward by placing the goal in the passive list. This can cause proofs to be missed, however, when the goals are not in the canonical form, because demodulation occurs before the check for a proof. We can sometimes get around this problem by modifying the goal (e.g., expanding a defined term) when we put it in the passive list.

Multiple Goals

We have several ways of handling multiple goals. Say we wish to prove commutativity and idempotence of join. The logically straightforward method is to deny the conjunction, with a clause such as (here the symbol | is disjunction, not the Sheffer stroke)

  A v B != B v A  |  C v C != C.

This, however, causes various subtle problems for Otter. A second method is to simply run two separate Otter jobs.

A third method is to include the two denials as separate statements in the passive list,

  A v B != B v A  |  $Answer(commutativity).
  C v C != C.     |  $Answer(idempotence).

and ask Otter to prove find two contradictions instead of one. The answer literals let the user know what has been proved.

The first method has the advantage of producing a single proof in the output file. The third method has the advantage of letting the user know when any of the goals has been proved. The separate proofs produced by the third method can be merged later for presentation.

Hints

Several of the Otter input files have a hints list. The hints are not used to make inferences; instead, they are used to guide Otter along specific lines of reasoning. In particular if Otter derives a clause that matches a hint, it gives priority to that clause in making further inferences.

Several of the proofs were difficult to find, requiring methods outside the scope of the document [21,22]. In those cases we have given input files containing hints, which guide Otter directly to specific proofs. One can view those jobs as proof-checking rather than proof-finding.

Another use of hints is in finding and presenting shorter proofs. Otter normally does not prefer short proofs; it simply reports the proofs that it finds, and the proofs are frequently much longer than necessary. Several methods have been developed to shorten Otter's proofs [see the work of Larry Wos], and the short proofs are then constructed by using hints.