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

M. Bezem, R.D.A. Hendriks

Research output: Contribution to JournalArticleAcademicpeer-review

234 Downloads (Pure)

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 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. © 2007 Springer Science+Business Media B.V.
Original languageEnglish
Pages (from-to)61-85
JournalJournal of Automated Reasoning
Volume40
Issue number1
DOIs
Publication statusPublished - 2008

Bibliographical note

beze:hend:2008

Fingerprint

Dive into the research topics of 'On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic'. Together they form a unique fingerprint.

Cite this