Machine Proofs in Geometry

DOI10.1142/2196zbMath0941.68503OpenAlexW3143504415MaRDI QIDQ4857780

Jing-Zhong Zhang, Shang-Ching Chou, Xiao-Shan Gao

Publication date: 6 December 1995

Published in: Series on Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1142/2196

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Elementary problems in Euclidean geometries (51M04) Linear incidence geometry (51A99)

Related Items

Learning to solve geometric construction problems from images ⋮ Automated theorem proving in GeoGebra: current achievements ⋮ Challenging theorem provers with Mathematical Olympiad problems in solid geometry ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Proof-checking Euclid ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Generalizing Morley's and other theorems with automated realization ⋮ Geometric constraint solving with geometric transformation ⋮ Automated discovery of geometric theorems based on vector equations ⋮ The Area Method and Proving Plane Geometry Theorems ⋮ Automated and readable simplification of trigonometric expressions ⋮ Self-evident automated geometric theorem proving based on complex number identity ⋮ Measuring the readability of geometric proofs: the area method case ⋮ Automated discovery of angle theorems ⋮ A program to create new geometry proof problems ⋮ A review and prospect of readable machine proofs for geometry theorems ⋮ A case study in formalizing projective geometry in Coq: Desargues theorem ⋮ Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry. ⋮ Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry. ⋮ Recent advances in automated theorem proving on inequalities ⋮ Self-evident automated proving based on point geometry from the perspective of Wu's method identity ⋮ Automated theorem proving practice with null geometric algebra ⋮ A graphical user interface for formal proofs in geometry ⋮ Retrieving geometric information from images: the case of hand-drawn diagrams ⋮ An introduction to geometry expert ⋮ A class of mechanically decidable problems beyond Tarski's model ⋮ Automated deduction and knowledge management in geometry ⋮ A symbolic dynamic geometry system using the analytical geometry method ⋮ On \(n\)-sectors of the angles of an arbitrary triangle ⋮ A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs ⋮ Can one define geometry today? ⋮ Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation ⋮ Mechanical Theorem Proving in Tarski’s Geometry ⋮ Cayley factorization and the area principle ⋮ The Voronoi diagram of three lines ⋮ Formalization of Wu’s Simple Method in Coq ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs ⋮ Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method ⋮ Complex brackets and balanced complex 1st-order difference polynomials in 4-dimensional Minkowski space ⋮ A FORMAL SYSTEM FOR EUCLID’SELEMENTS ⋮ New dynamics in dynamic geometry: dragging constructed points ⋮ Taxonomies of geometric problems

This page was built for publication: Machine Proofs in Geometry