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