On proving inequalities by cylindrical algebraic decomposition

Abstract. 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 flexible to be embedded in certain larger calculations. One such application of CAD is a proving procedure for inequalities involving recursive functions, invented by Gerhold and Kauers. We present an implementation of this algorithm as well. This paper also gives an overview with examples about the theory behind the implemented algorithms.