Session 9. Satisfiability Checking and Symbolic Computation


Aim and Scope

Software tools for checking the satisfiability of real-algebraic formulas play an important role in a wide range of applications. Such tools are being developed in Mathematics in form of computer algebra systems as well as in Computer Science as SAT-modulo-theories (SMT) solvers. With this topical session we want to strengthen the exchange between these areas, with presentations about algorithms and software tools from both domains and success stories about how the two communities can profit from achievements of each other.

Accepted Talks

Gereon Kremer and Erika Abraham: Incremental Cylindrical Algebraic Decomposition

Jan Horacek and Martin Kreuzer: 3BA: A Border Bases Solver with a SAT Extension

Casey Mulligan, James H. Davenport and Matthew England: TheoryGuru: A Mathematica Package to apply Quantifier Elimination Technology to Economics

Curtis Bright, Ilias Kotsireas and Vijay Ganesh: MathCheck: A SAT+CAS Mathematical Conjecture Verifier

Fernando Vale-Enriquez and Christopher Brown: Polynomial Constraints and Unsat Cores in TARSKI

Alexei Lisitsa: Andrews-Curtis conjecture, term rewriting and first-order proofs