TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 15381

Information from Deduction: Models and Proofs

( Sep 13 – Sep 18, 2015 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/15381

Organizers

Contact



Schedule

Motivation

Models and proofs are the quintessence of logical analysis and argumentation. Many applications of deduction tools need more than a simple answer whether a conjecture holds; often additional information - for instance proofs or models - can be extremely useful. For example, proofs are used by high-integrity systems as part of certifying results obtained from automated deduction tools, and models are used by program analysis tools to represent bug traces. Most modern deductive tools may be trusted to also produce a proof or a model when answering whether a conjecture is a theorem or whether a certain problem formalized in logic has a solution. Moreover, major progress has been obtained recently by procedures that rely on refining a simultaneous search for a model and a proof. Thus, proofs and models help producing models and proofs, and applications use proofs and models in many crucial ways.

Below, we point out several directions of work related to models and proofs in which there are challenging open questions:

Extracting proofs from derivations
An important use of proof objects from derivations is for applications that require certification. But although the format for proof objects and algorithms for producing and checking them has received widespread attention in the research community, the current situation is not satisfactory from a consumer's point of view.

Extracting models from derivations
Many applications rely on models, and models are as important to certify non-derivability. Extracting models from first-order saturation calculi is a challenging problem: the well-known completeness proofs of superposition calculi produce perfect models from a saturated set of clauses. The method is highly non-constructive, so extracting useful information, such as "whether a given predicate evaluates to true or false under the given saturated clauses," is challenging. The question of representation is not yet well addressed for infinite models.

Using models to guide the search for proofs and vice versa
An upcoming next generation of reasoning procedures employ (partial) models/proofs for proof search. They range from SAT to first-order to arithmetic reasoning and combinations thereof. It remains an open question what properties of models are crucial for successful proof search, how the models should be dynamically adapted to the actual problem, and how the interplay between the models and proof search progress through deduction should be designed.

External applications of models and proofs
Models and proofs are used in various ways in applications. So far application logics and automated proof search logics have been developed widely independently. In order to get more of a coupling, efforts of bringing logics closer together or the search for adequate translations are needed.

The seminar invites discussion about the production and consumption of proofs and models. The research questions to be pursued and answered include:

  • To what extent is it possible to design common exchange formats for theories, proofs, and models, despite the diversity of provers, calculi, and formalisms?
  • How can we generate, process, and check proofs and models efficiently?
  • How can we search for, represent, and certify infinite models?
  • How can we use models to guide proof search and proofs to guide model finding?
  • How can we make proofs and models more intelligible, yet at the same time provide the level of detail required by certification processes?

Summary

Models and proofs are the quintessence of logical analysis and argumentation. Many applications of deduction tools need more than a simple answer whether a conjecture holds; often additional information - for instance proofs or models -- can be extremely useful. For example, proofs are used by high-integrity systems as part of certifying results obtained from automated deduction tools, and models are used by program analysis tools to represent bug traces. Most modern deductive tools may be trusted to also produce a proof or a model when answering whether a conjecture is a theorem or whether a certain problem formalized in logic has a solution. Moreover, major progress has been obtained recently by procedures that rely on refining a simultaneous search for a model and a proof. Thus, proofs and models help producing models and proofs, and applications use proofs and models in many crucial ways.

Below, we point out several directions of work related to models and proofs in which there are challenging open questions:

  • Extracting proofs from derivations.An important use of proof objects from derivations is for applications that require certification. But although the format for proof objects and algorithms for producing and checking them has received widespread attention in the research community, the current situation is not satisfactory from a consumer's point of view.
  • Extracting models from derivations. Many applications rely on models, and models are as important to certify non-derivability. Extracting models from first-order saturation calculi is a challenging problem: the well-known completeness proofs of superposition calculi produce perfect models from a saturated set of clauses. The method is highly non-constructive, so extracting useful information, such as "whether a given predicate evaluates to true or false under the given saturated clauses," is challenging. The question of representation is not yet well addressed for infinite models.
  • Using models to guide the search for proofs and vice versa. An upcoming next generation of reasoning procedures employ (partial) models/proofs for proof search. They range from SAT to first-order to arithmetic reasoning and combinations thereof. It remains an open question what properties of models are crucial for successful proof search, how the models should be dynamically adapted to the actual problem, and how the interplay between the models and proof search progress through deduction should be designed.
  • External applications of models and proofs. Models and proofs are used in various ways in applications. So far application logics and automated proof search logics have been developed widely independently. In order to get more of a coupling, efforts of bringing logics closer together or the search for adequate translations are needed.

This Dagstuhl seminar allowed to bring together experts for these topics and invited discussion about the production and consumption of proofs and models. The research questions pursued and answered include:

  • To what extent is it possible to design common exchange formats for theories, proofs, and models, despite the diversity of provers, calculi, and formalisms?
  • How can we generate, process, and check proofs and models efficiently?
  • How can we search for, represent, and certify infinite models?
  • How can we use models to guide proof search and proofs to guide model finding?
  • How can we make proofs and models more intelligible, yet at the same time provide the level of detail required by certification processes?
Copyright Nikolaj S. Bjørner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, and Christoph Weidenbach

Participants
  • Noran Azmy (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Franz Baader (TU Dresden, DE) [dblp]
  • Peter Baumgartner (NICTA - Canberra, AU) [dblp]
  • Christoph Benzmüller (FU Berlin, DE) [dblp]
  • Nikolaj S. Bjørner (Microsoft Corporation - Redmond, US) [dblp]
  • Jasmin Christian Blanchette (INRIA Lorraine - Nancy, FR) [dblp]
  • Martin Bromberger (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Catherine Dubois (ENSIIE - Evry, FR) [dblp]
  • Bruno Dutertre (SRI - Menlo Park, US) [dblp]
  • Carsten Fuhs (Birkbeck, University of London, GB) [dblp]
  • Silvio Ghilardi (University of Milan, IT) [dblp]
  • Jürgen Giesl (RWTH Aachen, DE) [dblp]
  • Alberto Griggio (Bruno Kessler Foundation - Trento, IT) [dblp]
  • Arie Gurfinkel (Carnegie Mellon University - Pittsburgh, US) [dblp]
  • Liana Hadarean (University of Oxford, GB) [dblp]
  • Reiner Hähnle (TU Darmstadt, DE) [dblp]
  • Matthias Horbach (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Swen Jacobs (Universität des Saarlandes, DE) [dblp]
  • Dejan Jovanovic (SRI - Menlo Park, US) [dblp]
  • Deepak Kapur (University of New Mexico - Albuquerque, US) [dblp]
  • George Karpenkov (VERIMAG - Gières, FR) [dblp]
  • Zachary Kincaid (University of Toronto, CA) [dblp]
  • Konstantin Korovin (University of Manchester, GB) [dblp]
  • Christopher Lynch (Clarkson University - Potsdam, US) [dblp]
  • Aart Middeldorp (Universität Innsbruck, AT) [dblp]
  • Tobias Nipkow (TU München, DE) [dblp]
  • Albert Oliveras (UPC - Barcelona, ES) [dblp]
  • Andrei Paskevich (University Paris-Sud, FR) [dblp]
  • Alexander Rabinovich (Tel Aviv University, IL) [dblp]
  • Giles Reger (University of Manchester, GB) [dblp]
  • Albert Rubio (UPC - Barcelona, ES) [dblp]
  • Andrey Rybalchenko (Microsoft Research UK - Cambridge, GB) [dblp]
  • Stephan Schulz (Duale Hochschule Baden-Württemberg - Stuttgart, DE) [dblp]
  • Viorica Sofronie-Stokkermans (Universität Koblenz-Landau, DE) [dblp]
  • Christian Sternagel (Universität Innsbruck, AT) [dblp]
  • Geoff Sutcliffe (University of Miami, US) [dblp]
  • Cesare Tinelli (University of Iowa - Iowa City, US) [dblp]
  • Andrei Voronkov (University of Manchester, GB) [dblp]
  • Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Sarah Winkler (Microsoft Research UK - Cambridge, GB) [dblp]
  • Burkhart Wolff (University Paris-Sud, FR) [dblp]
  • Jian Zhang (Chinese Academy of Sciences - Beijing, CN) [dblp]

Related Seminars
  • 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 17371: Deduction Beyond First-Order Logic (2017-09-10 - 2017-09-15) (Details)
  • Dagstuhl Seminar 19371: Deduction Beyond Satisfiability (2019-09-08 - 2019-09-13) (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)

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

Keywords
  • Automated Deduction
  • Models
  • Proofs
  • Decision Procedures
  • SMT
  • SAT
  • ATP