2026-07-25T16:23:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5765 2024-03-06T10:26:29Z ddc:004 open_access

Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471) Ábrahám, Erika Fontaine, Pascal Sturm, Thomas Wang, Dongming algorithmic algebra arithmetic automated reasoning decision procedures quantifier elimination satisfiability checking SMT solving symbolic comp 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Erika Ábrahám and Pascal Fontaine and Thomas Sturm and Dongming Wang 2016 Is Part Of Dagstuhl Reports, Volume 5, Issue 11 (2016) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagRep.5.11.71 urn:nbn:de:0030-drops-57657 https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.11.71 eng https://creativecommons.org/licenses/by/3.0/legalcode