zbMATH — the first resource for mathematics

On proving inequalities by cylindrical algebraic decomposition. (English) Zbl 07307814
Summary: Cylindrical algebraic decomposition (CAD) is a basic concept in real algebraic geometry, and it has useful applications to deal with symbolic inequalities. We present a new implementation of CAD in the SageMath computer algebra system. This is not as fast as some existing implementations like QEPCAD, but it is more exible to be embedded in certain larger calculations. One such application of CAD is a proving procedure for inequalities involving recursive functions, invented by S. Gerhold and M. Kauers [in: Proceedings of the 2005 international symposium on symbolic and algebraic computation, ISSAC’05, Beijing, China, July 24–27, 2005. New York, NY: ACM Press. 156–162 (2005; Zbl 1360.68933)]. We present an implementation of this algorithm as well. This paper also gives an overview with examples about the theory behind the implemented algorithms.
68W30 Symbolic computation and algebraic computation
13P15 Solving polynomial systems; resultants
QEPCAD; SageMath
Full Text: Link