Posted on the Web March 6, 2002. Last updated on September 11, 2005 by Bob Veroff.

HBCK

The following problem is posed as an open question in [2].
Update: It turns out that Tomasz Kowalski had already published a proof by the time the McCune/Padmanabahn monograph came out.
T. Kowalski. A syntactic proof of a conjecture of Andrzej Wronski. Rep. Math. Logic, 28:1000-1005, 1994. (pdf)
The problem has been an interesting exercise for automated deduction in any case.

The quasivariety HBCK is defined as follows.

   (M3)  x * 1 = 1
   (M4)  1 * x = x
   (M5)  (x * y) * ((z * x) * (z * y)) = 1
   (M7)  x * y != 1 | y * x != 1 | x = y
   (M8)  x * x = 1
   (M9)  x * (y * z) = y * (x * z)
   (H)   (x * y) * (x * z) = (y * x) * (y * z)

The challenge is to find a first-order proof that the equation

   (((x * y) * y) * x) * x = (((y * x) * x) * y) * y
can be derived from HBCK. Blok and Ferreirim (see [2]) indicate that such a proof can be found, but the result relies on a model-theoretic argument.

Using the method of proof sketches [3], we have been able to find a proof with Otter [1]. Our proof makes use of the definition

   g(x,y) = (((x * y) * y) * x) * x
and can be found here.

References

[1] McCune, W., OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois, 1994.

[2] McCune, W., and Padmanabhan, R., Automated deduction in equational logic and cubic curves, Lecture Notes in Artificial Intelligene 1095, Springer-Verlag, Berlin (1996).

[3] Veroff, R., ``Solving open questions and other challenge problems using proof sketches,'' Journal of Automated Reasoning, Vol. 27, no. 2, pp. 157-174 (2001). (postscript)


The University of New Mexico

School of Engineering

Computer Science Department