Department of Computer Sciences 1999 ACL2 Workshop March 29 - March 31, 1999

Proof Checker for First Order Logic

The goal of the project is to build a high-performance, sound theorem-proving system for first-order logic. Part of the theorem proving will be done by ACL2 functions (normal form conversion, Solemization), and the hard part (searching for a proof) will be done by an existing theorem prover, say Otter. Otter's proofs will be checked by ACL2 functions, so that soundness of the system will not depend in any way on the soundness of Otter. The system will be able to search for (finite) counterexamples as well as for proofs, with a program such as MACE doing the hard part.

Soundness of the system is proved with respect to finite interpretations. This is clearly a limitation, because there are simple nontheorems that are true in all finite interpretations. But we are hoping to show that our soundness proofs (or some variation) mean something or infinite models as well.

Slides, ACL2 events, and more information can be found here.

William McCune
Mathematics and Computer Science Division
Argonne National Laboratory