TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 19371

Deduction Beyond Satisfiability

( 08. Sep – 13. Sep, 2019 )

(zum Vergrößern in der Bildmitte klicken)

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/19371

Organisatoren

Kontakt



Programm

Motivation

Research in automated deduction has traditionally focused on solving decision problems, which are problems with a binary answer. Prominent examples include proving the unsatisfiability of a formula, proving that a formula follows logically from others, checking the consistency of an ontology, proving safety or termination properties of programs, and so on. However, automated deduction methods and tools are increasingly being used to address problems with more complex answers, for instance to generate programs from formal specifications, compute complexity bounds, or find optimal solutions to constraint satisfaction problems.

In some cases, the required extended functionality (e.g., to identify unsatisfiable cores) can be provided relatively easily from current deduction procedures. In other cases (e.g., for Craig interpolation, or to find optimal solutions of constraints), elaborate extensions of these procedures are needed. Sometimes, altogether different methods have to be devised (e.g., to count the number of models of a formula, compute the set of all consequences of an ontology, identify missing information in a knowledge base, transform and mine proofs, or analyze probabilistic systems). In all cases, the step from yes/no answers to such extended queries and complex output drastically widens the application domain of deductive machinery. This is proving to be a key enabler in a variety of areas such as formal methods (for software/hardware development) and knowledge representation and reasoning.

While promising progress has been made, many challenges remain. Extending automated deduction methods and tools to support these new functionalities is often intrinsically difficult, and challenging both in theory and implementation. The scarcity of interactions between the involved sub-communities represents another substantial impediment to further advances, which is unfortunate because these sub-communities often face similar problems and so could greatly benefit from the cross-fertilization of ideas and approaches. An additional challenge is the lack of common standards for interfacing tools supporting the extended queries. Developing common formalisms, possibly as extensions of current standard languages, could be as transformative to the field as the introduction of standards such as TPTP and SMT-LIB has been in the past.

This Dagstuhl Seminar will bring together researchers working on deduction methods and tools that go beyond satisfiability and other traditional decision problems; specialists that work on advanced techniques in deduction and automated reasoning such as model counting, quantifier elimination, interpolation, abduction, or optimization; and consumers of deduction technology who need answers to more complex queries than just yes/no questions. The unifying theme of the seminar will be how to harness and extend the power of automated deduction methods to solve a variety of non-decision problems with useful applications. Some of the research questions addressed at the seminar will be the following:

  • What kind of information should be passed to a “beyond satisfiability” deduction tool, and what information should be returned to the user? The goal is to enhance the understanding of related concepts in different subfields and applications, and to converge towards common formalisms.
  • How can current ideas, results and systems in one sub-community of researchers and practitioners benefit the needs of other communities?
  • What are outstanding challenges in using and building deduction tools to attack logical problems with complex answers?
Copyright Carsten Fuhs, Philipp Rümmer, Renate Schmidt, and Cesare Tinelli

Summary

This report contains the program and outcomes of Dagstuhl Seminar 19371 on "Deduction Beyond Satisfiability" held at Schloss Dagstuhl, Leibniz Center for Informatics, during September 10--15, 2017. It was the thirteenth in a series of Dagstuhl Deduction seminars held biennially since 1993.

Research in automated deduction has traditionally focused on solving decision problems, which are problems with a binary answer. Prominent examples include proving the unsatisfiability of a formula, proving that a formula follows logically from others, checking the consistency of an ontology, proving safety or termination properties of programs, and so on. However, automated deduction methods and tools are increasingly being used to address problems with more complex answers, for instance to generate programs from formal specifications, compute complexity bounds, or find optimal solutions to constraint satisfaction problems.

In some cases, the required extended functionality (e.g., to identify unsatisfiable cores) can be provided relatively easily from current deduction procedures. In other cases (e.g., for Craig interpolation, or to find optimal solutions of constraints), elaborate extensions of these procedures are needed. Sometimes, altogether different methods have to be devised (e.g., to count the number of models of a formula, compute the set of all consequences of an ontology, identify missing information in a knowledge base, transform and mine proofs, or analyze probabilistic systems). In all cases, the step from yes/no answers to such extended queries and complex output drastically widens the application domain of deductive machinery. This is proving to be a key enabler in a variety of areas such as formal methods (for software/hardware development) and knowledge representation and reasoning.

While promising progress has been made, many challenges remain. Extending automated deduction methods and tools to support these new functionalities is often intrinsically difficult, and challenging both in theory and implementation. The scarcity of interactions between the involved sub-communities represents another substantial impediment to further advances, which is unfortunate because these sub-communities often face similar problems and so could greatly benefit from the cross-fertilization of ideas and approaches. An additional challenge is the lack of common standards for interfacing tools supporting the extended queries. Developing common formalisms, possibly as extensions of current standard languages, could be as transformative to the field as the introduction of standards such as TPTP and SMT-LIB has been in the past.

This Dagstuhl seminar brought together researchers working on deduction methods and tools that go beyond satisfiability and other traditional decision problems; specialists that work on advanced techniques in deduction and automated reasoning such as model counting, quantifier elimination, interpolation, abduction, or optimization; and consumers of deduction technology who need answers to more complex queries than just yes/no questions.

