http://www.dagstuhl.de/15381
13. – 18. September 2015, Dagstuhl Seminar 15381
Information from Deduction: Models and Proofs
Organisatoren
Nikolaj S. Bjorner (Microsoft Corporation – Redmond, US)
Jasmin Christian Blanchette (INRIA Lorraine – Nancy, FR)
Viorica Sofronie-Stokkermans (Universität Koblenz-Landau, DE)
Christoph Weidenbach (MPI für Informatik – Saarbrücken, DE)
Auskunft zu diesem Dagstuhl Seminar erteilt
Dokumente
Dagstuhl Report, Volume 5, Issue 9
Motivationstext
Teilnehmerliste
Gemeinsame Dokumente
Dagstuhl's Impact: Dokumente verfügbar
Programm des Dagstuhl Seminars [pdf]
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?
Creative Commons BY 3.0 Unported license
Nikolaj S. Bjorner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, and Christoph Weidenbach
Dagstuhl Seminar Series
- 17371: "Deduction Beyond First-Order Logic" (2017)
- 13411: "Deduction and Arithmetic" (2013)
- 09411: "Interaction versus Automation: The two Faces of Deduction" (2009)
- 07401: "Deduction and Decision Procedures" (2007)
- 05431: "Deduction and Applications" (2005)
- 03171: "Deduction and Infinite-state Model Checking" (2003)
- 01101: "Deduction" (2001)
- 99091: "Deduction" (1999)
- 9709: "Deduction" (1997)
- 9512: "Deduction" (1995)
- 9310: "Deduction" (1993)
Classification
- Artificial Intelligence / Robotics
- Semantics / Formal Methods
- Verification / Logic
Keywords
- Automated Deduction
- Models
- Proofs
- Decision Procedures
- SMT
- SAT
- ATP
Buchausstellung im Erdgeschoss der Bibliothek
(nur in der Veranstaltungswoche).
In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.
Download Übersichtsflyer (PDF).
Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.
Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet und im Erdgeschoss der Bibliothek präsentiert.
Seminar Homepage : Letzte Änderung 22.01.2018, 07:18 Uhr