TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 13411

Deduction and Arithmetic

( Oct 06 – Oct 11, 2013 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/13411

Organizers

Contact



Schedule

Motivation

Arithmetic plays a fundamental role in deduction. Logical constraints over arithmetical properties occur frequently in classical theorems in mathematics, as well as in program analysis and verification. The first automatic theorem prover was an implementation of Presburger Arithmetic in 1954. With the availability of powerful predicate calculus proof procedures some years later, arithmetic would be relegated to the sidelines. Interest in arithmetic revived in the 1980s with the advent of powerful interactive theorem provers that needed and supported arithmetic for their applications. The need for efficient computer aided deduction with support for arithmetic in the area of program analysis and verification recently gave birth to a new technology, so called SMT solvers.

Thus we have three strands of automated deduction

  1. SMT solvers,
  2. automated first-order provers, and
  3. interactive provers in need of (more) arithmetic.

SMT:
SMT solvers distinguish themselves by integrating built-in support for a combination of theories, including prominently the theory of arithmetic. Most often handling arithmetic formulas in isolation is not sufficient. Applications typically use a non-disjoint combination of arithmetic and other theory reasoning. SMT solvers nowadays handle quantifier-free arithmetic well, but are not directly equipped to solve arithmetical formulas with quantifiers. Recent progress on building in quantifier-elimination procedures for linear and non-linear arithmetic have made practical integration of such richer arithmetic deduction viable.

ATP:
Research in first-order logic theorem proving used to concentrate on efficient calculi in general and the integration of equational theories in particular. It is obvious that further integration of "richer" arithmetic theories into first-order logic should be done by rather a combination approach than an integration approach. One major challenge of combining first-order logic calculi with arithmetic procedures is that of compactness/completeness and termination. While Boolean combinations of ground atoms, as they are considered by SMT solvers typically do not cause trouble with respect to those challenges, combining first-order clauses with an arithmetic theory can never result in a compact/complete/terminating calculus, in general. The actual combination typically requires the solution of purely arithmetic problems in order to establish valid inferences and simplifications. These problems are of a specific nature in that the form of the arithmetic formulas and the way they need to be tested require specific variants of the known arithmetic procedures.

ITP:
Interactive theorem provers initially came with built-in decision procedures for quantifier-free linear arithmetic. More foundational systems then developed new techniques to implement these decision procedures by reducing them to pure logic, trading efficiency for guaranteed correctness. Aspects of arithmetic reasoning are present in deductive software verification systems: interactive systems combine a number of automatic arithmetic reasoning methods and control them with heuristics that are specific for verification. A challenging application of interactive proof and arithmetic is the Flyspeck project, an effort to formalize Hales' proof of the Kepler conjecture in an interactive theorem prover.

The time is clearly ripe to bring together experts in the above subareas of deduction, and in reasoning about arithmetic, to exchange experiences and insights. The research questions to be pursued and answered include:

  • Which arithmetic problems are best solved with which approach?
  • How to handle very complex numeric representations such as the IEEE floating point standard with a high degree of automation?
  • Arithmetic in combination with other theories results easily in languages with a very complex decision problem---how can a high degree of automation be obtained nevertheless?
  • How can SMT-based reasoning be combined with Abstract Interpretation?
  • What is the best way to incorporate arithmetic simplification available in computer algebra systems into deductive frameworks?
  • How can the specific structure of arithmetic problems generated by deduction systems be exploited?

Summary

Arithmetic plays a fundamental role in deduction. Logical constraints over arithmetical properties occur frequently in classical theorems in mathematics, as well as in program analysis and verification. The first automatic theorem prover was an implementation of Presburger Arithmetic in 1954. With the availability of powerful predicate calculus proof procedures some years later, arithmetic would be relegated to the sidelines. Interest in arithmetic revived in the 1980s with the advent of powerful interactive theorem provers that needed and supported arithmetic for their applications. The need for efficient computer aided deduction with support for arithmetic in the area of program analysis and verification recently gave birth to a new technology, so called SMT solvers.

Thus we have three strands of automated deduction: SMT solvers, automated first-order provers, and interactive provers in need of (more) arithmetic.

SMT SMT (satisfiability modulo theories) solvers distinguish themselves by integrating built-in support for a combination of theories, including prominently the theory of arithmetic. Most often handling arithmetic formulas in isolation is not sufficient. Applications typically use a non-disjoint combination of arithmetic and other theory reasoning. SMT solvers nowadays handle quantifier-free arithmetic well, but are not directly equipped to solve arithmetical formulas with quantifiers. Recent progress on building in quantifier-elimination procedures for linear and non-linear arithmetic have made practical integration of such richer arithmetic deduction viable.

ATP Research in first-order logic theorem proving used to concentrate on efficient calculi in general and the integration of equational theories in particular. It is obvious that further integration of ``richer'' arithmetic theories into first-order logic should be done by rather a combination approach than an integration approach. One major challenge of combining first-order logic calculi with arithmetic procedures is that of compactness/completeness and termination. While Boolean combinations of ground atoms, as they are considered by SMT solvers typically do not cause trouble with respect to those challenges, combining first-order clauses with an arithmetic theory can never result in a compact/complete/terminating calculus, in general. The actual combination typically requires the solution of purely arithmetic problems in order to establish valid inferences and simplifications. These problems are of a specific nature in that the form of the arithmetic formulas and the way they need to be tested require specific variants of the known arithmetic procedures.

ITP Interactive theorem provers initially came with built-in decision procedures for quantifier-free linear arithmetic. More foundational systems then developed new techniques to implement these decision procedures by reducing them to pure logic, trading efficiency for guaranteed correctness. Aspects of arithmetic reasoning are present in deductive software verification systems: interactive systems combine a number of automatic arithmetic reasoning methods and control them with heuristics that are specific for verification. A challenging application of interactive proof and arithmetic is the Flyspeck project, an effort to formalize Hales's proof of the Kepler conjecture in an interactive theorem prover.

The Dagstuhl seminar was a timely event that brought together experts in the above subareas of deduction, and in reasoning about arithmetic, to exchange experiences and insights. The research questions pursued and answered included:

  • Which arithmetic problems are best solved with which approach?
  • How to handle very complex numeric representations such as the IEEE floating-point standard with a high degree of automation?
  • Arithmetic in combination with other theories results easily in languages with a very complex decision problem---how can a high degree of automation be obtained nevertheless?
  • How can SMT-based reasoning be combined with model-based reasoning?
  • What is the best way to incorporate arithmetic simplification available in computer algebra systems into deductive frameworks?
  • How can the specific structure of arithmetic problems generated by deduction systems be exploited?

In addition to the technical contributions, the seminar participants attempted in an open discussion session to identify the major trends and open questions around Deduction and Arithmetic.

Copyright Nikolaj S. Bjørner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach

Participants
  • Wolfgang Ahrendt (Chalmers UT - Göteborg, SE) [dblp]
  • Jeremy Avigad (Carnegie Mellon University, US) [dblp]
  • Peter Baumgartner (NICTA - Canberra, AU) [dblp]
  • Bernhard Beckert (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Nikolaj S. Bjørner (Microsoft Corporation - Redmond, US) [dblp]
  • Jasmin Christian Blanchette (TU München, DE) [dblp]
  • Richard Bubel (TU Darmstadt, DE) [dblp]
  • Eva Darulova (EPFL - Lausanne, CH) [dblp]
  • Leonardo de Moura (Microsoft Corporation - Redmond, US) [dblp]
  • Stephan Falke (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Pascal Fontaine (LORIA - Nancy, FR) [dblp]
  • Martin Fränzle (Universität Oldenburg, DE) [dblp]
  • Carsten Fuhs (University College London, GB) [dblp]
  • Jürgen Giesl (RWTH Aachen, DE) [dblp]
  • Alberto Griggio (Bruno Kessler Foundation - Trento, IT) [dblp]
  • Arie Gurfinkel (Carnegie Mellon University - Pittsburgh, US) [dblp]
  • Reiner Hähnle (TU Darmstadt, DE) [dblp]
  • James J. Hunt (aicas GmbH - Karlsruhe, DE) [dblp]
  • Dejan Jovanovic (SRI - Menlo Park, US) [dblp]
  • Tim A. King (New York University, US) [dblp]
  • Konstantin Korovin (University of Manchester, GB) [dblp]
  • Marek Kosta (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Jérôme Leroux (University of Bordeaux, FR) [dblp]
  • Assia Mahboubi (INRIA Saclay - Île-de-France, FR) [dblp]
  • Aart Middeldorp (Universität Innsbruck, AT) [dblp]
  • David Monniaux (VERIMAG - Grenoble, FR) [dblp]
  • Wojciech Mostowski (University of Twente, NL) [dblp]
  • Tobias Nipkow (TU München, DE) [dblp]
  • Grant Olney Passmore (University of Cambridge, GB & University of Edinburgh, GB) [dblp]
  • Ruzica Piskac (Yale University, US) [dblp]
  • André Platzer (Carnegie Mellon University, US) [dblp]
  • Enric Rodríguez-Carbonell (UPC - Barcelona, ES) [dblp]
  • Philipp Rümmer (Uppsala University, SE) [dblp]
  • Peter H. Schmitt (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Carsten Sinz (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Viorica Sofronie-Stokkermans (Universität Koblenz-Landau, DE) [dblp]
  • Christian Sternagel (JAIST - Ishikawa, JP) [dblp]
  • Thomas Sturm (MPI für Informatik - Saarbrücken, DE) [dblp]
  • René Thiemann (Universität Innsbruck, AT) [dblp]
  • Cesare Tinelli (University of Iowa - Iowa City, US) [dblp]
  • Tjark Weber (Uppsala University, SE) [dblp]
  • Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]

Related Seminars
  • 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 15381: Information from Deduction: Models and Proofs (2015-09-13 - 2015-09-18) (Details)
  • Dagstuhl Seminar 17371: Deduction Beyond First-Order Logic (2017-09-10 - 2017-09-15) (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)

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

Keywords
  • Automated Deduction
  • Program Verification
  • Arithmetic Constraint Solving