TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 17371

Deduction Beyond First-Order Logic

( 10. Sep – 15. Sep, 2017 )

(zum Vergrößern in der Bildmitte klicken)

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/17371

Organisatoren

Kontakt


Programm

Motivation

Much research on automated deduction has traditionally focused on automated reasoning in first-order logic. First-order logic with equality is generally considered a "sweet spot" on the logic design continuum. Yet, from the point of view of several applications it can be too restrictive as a modeling and reasoning tool. In recent years, there has been a realization that while first-order reasoning is very useful to discharge the bulk of proof obligations, it must be tightly integrated with richer features to be useful in many applications. Practical problems often need a mixture of first-order proof search and some more advanced reasoning, for instance, about non-first-order-axiomatizable theories, higher-order formulas, or simply higher-level reasoning steps.

First-order logic cannot be used to finitely axiomatize many interesting theories, such as those including transitive closure operators, inductive predicates, datatypes, and standard arithmetic on integers or reals. Even provers that provide native support for some of these theories typically fail to prove trivial-looking problems because they lack general support for induction. Some applications need a richer set of constructs than those provided by first-order logic such as, for instance, the separating conjunction (*) and magic wand (-*) connectives of Separation Logic or the disjunctive well-foundedness predicates used in HSF, a popular approach to software model checking based on first-order Horn logic.

There are potential synergies between automatic first-order proving and verification methods developed in the context of richer logics. However, they have not received enough attention by the various deduction subcommunities so far. In general, there is a cultural gap between the various deduction communities that hinders cross-fertilization of ideas and progress.

This Dagstuhl Seminar will bring together first-order reasoning experts and researchers working on deduction methods and tools that go beyond first-order logic. The latter include specialists on proof methods for induction, proof planning, and other higher-order or higher-level procedures; and consumers of deduction technology whose specification languages contain non-first-order features. The main goal of the seminar is to exchange ideas and explore ways to facilitate the transition from first-order to more expressive settings.

Research questions to be discussed at the seminar include the following:

  • What higher-order features do applications need, and what features can be incorporated smoothly in existing first-order proof calculi and provers?
  • How can we best extend first-order reasoning techniques beyond first-order logic?
  • Can proof-assistant-style automation and first-order reasoning techniques be combined in a synergetic fashion?
  • What are good strategies for automatic induction and coinduction or invariant synthesis?
  • Is a higher layer of reasoning, in the spirit of proof planning, necessary to solve more difficult higher-order problems?
Copyright Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli

Summary

Much research on automated deduction has traditionally focused on automated reasoning in first-order logic. First-order logic with equality is generally considered a sweet spot on the logic design continuum. Yet, from the point of view of several applications it can be too restrictive as a modeling and reasoning tool. In recent years, there has been a realization that while first-order reasoning is very useful to discharge the bulk of proof obligations, it must be tightly integrated with richer features to be useful in many applications. Practical problems often need a mixture of first-order proof search and some more advanced reasoning, for instance, about non-first-order-axiomatisable theories, higher-order formulas, or simply higher-level reasoning steps.

First-order logic cannot be used to finitely axiomatize many interesting theories, such as those including transitive closure operators, inductive predicates, datatypes, and standard arithmetic on integers or reals. Even provers that provide native support for some of these theories typically fail to prove trivial-looking problems because they lack general support for mathematical induction. Some applications need a richer set of constructs than those provided by first-order logic such as, for instance, the separating conjunction (*) and magic wand (-*) connectives of Separation Logic or the disjunctive well-foundedness predicates used in HSF, a popular approach to software model checking based on first-order Horn logic.

There are potential synergies between automatic first-order proving and verification methods developed in the context of richer logics. However, they have not received enough attention by the various deduction sub-communities so far. In general, there is a cultural gap between the various deduction communities that hinders cross-fertilization of ideas and progress.

This Dagstuhl Seminar brought together experts in automated reasoning in first-order logic and researchers working on deduction methods and tools that go beyond first-order logic. The latter included specialists on proof methods for induction, proof planning, and other higher-order or higher-level procedures; and consumers of deduction technology whose specification languages contain non-first-order features. The main goal of the seminar was to exchange ideas and explore ways to facilitate the transition from first-order to more expressive settings.

