Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch's trick

DOI10.1007/S13398-020-00874-8MaRDI QIDQ783254zbMATH OpenOpenAlexFDO

Authors M. Ladra, Pilar Páez-Guillán, Tomas Recio

Publication date 12 August 2020

Published in Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales. Serie A: Matemáticas. RACSAM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s13398-020-00874-8

zbMATH Keywords

saturationautomated discoverynon-degeneracy conditionsautomated provingRabinowitsch's trick

Mathematics Subject Classification ID

Effectivity, complexity and computational aspects of algebraic geometry (14Q20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• The generalized Rabinowitsch trick
• scientific article; zbMATH DE number 1745036
• scientific article; zbMATH DE number 978243
• A new approach for automatic theorem proving in real geometry
• Algebraic proofs for geometric statements

Cites work

• scientific article; zbMATH DE number 41286 (Why is no real title available?)
• scientific article; zbMATH DE number 3586510 (Why is no real title available?)
• scientific article; zbMATH DE number 517393 (Why is no real title available?)
• A refutational approach to geometry theorem proving
• An introduction to automated discovery in geometry through symbolic computation
• Automated reducible geometric theorem proving and discovery by Gröbner basis method
• Automatic discovery of theorems in elementary geometry
• Development of automatic reasoning tools in GeoGebra
• Generalizing the Steiner-Lehmus theorem using the Gröbner cover
• Ideals, Varieties, and Algorithms
• On protocols for the automated discovery of theorems in elementary geometry
• On the unavoidable uncertainty of truth in dynamic geometry proving
• The generalized Rabinowitsch trick
• Towards the Automatic Discovery of Theorems in GeoGebra

Cited in

(2)

• Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom?
• Open geometry prover community project

Describes a project that uses

Uses Software

• GeoGebra
• SINGULAR

This page was built for publication: Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch's trick

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