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

DOI10.1007/S11786-022-00532-9MaRDI QIDQ6157640FDOQ6157640

Authors: Christopher W. Brown, Zoltán Kovács, Tomas Recio, R. Vajda, M. Pilar Vélez 

Publication date: 22 June 2023

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

zbMATH Keywords

computer algebraautomated theorem provingGeoGebraautomated discoveryTarskireal quantifier eliminationQEPCAD B

Mathematics Subject Classification ID

Plane and space curves (14H50) Mechanization of proofs and logical operations (03B35) Inequalities and extremum problems in real or complex geometry (51M16) Software, source code, etc. for problems pertaining to geometry (51-04) Plane and solid geometry (educational aspects) (97G40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational methods for problems pertaining to geometry (51-08) Computational real algebraic geometry (14Q30)

Cites Work

• SyNRAC: a toolbox for solving real algebraic constraints
• Polynomial constraints and unsat cores in \textsc{Tarski}
• Partial cylindrical algebraic decomposition for quantifier elimination
• Title not available (Why is that?)
• Automatic discovery of theorems in elementary geometry
• Title not available (Why is that?)
• Title not available (Why is that?)
• Real quantifier elimination is doubly exponential
• A new approach for automatic theorem proving in real geometry
• Title not available (Why is that?)
• The complexity of quantifier elimination and cylindrical algebraic decomposition
• Title not available (Why is that?)
• Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch's trick
• A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications
• Quantifier elimination by cylindrical algebraic decomposition based on regular chains
• Title not available (Why is that?)
• Computational Science and Its Applications – ICCSA 2004
• Title not available (Why is that?)
• Title not available (Why is that?)
• Detecting truth, just on parts
• Title not available (Why is that?)

Cited In (1)

• Computing with Tarski formulas and semi-algebraic sets in a web browser

This page was built for publication: Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom?

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