The CM prover an automated first-order theorem prover with interfaces to the TPTP.
It was originally written in 1992, based on the description of the Prolog Technology Theorem Prover in [Stickel 1988], but as compiler to Prolog instead of Lisp. The underlying calculus can be understood as model elimination, as clausal tableau construction, or as the connection method. The leanCoP prover [Otten 2010], also implemented in Prolog, is based on the same calculus and regularly takes part in the CASC competitions. A conceptual difference to leanCoP is that CM proceeds in a two-step way, by first compiling the proving problem. A serious price for the compilation approach is the lack of flexibility at runtime. Advantages seem to be that some operations can be implemented more efficiently and that the possibility to inspect the output of the compiler on its own contributes to robustness and facilitates experimenting with modifications.
The prover had been revised in 1997 [Dahn+ 1997] and recently in 2015 where it has been ported to SWI Prolog and improved with the problems of the 2015 CASC competition, CASC-25, taken as yardstick. In particular for problems without equality, it turned out to be not completely far off the mid-range of the competition provers:
The main features of CM are: Literals in contrapositive bodies and contrapositives are heuristically ordered, which is performed statically at compilation. Three basic modes for the depth measure used at iterative deepening are available: The default is a combination of the tableau height and the size of processed clauses. The second mode takes just the height of the tableau, the third the number of solved subgoals. Support for “dynamic depth increase” is provided: if the search space is exhausted in consecutive runs with increasing depth within similar time spans, then the depth for the next run is multiplied by some factor. In this way, the prover rapidly reaches large depths required to solve some of the CASC-25 FNE problems, without losing completeness. A convenient side effect of this “dynamic depth increase” is termination for many satisfiable formulas by quickly reaching a large maximally allowed depth. Implemented refinements include enforcing tableau regularity, disequality literals that fail for tautological and subsumed clause instances [Goller+ 1994], a variant of antilemmas [Goller+ 1994], “sideways” lemmas [Otten 2010], and forms to restrict backtracking in incomplete ways [Otten 2010]. At preprocessing and compilation potentially expensive conversions are first attempted with a short timeout after which cheaper variants are invoked. Proofs are output as Prolog terms, which can be converted into the tableau format used by the PIE system for interpolant construction.
The CM prover is integrated into the PIE system, which is available under GNU General Public License and runs with SWI Prolog.
Contact: info@christophwernhard.com