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

Abstract. 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 objects. 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.

• Type: Journal
• Year: 2008
• Where: JAR
• Authors: Marc Bezem, Dimitri Hendriks
• Keywords: Constructive Proof, Interactive Proof, JAR 2008, Proof Automation