Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Fuhs, Carsten; Rümmer, Philipp; Schmidt, Renate; Tinelli, Cesare https://www.dagstuhl.de/dagrep License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-118432
URL:

; ; ;
Weitere Beteiligte (Hrsg. etc.): Carsten Fuhs and Philipp Rümmer and Renate Schmidt and Cesare Tinelli

Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)

pdf-format:


Abstract

Research in automated deduction is traditionally focused on the problem of determining the satisfiability of formulas or, more generally, on solving logical problems with yes/no answers. Thanks to recent advances that have dramatically increased the power of automated deduction tools, there is now a growing interest in extending deduction techniques to attack logical problems with more complex answers. These include both problems with a long history, such as quantifier elimination, which are now being revisited in light of the new methods, as well as newer problems such as minimal unsatisfiable cores computation, model counting for propositional or first-order formulas, Boolean or SMT constraint optimization, generation of interpolants, abductive reasoning, and syntax-guided synthesis. Such problems arise in a variety of applications including the analysis of probabilistic systems (where properties like safety or liveness can be established only probabilistically), network verification (with relies on model counting), the computation of tight complexity bounds for programs, program synthesis, model checking (where interpolation or abductive reasoning can be used to achieve scale), and ontology-based information processing. The seminar brought together researchers and practitioners from many of the often disjoint sub-communities interested in the problems above. The unifying theme of the seminar was how to harness and extend the power of automated deduction methods to solve problems with more complex answers than binary ones.

BibTeX - Entry

@Article{fuhs_et_al:DR:2020:11843,
  author =	{Carsten Fuhs and Philipp R{\"u}mmer and Renate Schmidt and Cesare Tinelli},
  title =	{{Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)}},
  pages =	{23--44},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{9},
  number =	{9},
  editor =	{Carsten Fuhs and Philipp R{\"u}mmer and Renate Schmidt and Cesare Tinelli},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/11843},
  URN =		{urn:nbn:de:0030-drops-118432},
  doi =		{10.4230/DagRep.9.9.23},
  annote =	{Keywords: abduction, automated deduction, interpolation, quantifier elimination, synthesis}
}

Keywords: abduction, automated deduction, interpolation, quantifier elimination, synthesis
Seminar: Dagstuhl Reports, Volume 9, Issue 9
Issue date: 2020
Date of publication: 19.02.2020


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI