On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic

摘要

We propose to combine interactive proof construction with proof automation for a fragment of first-order logic called Coherent Logic (CL). CL allows enough existential quantification to make Skolemization unnecessary. Moreover, CL has a constructive proof system based on forward reasoning, which is easy to automate and where standardized proof objects can easily be obtained. We have implemented in Prolog a CL prover which generates Coq proof scripts. We test our approach with a case study: Hessenberg's theorem, which states that in elementary projective plane geometry Pappus' axiom implies Desargues' axiom. Our CL prover makes it possible to automate large parts of the proof, in particular taking care of the large number of degenerate cases.