Challenging theorem provers with Mathematical Olympiad problems in solid geometry

DOI10.1007/s11786-016-0256-2zbMath1358.68265OpenAlexW2326082881MaRDI QIDQ294381

Changpeng Shao, Lei Huang, Hong-Bo Li

Publication date: 16 June 2016

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11786-016-0256-2

zbMATH Keywords

Gröbner basisautomated geometric theorem provingcharacteristic setnon-degeneracy condition (NDG)vector algebra

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to geometry (51-04) Plane and solid geometry (educational aspects) (97G40)

Uses Software

• Coq
• Wsolve

Cites Work

• On the application of Buchberger's algorithm to automated geometry theorem proving
• Using Gröbner bases to reason about geometry problems
• Elimination methods
• Decomposing polynomial systems into simple systems
• Vectorial equations solving for mechanical geometry theorem proving
• Symbolic computation in the homogeneous geometric model with clifford algebra
• Machine Proofs in Geometry
• Ideals, Varieties, and Algorithms
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item