OTTER Encapsulated

Consider the following simple ``natural deduction" style proof in the propositional calculus of the fact that from a conditional $p \rightarrow q$ one can derive $\neg q \rightarrow \neg p$ (this move is known as contraposition or transposition).

1.

$p \rightarrow q$ (given)

2.

$\neg q$ (assumption)

3.

$\neg p$ (modus tollens, lines 1 and 2)

4.

$\neg q \rightarrow \neg p$ (lines 2-3, conditional proof)

This is the sort of simple proof that students of logic learn at the outset of their education. Notice the use of three rules in this little proof: assumption, modus tollens, and conditional proof. Normally, many such rules are added to the arsenal of the human who learns to do proofs in first-order logic. By contrast, OTTER really only has, at bottom, one rule: resolution. Here is an actual OTTER input file for the problem of finding a proof of transposition:

% This propositional logic problem, by the way, was the
% "most difficult" (!) theorem proved by the original
% Logic Theorist of 1957.

set(auto).

formula_list(usable).

-((p -> q) <-> (-q -> -p)).

end_of_list.

The lines that begin with the character % are comments (and they may well reveal how far theorem proving has come in just over four decades!). The line set(auto). simply tells OTTER to attack the problem ``autonomously" as it sees fit, without using any particular strategies. There then follows a list flanked top and bottom by formula_list(usable). and end_of_list; in this case the list only has one element, viz., -((p -> q) <-> (-q -> -p)).⁶ This is the negation of the theorem to be proved. The theorem is negated because if OTTER can derive a contradiction from this negation conjoined with consistent information given it, it will follow by indirect proof that transposition is valid. OTTER does indeed find such a proof instantaneously; here is the actual output.

---------------- PROOF ----------------

1 [] -p|q.
2 [] -q.
3 [] p.
4 [hyper,3,1] q.
5 [binary,4.1,2.1] $F.

------------ end of proof -------------

Lines 1, 2, and 3 represent the result of reformulating the formula

$$\mbox{{\tt -((p -> q) <-> (-q -> -p))}}$$

in clausal form. The formula -((p -> q) <-> (-q -> -p)) is therefore equivalent to the conjunction of -p|q, -q, and p. (A truth table will reveal that this conjuction is true and false under exactly the same truth-value assignments to p and q as -((p -> q) <-> (-q -> -p)) is.) Each of these conjucts is composed of a disjunction of literals, where a literal is either a propositional letter (in which case it is said to be positive) or the negation of one (in which case it's said to be negative). Lines 4 and 5 in the OTTER proof are applications of the rules of inference `binary resolution' and `hyperresolution,' respectively. These rules are really quite straightforward. Binary resolution for the propositional case is just

$$\begin{array}{c} \phi \vee \psi \quad \neg\psi\\ \hline \phi \end{array}$$

where the formula below the horizontal line is inferred from the formulas above the line. (The greek letters here stand for arbitrary formulas in the propositional calculus.) You should be able to see now, after looking at this rule, why the inference in line 5 of the OTTER proof goes through. Hyperresolution is a little more complex. To understand it, notice that each disjunction of literals, e.g., p|q|r|-s, can be viewed as a set; this particular disjunction would become { $p, q, r, \neg s\}$. Now, intuitively, hyperresolution simply says that contradictory literals are cancelled out to leave positive literals. In line 4 of the above OTTER proof, for example, p in line 1 and -p in line 3 contradict each other and cancel out, leaving q. The general schema for hyperresolution is as follows.

$$\begin{array}{ll} \Phi_1 \cup \{\neg\psi_1, \neg\psi_2, \ldo... ...Phi_1 \cup \Phi_ 2 \cup \cdots \cup \Phi_{n+1} &\\ \end{array}$$