Notes on the Otter Proofs and Searches

Back to the Main Page

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.
• 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).
```