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

(J) (((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 Intelligence* 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