http://www.dagstuhl.de/17371

10. – 15. September 2017, Dagstuhl Seminar 17371

Deduction Beyond First-Order Logic

Organisatoren

Jasmin Christian Blanchette (VU University of Amsterdam, NL)
Carsten Fuhs (Birkbeck, University of London, GB)
Viorica Sofronie-Stokkermans (Universität Koblenz-Landau, DE)
Cesare Tinelli (University of Iowa – Iowa City, US)

Auskunft zu diesem Dagstuhl Seminar erteilen

Simone Schilke zu administrativen Fragen

Michael Gerke zu wissenschaftlichen Fragen

Dagstuhl Reports

Wir bitten die Teilnehmer uns bei der notwendigen Dokumentation zu unterstützen und Abstracts zu ihrem Vortrag, Ergebnisse aus Arbeitsgruppen, etc. zur Veröffentlichung in unserer Serie Dagstuhl Reports einzureichen über unser
Dagstuhl Reports Submission System.

Dokumente

Teilnehmerliste
Gemeinsame Dokumente
Dagstuhl Seminar Wiki
Programm des Dagstuhl Seminars [pdf]

(Zum Einloggen bitte Seminarnummer und Zugangscode verwenden)

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?

License
  Creative Commons BY 3.0 DE
  Jasmin Christian Blanchette and Carsten Fuhs and Viorica Sofronie-Stokkermans and Cesare Tinelli

Dagstuhl Seminar Series

Classification

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

Keywords

  • Automated reasoning
  • Automated deduction
  • Decision procedures
  • Higher-order logic
  • Formal proof
  • Program verification

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

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).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

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.