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.

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)) % DMThis 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]).

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.

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.

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.