The unifying theme of the seminar was how to harness and extend the power of automated deduction methods to solve a variety of non-decision problems with useful applications. Research questions addressed at the seminar were the following:

  • What kind of information should be passed to a "beyond satisfiability" deduction tool, and what information should be returned to the user? The goal should be to enhance the understanding of related concepts in different subfields and applications, and to converge towards common formalisms.
  • How can current ideas, results and systems in one sub-community of researchers and practitioners benefit the needs of other communities?
  • What are outstanding challenges in using and building deduction tools to attack logical problems with complex answers?
Copyright Carsten Fuhs, Philipp Rümmer, Renate Schmidt, and Cesare Tinelli

Teilnehmer
  • Alexander Bentkamp (Free University Amsterdam, NL) [dblp]
  • Nikolaj S. Bjørner (Microsoft Research - Redmond, US) [dblp]
  • Maria Paola Bonacina (Università degli Studi di Verona, IT) [dblp]
  • Florent Capelli (INRIA Lille, FR) [dblp]
  • Warren Del-Pinto (University of Manchester, GB) [dblp]
  • Rayna Dimitrova (University of Leicester, GB) [dblp]
  • Pascal Fontaine (LORIA & INRIA - Nancy, FR) [dblp]
  • Florian Frohn (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Carsten Fuhs (Birkbeck, University of London, GB) [dblp]
  • Jürgen Giesl (RWTH Aachen, DE) [dblp]
  • Alberto Griggio (Bruno Kessler Foundation - Trento, IT) [dblp]
  • Arie Gurfinkel (University of Waterloo, CA) [dblp]
  • Reiner Hähnle (TU Darmstadt, DE) [dblp]
  • Matthias Heizmann (Universität Freiburg, DE) [dblp]
  • Benjamin Kaminski (RWTH Aachen, DE) [dblp]
  • Laura Kovács (TU Wien, AT) [dblp]
  • Quang Loc Le (Teesside University - Middlesbrough, GB) [dblp]
  • Alexander Leitsch (TU Wien, AT) [dblp]
  • Anthony W. Lin (TU Kaiserslautern, DE) [dblp]
  • Joao Marques-Silva (Federal University - Toulouse, FR) [dblp]
  • David Monniaux (VERIMAG - Grenoble, FR) [dblp]
  • Alexander Nadel (Intel Israel - Haifa, IL) [dblp]
  • Claudia Nalon (University of Brasilia, BR) [dblp]
  • Naoki Nishida (Nagoya University, JP) [dblp]
  • Quoc Sang Phan (Synopsys Inc. - Mountain View, US) [dblp]
  • Ruzica Piskac (Yale University - New Haven, US) [dblp]
  • Albert Rubio (Complutense University of Madrid, ES) [dblp]
  • Philipp Rümmer (Uppsala University, SE) [dblp]
  • Andrey Rybalchenko (Microsoft Research - Cambridge, GB) [dblp]
  • Renate Schmidt (University of Manchester, GB) [dblp]
  • Martina Seidl (Johannes Kepler Universität Linz, AT) [dblp]
  • Viorica Sofronie-Stokkermans (Universität Koblenz-Landau, DE) [dblp]
  • Sorin Stratulat (University of Lorraine - Metz, FR) [dblp]
  • Andrzej Szalas (University of Warsaw, PL) [dblp]
  • Tachio Terauchi (Waseda University - Tokyo, JP) [dblp]
  • Cesare Tinelli (University of Iowa - Iowa City, US) [dblp]
  • Sophie Tourret (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Andrei Voronkov (University of Manchester, GB & EasyChair) [dblp]
  • Uwe Waldmann (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Thomas Wies (New York University, US) [dblp]
  • Sarah Winkler (University of Verona, IT) [dblp]

Verwandte Seminare
  • Dagstuhl-Seminar 9310: Deduction (1993-03-08 - 1993-03-12) (Details)
  • Dagstuhl-Seminar 9512: Deduction (1995-03-20 - 1995-03-24) (Details)
  • Dagstuhl-Seminar 9709: Deduction (1997-02-24 - 1997-02-28) (Details)
  • Dagstuhl-Seminar 99091: Deduction (1999-02-28 - 1999-03-05) (Details)
  • Dagstuhl-Seminar 01101: Deduction (2001-03-04 - 2001-03-09) (Details)
  • Dagstuhl-Seminar 03171: Deduction and Infinite-state Model Checking (2003-04-21 - 2003-04-25) (Details)
  • Dagstuhl-Seminar 05431: Deduction and Applications (2005-10-23 - 2005-10-28) (Details)
  • Dagstuhl-Seminar 07401: Deduction and Decision Procedures (2007-09-30 - 2007-10-05) (Details)
  • Dagstuhl-Seminar 09411: Interaction versus Automation: The two Faces of Deduction (2009-10-04 - 2009-10-09) (Details)
  • Dagstuhl-Seminar 13411: Deduction and Arithmetic (2013-10-06 - 2013-10-11) (Details)
  • Dagstuhl-Seminar 15381: Information from Deduction: Models and Proofs (2015-09-13 - 2015-09-18) (Details)
  • Dagstuhl-Seminar 17371: Deduction Beyond First-Order Logic (2017-09-10 - 2017-09-15) (Details)
  • Dagstuhl-Seminar 21371: Integrated Deduction (2021-09-12 - 2021-09-17) (Details)
  • Dagstuhl-Seminar 23471: The Next Generation of Deduction Systems: From Composition to Compositionality (2023-11-19 - 2023-11-24) (Details)

Klassifikation
  • artificial intelligence / robotics
  • semantics / formal methods
  • verification / logic

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