ICMS 2018 - Session 9: Satisfiability Checking and Symbolic Computation
Organizers
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
© 2024. All rights reserved.
