Date: September 1988
Creator: Wos, Larry
Description: In this report, we establish that the use of an automated theorem- proving program to study deep questions from mathematics and logic is indeed an excellent move. Among such problems, we focus mainly on that concerning the construction of fixed point combinators--a problem considered by logicians to be significant and difficult to solve, and often computationally intensive and arduous. To be a fixed point combinator, THETA must satisfy the equation THETAx = x(THETAx) for all combinators x. The specific questions on which we focus most heavily ask, for each chosen set of combinators, whether a fixed point combinator can be constructed from the members of that set. For answering questions of this type, we present a new, sound, and efficient method, called the kernel method, which can be applied quite easily by hand and very easily by an automated theorem-proving program. For the application of the kernel method by a theorem-proving program, we illustrate the vital role that is played by both paramodulation and demodulation--two of the powerful features frequently offered by an automated theorem-proving program for treating equality as if it is ''understood.'' We also state a conjecture that, if proved, establishes the completeness of the kernel method. From ...
Contributing Partner: UNT Libraries Government Documents Department