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?

• 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]