Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471)
Erika Ábrahám, Pascal Fontaine, Thomas Sturm, Dongming Wang · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2016
The seminar focused on satisfiability checking for combinations of first-order logic and subclasses thereof with arithmetic theories in a very liberal sense, also covering quantifiers and parameters. It gathered members of the two communities of symbolic computation (or computer algebra) and satisfiability checking (including satisfiability modulo theories). Up-to-now, these two communities have been working quite independently. We are confident that the seminar will initiate cross-fertilization of both fields and bring improvements for both satisfiability checking and symbolic computation, and for their applications.