Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Errors in McCune's Papers
Errors in McCune's Papers
W. McCune and L. Wos.
A case study in automated theorem proving: Searching for sages in
combinatory logic.
J. Automated Reasoning, 3(1):91--107, 1987.
In Section 7, the extensionality is written incorrectly as
[all x all y all z] (xy)=(zy) -> x=z. It should be
[all x all z] ([all y] (xy)=(zy)) -> x=z.
The clause form of extensionality (clause 4) should be
s(x,g(x,z)) != s(z,g(x,z)) | x=z, and clauses 6 and 7 should
have the Skolem term g(J,K). Otherwise, the proof is correct.
L. Wos and W. McCune.
Challenge problems focusing on equality and combinatory logic:
Evaluating automated theorem-proving programs.
In E. Lusk and R. Overbeek, editors, Proceedings of the 9th
International Conference on Automated Deduction, Lecture Notes in Computer
Science, Vol. 310, pages 714--729, Berlin, 1988. Springer-Verlag.
Section 2.4, Problem 4. The example
S (S (K S) K) (S (K (S (S (S K K) (S K K)))) K)
of a U combinator is incorrect.
We switched the variables
when constructing the combinator: in fact, it behaves like
a combinator U', where U'xy = x(yyx).
W. McCune and R Padmanabhan.
Automated Deduction in Equational Logic and Cubic Curves,
Springer-Verlag LNAI #1095, 1996.
Page 164, 6 lines from the bottom of the page.
The equation for collapsing a pair of absorption equations should be
p(u,g(x),x) = p(u,h(y),y).
Please let me know if you find any substantial errors not listed here.