A graphical user interface for formal proofs in geometry

DOI10.1007/S10817-007-9071-4zbMath1131.68094OpenAlexW2088823840MaRDI QIDQ2462636

Julien Narboux

Publication date: 3 December 2007

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

Full work available at URL: https://hal.inria.fr/inria-00118903/file/JARuitp-narboux.pdf

zbMATH Keywords

GeometryInterfaceCoqAutomated theorem provingDynamic geometryProof assistantTheorem prover

Mathematics Subject Classification ID

Related Items (19)

GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry ⋮ Automated theorem proving in GeoGebra: current achievements ⋮ The Relation Tool in GeoGebra 5 ⋮ Geometry constructions language ⋮ Automatic Deduction in an AI Geometry Book ⋮ Automated generation of illustrated proofs in geometry and beyond ⋮ Towards an intelligent and dynamic geometry book ⋮ The area method. A recapitulation ⋮ A review and prospect of readable machine proofs for geometry theorems ⋮ Automated deduction and knowledge management in geometry ⋮ A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs ⋮ Proof Assistant Decision Procedures for Formalizing Origami ⋮ Mechanical Theorem Proving in Tarski’s Geometry ⋮ GeoProof ⋮ Formalization of Wu’s Simple Method in Coq ⋮ Proof Documents for Automated Origami Theorem Proving ⋮ Thousands of Geometric Problems for Geometric Theorem Provers (TGTP) ⋮ A FORMAL SYSTEM FOR EUCLID’SELEMENTS ⋮ Taxonomies of geometric problems

Uses Software

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isar
• Geometer's Sketchpad
• Cabri-geometry
• Proof General Kit
• GEX
• Pcoq
• Dr.Doodle
• GeoView
• Geometrix
• Geometry Tutor
• CHYPRE
• Baghera

Cites Work

• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• Term Rewriting and All That
• Machine Proofs in Geometry
• Automated Reasoning
• A Framework for Interactive Proof
• Mechanical Theorem Proving in Tarski’s Geometry
• Theorem Proving in Higher Order Logics
• Automated Deduction in Geometry
• Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A graphical user interface for formal proofs in geometry