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.
@Article{abraham_et_al:DagRep.5.11.71, author = {\'{A}brah\'{a}m, Erika and Fontaine, Pascal and Sturm, Thomas and Wang, Dongming}, title = {{Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471)}}, pages = {71--89}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2016}, volume = {5}, number = {11}, editor = {\'{A}brah\'{a}m, Erika and Fontaine, Pascal and Sturm, Thomas and Wang, Dongming}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.11.71}, URN = {urn:nbn:de:0030-drops-57657}, doi = {10.4230/DagRep.5.11.71}, annote = {Keywords: algorithmic algebra, arithmetic, automated reasoning, decision procedures, quantifier elimination, satisfiability checking, SMT solving, symbolic comp} }
Feedback for Dagstuhl Publishing