CPTP
An Automated Critical Pairs
Equational Theorem Prover

The only mechanism used in this simple automated theorem prover is the formation of critical pairs (see Sec. 3.13.4 of LMCS). The algorithm is a simple iteration of the following loop:

LOOP
Given: a list of identities (with the right hand sides no longer than the left hand sides)
  • s1 = t1

    ......

  • sn = tn.
  • For each i,j between 1 and n:
    find all the critical pairs (p,q) for the pair of rewrite rules si --> ti and sj --> tj.
  • If such a critical pair (p,q) gives an identity p = q not on the list, add p = q to the list.
  • If, at the end of considering all the i,j between 1 and n, new identities have been found, then goto LOOP.
    Otherwise exit the loop.
    ENDLOOP

    • There are only two parameters that one can set in this program, namely the size of the terms that one will permit in new critical pairs, and the number of new identities that one can add to the list.

    In a full fledged theorem prover, such as William McCune's Otter, one has a wide range of parameter options. It is in the management of these parameters that the "art" of automated theorem proving is exercised.

    Even with this simple program, CPTP, one will quickly see the dramatic effects of changing parameters.

    There is one short cut used in the program, namely if one starts with an identity t = x such that x is neither the leftmost nor rightmost variable of t, and if one derives the equation x+y = x or x+y = y then the program immediately announces that one has u = v. This follows from the fact that using x+y = x one can reduce t = x to leftvariable(t) = x; and similarly for x+y = y.