A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs

摘要

We present a theorem prover ArgoCLP based on coherent logic that can be used for generating both readable and formal (machine verifiable) proofs in various theories, primarily geometry. We applied the prover to various axiomatic systems and proved tens of theorems from standard university textbooks on geometry. The generated proofs can be used in different educational purposes and can contribute to the growing body of formalized mathematics. The system can be used, for instance, in showing that modifications of some axioms do not change the power of an axiom system. The system can also be used as an assistant for proving appropriately chosen subgoals of complex conjectures.