Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381)

Abstract

This report documents the program and the outcomes of  Dagstuhl Seminar 15381 "Information from Deduction: Models and Proofs". The aim of the seminar was to bring together researchers working in deduction and applications that rely on models and proofs produced by deduction tools.
Proofs and models serve two main purposes: (1) as an upcoming paradigm towards the next generation of automated deduction tools where search relies on (partial) proofs and models; (2) as the actual result of an automated deduction tool, which is increasingly integrated into application tools.
Applications are rarely well served by a simple yes/no answer from a deduction tool. Many use models as certificates for satisfiability to extract feasible program executions; others use proof objects as certificates for unsatisfiability in  the context of high-integrity systems development. Models and proofs even play an integral role within deductive
tools as major methods for efficient proof search rely on refining a simultaneous search for a model or a proof. The topic is in a sense evergreen: models and proofs will always be an integral part of deduction. Nonetheless, the seminar was especially timely given recent activities in deduction and applications, and it enabled researchers from different subcommunities to communicate with each other towards exploiting synergies.