Combining Algebraic Reasoning with Propositional Solvers


Thomas Sturm,
Universidad de Cantabria, Spain

Title Combining Algebraic Reasoning with Propositional Solvers
When 28.05.2008
Where Lecture Room Informatik 11
Abstract Our computer logic system Redlog is a component of the well-established computer algebra system Reduce, which has gone open source in December 2008. The starting point for the development of Redlog around 1992 was the efficient implementation of real quantifier elimination methods (virtual substitution, pCAD, Hermitian QE).

Meanwhile Redlog comprises in addition quantifier elimination methods for complex numbers, integers, p-adic numbers, queues of real numbers, differential algebras, Malcev-type term algebras, and quantified propositional calculus. We give an overview of the system and mention some existing applications. We sketch the available methods for the reals. Then we turn to the framework of quantified propositional calculus introducing some recent work on parametric quantified SAT-checking in Redlog. We are also going to address some technical issues concerning the possible connection of and interaction between Reduce/Redlog and other solvers.