On the mechanization of the proof of Hessenberg's theorem in coherent logic

DOI10.1007/s10817-007-9086-xzbMath1140.03004OpenAlexW2142703483MaRDI QIDQ2471743

Dimitri Hendriks, Marc Bezem

Publication date: 18 February 2008

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://research.vu.nl/en/publications/23049501-068c-48b6-be93-fec9c22ca4d6

zbMATH Keywords

automated theorem provingprojective plane geometrycoherent logicproof objectsHessenberg's theorem

Mathematics Subject Classification ID

Related Items (10)

A synthetic proof of Pappus' theorem in Tarski's geometry ⋮ From informal to formal proofs in Euclidean geometry ⋮ Invited Talk: Coherentisation of First-Order Logic ⋮ A case study in formalizing projective geometry in Coq: Desargues theorem ⋮ GEOMETRISATION OF FIRST-ORDER LOGIC ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs ⋮ A Vernacular for Coherent Logic ⋮ Theorem proving as constraint solving with coherent logic ⋮ Geometric Rules in Infinitary Logic ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry

Uses Software

• Coq
• Isabelle
• TPTP
• Zenon
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The TPTP problem library. CNF release v1. 2. 1
• Isabelle. A generic theorem prover
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Automated proof construction in type theory using resolution
• Translation of resolution proofs into short first-order proofs without choice axioms
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• A framework for defining logics
• Automating Coherent Logic
• A Proof of Hessenberg's Theorem

This page was built for publication: On the mechanization of the proof of Hessenberg's theorem in coherent logic