From the AAR President
Herbrand Award: Call for Nominations
Fascinating XCB Inference
Call for Papers

From the AAR President, Larry Wos...

A long-standing question in propositional logic was answered in 2002 by Larry Wos [2]. The question was whether the formula XCB,

(1)

The problem can be stated easily in first-order logic. Because the pair of axioms {symmetry, transitivity} is a basis for EC, the following clauses represent the problem (x, y, z are variables, and a, b, c are constants).

    -P(e(x,y)) | -P(x) | P(y).      % condensed detachment
    P(e(x,e(e(e(x,y),e(z,y)),z))).  % XCB
    -P(e(e(a,b),e(b,a))) | -P(e(e(a,b),e(e(b,c),e(a,c)))).  % denial

Wos proved the theorem with a sequence of Otter searches, first proving short EC theorems and then using the proofs to guide subsequent searches. Many search strategies were used, including resonance, the hot list, and not allowing formulas containing instances of [1]. In addition, the search strategy was changed from one search to the next, with various combinations of the weight threshold (max_weight), the age-weight ratio (pick_given_ratio), and other parameters. The first proof Wos found has 71 steps; he then simplified it to 25 steps (see the proof in [2]). Later he found a 23-step proof.

All of Wos's proofs were derived from his original 71-step proof. The 71-step proof and the 25-step proof contain a fascinating inference:

A.  P(e(e(e(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,
         v6)),v7)),y)),v8),e(v9,v8)),v9))),x),v10),e(v11,v10)),v11)).
B.  P(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),
         v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10),e(v11,v10)),v11)))).
C.  [from A and B] P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))).

A2. P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(v,w),e(v6,w)),v6)),
   x))),e(v7,e(e(e(v7,v8),e(v9,v8)),v9))),v10),e(v11,v10)),v11)).
B2. P(e(e(x,e(e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),y),w),e(v6,w)),v6)),x)),
   e(v7,e(e(e(v7,v8),e(v9,v8)),v9)))).  
C.  [from A2 and B2] P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))).

Although a human might never find a proof with such complex inferences, they are trivial for a program. What makes these particular proofs difficult for our programs to find are premises A, A2, B, and B2 themselves. Clauses are typically selected for inference if they are short or if they appear early in the search (as determined by the pick_given_ratio). These premises have neither property.

I wished to find an automatic proof (without using guidance from any of Wos's proofs) and, if successful, to see whether the proof had such complex inferences. Because Wos's original proof was found in such an roundabout way, I hoped that any proofs found independently would be substantially different.

I ran a set of searches with various combinations of the basic search parameters and with the strategy of deleting clauses containing instances of . The searches were automatic (trying to prove the whole theorem) and independent, as opposed to Wos's iterative approach. One search succeeded, producing a proof in about ten minutes.

Does the new proof contain such a complex inference? Yes, and it is exactly the same inference (same premises, same conclusion) as in Wos's 23-step proof. The conclusion seems to be a key step.

In addition, I found by exhaustive search that if the weight threshold is less than 48 (the weight of clauses A, A2, and B above), and if clauses containing instances of are deleted, then no proofs can be found.

Otter input files, output files, proofs, and the instances corresponding to the complex inferences can be found on the Web.

Bibliography