Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)

Authors Carsten Fuhs, Philipp Rümmer, Renate Schmidt, Cesare Tinelli and all authors of the abstracts in this report



PDF
Thumbnail PDF

File

DagRep.9.9.23.pdf
  • Filesize: 3.34 MB
  • 22 pages

Document Identifiers

Author Details

Carsten Fuhs
Philipp Rümmer
Renate Schmidt
Cesare Tinelli
and all authors of the abstracts in this report

Cite As Get BibTex

Carsten Fuhs, Philipp Rümmer, Renate Schmidt, and Cesare Tinelli. Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). In Dagstuhl Reports, Volume 9, Issue 9, pp. 23-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/DagRep.9.9.23

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.

Subject Classification

Keywords
  • abduction
  • automated deduction
  • interpolation
  • quantifier elimination
  • synthesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail