First-order Proof of Basarab's Theorem

Robert Veroff

April 2007 (under construction)

Introduction

This Web page contains some notes on our solution to a problem in loop theory. The problem was not open, but it was posed to us by Michael Kinyon as a good challenge for theorem provers.

Problem Statement

   % loop axioms
   1 * x = x.
   x * 1 = x.
   x * (x \ y) = y.
   x \ (x * y) = y.
   (x * y) / y = x.
   (x / y) * y = x.

   % axioms for a conjugacy closed loop
   ((x * y) / x) * (x * z) = x * (y * z) # label(LCC).
   (z * x) * (x \ (y * x)) = (z * y) * x # label(RCC).

   % theorem to prove
   x * (y * ((u * z) \ (z * u))) = (x * y) * ((u * z) \ (z * u)).
(... include some comments about the problem ...)

Proof

We found a proof with Prover9 using the method of proof sketches. Here is the first proof we found.
basarab.pf
(... include some comments about the use of proof sketches for this problem ...)

Here is another proof, derived from the preceding one, in which all demodulation (rewriting) steps are explicit, and the goal is derived directly. We call this a strictly-forward, demodulation-free (sfdf) proof.

basarab_sfdf.pf
The sfdf version of the proof was found using Otter.

Getting the Proof from Scratch with Autosketches

newauto -f basarab_auto.in > basarab_auto.out

References

  1. W. McCune. Otter 3.0 Reference Manual and Guide. Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL, 1994.
  2. W. McCune. Prover9. http://www.cs.unm.edu/~mccune/prover9/, 2007.
  3. R. Veroff. Solving Open Questions and Other Challenge Problems Using Proof Sketches. J. Automated Reasoning, 27(2):157-174, 2001.