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

DOI10.1007/s13398-020-00874-8zbMath1453.68209OpenAlexW3038289190MaRDI QIDQ783254

Pilar Páez-Guillán, Tomás Recio, Manuel Ladra Gonzalez

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

saturationnon-degeneracy conditionsautomated discoveryautomated 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)

Related Items

Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom?

Uses Software

• SINGULAR
• GeoGebra

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the unavoidable uncertainty of truth in dynamic geometry proving
• On protocols for the automated discovery of theorems in elementary geometry
• A refutational approach to geometry theorem proving
• Automated reducible geometric theorem proving and discovery by Gröbner basis method
• Automatic discovery of theorems in elementary geometry
• Generalizing the Steiner-Lehmus theorem using the Gröbner cover
• Towards the Automatic Discovery of Theorems in GeoGebra
• An Introduction to Automated Discovery in Geometry through Symbolic Computation
• The Generalized Rabinowitsch Trick
• Ideals, Varieties, and Algorithms
• Development of automatic reasoning tools in GeoGebra