From informal to formal proofs in Euclidean geometry

DOI10.1007/S10472-018-9597-7OpenAlexW2889439262WikidataQ113904582 ScholiaQ113904582MaRDI QIDQ2631958FDOQ2631958

Authors: 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

Recommendations

• scientific article; zbMATH DE number 994744
• scientific article; zbMATH DE number 1745036
• Formalization of the arithmetization of Euclidean plane geometry and applications
• Proof and computation in geometry
• Theorem proving in infinitesimal geometry
• scientific article; zbMATH DE number 2206021

zbMATH Keywords

Euclidean geometryautomated theorem provinginteractive theorem provinginformal proofscoherent logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• GCLC -- a tool for constructive Euclidean geometry and more than that
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• MizAR 40 for Mizar 40
• A coherent logic based geometry theorem prover capable of producing formal and readable proofs
• Title not available (Why is that?)
• Automatic proof and disproof in Isabelle/HOL
• Title not available (Why is that?)
• A synthesis of the procedural and declarative styles of interactive theorem proving
• Isabelle/HOL. A proof assistant for higher-order logic
• Title not available (Why is that?)
• Solution of the Robbins problem
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• Extending Sledgehammer with SMT solvers
• Translating higher-order clauses to first-order clauses
• Title not available (Why is that?)
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Mechanical Theorem Proving in Tarski’s Geometry
• Title not available (Why is that?)
• Formalizing Hilbert's Grundlagen in Isabelle/Isar
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• A machine-checked proof of the odd order theorem
• Scalable LCF-style proof translation
• A fully automatic theorem prover with human-style output
• Automation for interactive proof: first prototype
• Loops with abelian inner mapping groups: an application of automated deduction
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• Developing corpus-based translation methods between informal and formal mathematics: project description
• Automating formalization by statistical and semantic parsing of mathematics
• Learning to parse on aligned corpora (rough diamond)
• A synthetic proof of Pappus' theorem in Tarski's geometry
• A vernacular for coherent logic
• Automated theorem proving in quasigroup and loop theory
• An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
• Proof-checking Euclid
• Automating Coherent Logic
• Skolem Machines and Geometric Logic
• CDCL-Based Abstract State Transition System for Coherent Logic

Cited In (2)

• Enthymemathical Proofs and Canonical Proofs in Euclid’s Plane Geometry
• Gapless Lines and Gapless Proofs: Intersections and Continuity in Euclid’s Elements

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2631958)