Combining logical and algebraic techniques for natural style proving in elementary analysis

DOI10.1016/j.matcom.2008.11.002zbMath1183.68563OpenAlexW2047275139MaRDI QIDQ1025313

Robert Vajda, Bruno Buchberger, Tudor Jebelean

Publication date: 18 June 2009

Published in: Mathematics and Computers in Simulation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.matcom.2008.11.002

zbMATH Keywords

CADGroebner basesautomated theorem provingextended quantifier elimination

Mathematics Subject Classification ID

Related Items (1)

A heuristic prover for elementary analysis in \textit{Theorema}

Uses Software

• Mathematica
• QEPCAD
• Theorema
• REDLOG

Cites Work

• Quantifier elimination for real algebra -- the quadratic case and beyond
• Hierarchical deduction
• Polynomial algorithms in computer algebra
• Applying Linear Quantifier Elimination
• Model Theory
• On using bi-equational constraints in CAD construction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Combining logical and algebraic techniques for natural style proving in elementary analysis