From informal to formal proofs in Euclidean geometry

DOI10.1007/s10472-018-9597-7OpenAlexW2889439262WikidataQ113904582 ScholiaQ113904582MaRDI QIDQ2631958

Sana Stojanović Đurđević

Publication date: 16 May 2019

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-018-9597-7

zbMATH Keywords

Euclidean geometryautomated theorem provinginteractive theorem provinginformal proofscoherent logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Uses Software

• Coq
• GCLC
• Isabelle/HOL
• VAMPIRE
• SPASS
• TPTP
• Isar
• z3
• HOL Light
• Sledgehammer
• ArgoCLP
• E Theorem Prover
• Flyspeck
• miz3

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• MizAR 40 for Mizar 40
• Solution of the Robbins problem
• Isabelle/HOL. A proof assistant for higher-order logic
• Automating formalization by statistical and semantic parsing of mathematics
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• Extending Sledgehammer with SMT solvers
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• A synthetic proof of Pappus' theorem in Tarski's geometry
• A fully automatic theorem prover with human-style output
• Automation for interactive proof: first prototype
• Translating higher-order clauses to first-order clauses
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• Proof-checking Euclid
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
• CDCL-Based Abstract State Transition System for Coherent Logic
• Learning to Parse on Aligned Corpora (Rough Diamond)
• An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
• A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
• Automatic Proof and Disproof in Isabelle/HOL
• Skolem Machines and Geometric Logic
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• Automated theorem proving in quasigroup and loop theory
• Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction
• Scalable LCF-Style Proof Translation
• A Machine-Checked Proof of the Odd Order Theorem
• Automating Coherent Logic
• Mechanical Theorem Proving in Tarski’s Geometry
• A Vernacular for Coherent Logic
• Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description
• GCLC — A Tool for Constructive Euclidean Geometry and More Than That
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS

This page was built for publication: From informal to formal proofs in Euclidean geometry