The area method. A recapitulation
From MaRDI portal
Publication:437042
DOI10.1007/s10817-010-9209-7zbMath1242.68281OpenAlexW86824626WikidataQ57552308 ScholiaQ57552308MaRDI QIDQ437042
Predrag Janičić, Julien Narboux, Pedro Quaresma
Publication date: 17 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9209-7
Related Items
A synthetic proof of Pappus' theorem in Tarski's geometry ⋮ Automated theorem proving in GeoGebra: current achievements ⋮ The Relation Tool in GeoGebra 5 ⋮ Current Status of the I2GATP Common Format ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Two cryptomorphic formalizations of projective incidence geometry ⋮ Towards Understanding Triangle Construction Problems ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Generalizing Morley's and other theorems with automated realization ⋮ Measuring the readability of geometric proofs: the area method case ⋮ Towards an intelligent and dynamic geometry book ⋮ A review and prospect of readable machine proofs for geometry theorems ⋮ Automated deduction and knowledge management in geometry ⋮ A symbolic dynamic geometry system using the analytical geometry method ⋮ Formalization of Wu’s Simple Method in Coq ⋮ Thousands of Geometric Problems for Geometric Theorem Provers (TGTP) ⋮ Taxonomies of geometric problems ⋮ Theorem proving as constraint solving with coherent logic ⋮ Formalizing complex plane geometry
Uses Software
Cites Work
- A case study in formalizing projective geometry in Coq: Desargues theorem
- Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method
- Visually dynamic presentation of proofs in plane geometry. II: Automated generation of visually dynamic presentations with the full-angle method and the deductive database method
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Using Gröbner bases to reason about geometry problems
- Automated reasoning in geometry theorem proving with Prolog
- Plane geometry theorem proving using forward chaining
- Formalization of Hilbert's geometry of incidence and parallelism
- A deductive database approach to automated geometry theorem proving and discovering
- Automated production of traditional proofs in solid geometry
- The axioms of constructive geometry
- Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems
- A graphical user interface for formal proofs in geometry
- Geometry constructions language
- Formalizing Projective Plane Geometry in Coq
- Formalizing Hilbert’s Grundlagen in Isabelle/Isar
- Formal certification of a compiler back-end or
- Automatic Verification of Regular Constructions in Dynamic Geometry Systems
- Mechanical Theorem Proving in Tarski’s Geometry
- Theorem Proving in Higher Order Logics
- GCLC — A Tool for Constructive Euclidean Geometry and More Than That
- Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories
- Automated Deduction in Geometry
- Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
- Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: The area method. A recapitulation