Research questions that were discussed and answered at the seminar included the following:

  • What higher-order features do applications need, and what features can be incorporated smoothly in existing first-order proof calculi and provers?
  • How can we best extend first-order reasoning techniques beyond first-order logic?
  • Can proof-assistant-style automation and first-order reasoning techniques be combined in a synergetic fashion?
  • What are good strategies for automatic induction and coinduction or invariant synthesis?
  • Is a higher layer of reasoning, in the spirit of proof planning, necessary to solve more difficult higher-order problems?
Copyright Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli

Teilnehmer
  • Franz Baader (TU Dresden, DE) [dblp]
  • Christoph Benzmüller (FU Berlin, DE) [dblp]
  • Nikolaj S. Bjørner (Microsoft Corporation - Redmond, US) [dblp]
  • Jasmin Christian Blanchette (VU University of Amsterdam, NL) [dblp]
  • James Brotherston (University College London, GB) [dblp]
  • Chad E. Brown (Czech Technical University - Prague, CZ) [dblp]
  • Hans de Nivelle (University of Wroclaw, PL) [dblp]
  • Pascal Fontaine (LORIA & INRIA - Nancy, FR) [dblp]
  • Carsten Fuhs (Birkbeck, University of London, GB) [dblp]
  • Jürgen Giesl (RWTH Aachen, DE) [dblp]
  • Georges Gonthier (INRIA Saclay - Île-de-France, FR) [dblp]
  • Reiner Hähnle (TU Darmstadt, DE) [dblp]
  • Swen Jacobs (Universität des Saarlandes, DE) [dblp]
  • Moa Johansson (Chalmers University of Technology - Göteborg, SE) [dblp]
  • Cezary Kaliszyk (Universität Innsbruck, AT) [dblp]
  • Deepak Kapur (University of New Mexico - Albuquerque, US) [dblp]
  • Chantal Keller (University of Paris Sud - Orsay, FR) [dblp]
  • Cynthia Kop (University of Copenhagen, DK) [dblp]
  • Konstantin Korovin (University of Manchester, GB) [dblp]
  • K. Rustan M. Leino (Microsoft Corporation - Redmond, US) [dblp]
  • Tomer Libal (INRIA Saclay - Île-de-France, FR) [dblp]
  • Tobias Nipkow (TU München, DE) [dblp]
  • Naoki Nishida (Nagoya University, JP) [dblp]
  • Andrei Paskevich (University of Paris Sud - Orsay, FR) [dblp]
  • Ruzica Piskac (Yale University - New Haven, US) [dblp]
  • Andrei Popescu (Middlesex University - London, GB) [dblp]
  • Andrew Reynolds (University of Iowa - Iowa City, US) [dblp]
  • Philipp Rümmer (Uppsala University, SE) [dblp]
  • Renate Schmidt (University of Manchester, GB) [dblp]
  • Stephan Schulz (Duale Hochschule Baden-Württemberg - Stuttgart, DE) [dblp]
  • Thomas Sewell (Data61 - Sydney, AU) [dblp]
  • Natarajan Shankar (SRI - Menlo Park, US) [dblp]
  • Mihaela Sighireanu (University Paris-Diderot, FR) [dblp]
  • Viorica Sofronie-Stokkermans (Universität Koblenz-Landau, DE) [dblp]
  • Alexander Steen (FU Berlin, DE) [dblp]
  • Sorin Stratulat (University of Lorraine - Metz, FR) [dblp]
  • Thomas Ströder (Metro Systems GmbH - Düsseldorf, DE) [dblp]
  • Martin Suda (TU Wien, AT) [dblp]
  • Laurent Théry (INRIA Sophia Antipolis, FR) [dblp]
  • Cesare Tinelli (University of Iowa - Iowa City, US) [dblp]
  • Josef Urban (Czech Technical University - Prague, CZ) [dblp]
  • Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]

Verwandte Seminare
  • 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 15381: Information from Deduction: Models and Proofs (2015-09-13 - 2015-09-18) (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)
  • Dagstuhl-Seminar 26091: Revisiting the Foundations of Deduction in a New World (2026-02-22 - 2026-02-27) (Details)

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

Schlagworte
  • automated reasoning
  • automated deduction
  • decision procedures
  • higher-order logic
  • formal proof
  • program verification