MOVES Seminar, 28 May 2009, 15:00
Combining Algebraic Reasoning with Propositional Solvers
Dr. Thomas Sturm (Universidad de Cantabria, ES)
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.
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.
