Challenging theorem provers with Mathematical Olympiad problems in solid geometry

DOI10.1007/S11786-016-0256-2MaRDI QIDQ294381zbMATH OpenOpenAlexFDO

Authors Changpeng Shao, Lei Huang, Hongbo 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

automated geometric theorem provingcharacteristic setnon-degeneracy condition (NDG)vector algebraGröbner basis

Mathematics Subject Classification ID

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

Recommendations

• Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
• Evaluation of automated theorem proving on the Mizar mathematical library
• Thousands of geometric problems for geometric theorem provers (TGTP)
• Mechanical geometry theorem proving
• Automated theorem provers: a practical tool for the working mathematician?

Cites work

• scientific article; zbMATH DE number 3941661 (Why is no real title available?)
• scientific article; zbMATH DE number 41286 (Why is no real title available?)
• scientific article; zbMATH DE number 1263333 (Why is no real title available?)
• scientific article; zbMATH DE number 1276823 (Why is no real title available?)
• scientific article; zbMATH DE number 1159859 (Why is no real title available?)
• scientific article; zbMATH DE number 4197462 (Why is no real title available?)
• scientific article; zbMATH DE number 967404 (Why is no real title available?)
• Decomposing polynomial systems into simple systems
• Elimination methods
• Ideals, Varieties, and Algorithms
• Machine Proofs in Geometry
• On the application of Buchberger's algorithm to automated geometry theorem proving
• Symbolic computation in the homogeneous geometric model with clifford algebra
• Using Gröbner bases to reason about geometry problems
• Vectorial equations solving for mechanical geometry theorem proving

Cited in

(2)

• Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
• Towards automated proving in solid geometry

Describes a project that uses

Uses Software

• Wsolve
• Coq

This page was built for publication: Challenging theorem provers with Mathematical Olympiad problems in solid geometry

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q294381)