http://www.dagstuhl.de/15381

September 13 – 18 , 2015, Dagstuhl Seminar 15381

Information from Deduction: Models and Proofs

Organizers

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)


1 / 3 >

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 5, Issue 9 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl's Impact: Documents available
Dagstuhl Seminar Schedule [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?
License
  Creative Commons BY 3.0 Unported license
  Nikolaj S. Bjorner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, and Christoph Weidenbach

Dagstuhl Seminar Series

Classification

  • Artificial Intelligence / Robotics
  • Semantics / Formal Methods
  • Verification / Logic

Keywords

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

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.