Machine Proofs in Geometry
From MaRDI portal
Publication:4857780
DOI10.1142/2196zbMATH Open0941.68503OpenAlexW3143504415MaRDI QIDQ4857780FDOQ4857780
Authors: Shang-Ching Chou, Jingzhong Zhang, 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
Recommendations
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mechanization of proofs and logical operations (03B35) Linear incidence geometry (51A99) Elementary problems in Euclidean geometries (51M04)
Cited In (56)
- Recent advances in automated theorem proving on inequalities
- A review and prospect of readable machine proofs for geometry theorems
- A graphical user interface for formal proofs in geometry
- A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs
- A symbolic dynamic geometry system using the analytical geometry method
- On \(n\)-sectors of the angles of an arbitrary triangle
- Automated theorem proving practice with null geometric algebra
- Self-evident automated proving based on point geometry from the perspective of Wu's method identity
- Retrieving geometric information from images: the case of hand-drawn diagrams
- New dynamics in dynamic geometry: dragging constructed points
- An introduction to geometry expert
- Self-evident automated geometric theorem proving based on complex number identity
- Taxonomies of geometric problems
- Readable machine proofs for mass point geometry
- Proof-checking Euclid
- Measuring the readability of geometric proofs: the area method case
- Title not available (Why is that?)
- Portfolio theorem proving and prover runtime prediction for geometry
- Automated theorem proving in GeoGebra: current achievements
- Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry.
- Learning to solve geometric construction problems from images
- Title not available (Why is that?)
- A case study in formalizing projective geometry in Coq: Desargues theorem
- Challenging theorem provers with Mathematical Olympiad problems in solid geometry
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- Mechanical Theorem Proving in Tarski’s Geometry
- Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
- Automated deduction and knowledge management in geometry
- Formalization of Wu's simple method in Coq
- Formalization of the arithmetization of Euclidean plane geometry and applications
- A program to create new geometry proof problems
- Automated discovery of angle theorems
- Generalizing Morley's and other theorems with automated realization
- Complex brackets and balanced complex 1st-order difference polynomials in 4-dimensional Minkowski space
- A class of mechanically decidable problems beyond Tarski's model
- The Voronoi diagram of three lines
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Automated generation of readable proofs for constructive geometry statements with the mass point method
- Title not available (Why is that?)
- Automated production of traditional proofs in solid geometry
- Automated discovery of geometric theorems based on vector equations
- Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.
- Title not available (Why is that?)
- Title not available (Why is that?)
- Geometric constraint solving with geometric transformation
- The area method and proving plane geometry theorems
- Automatic Deduction in an AI Geometry Book
- Automated and readable simplification of trigonometric expressions
- Automated reasoning in geometry
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Can one define geometry today?
- Cayley factorization and the area principle
- Geometry machines: from AI to SMC
- A method for the automated discovery of angle theorems
- Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach
- The area method in the Wolfram language
This page was built for publication: Machine Proofs in Geometry
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4857780)
