Deduction and Arithmetic (Dagstuhl Seminar 13411)

Authors Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, Christoph Weidenbach and all authors of the abstracts in this report

Thumbnail PDF


  • Filesize: 1.09 MB
  • 24 pages

Document Identifiers

Author Details

Nikolaj Bjorner
Reiner Hähnle
Tobias Nipkow
Christoph Weidenbach
and all authors of the abstracts in this report

Cite AsGet BibTex

Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach. Deduction and Arithmetic (Dagstuhl Seminar 13411). In Dagstuhl Reports, Volume 3, Issue 10, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


This report documents the program and the outcomes of Dagstuhl Seminar 13411 "Deduction and Arithmetic". The aim of this seminar was to bring together researchers working in deduction and fields related to arithmetic constraint solving. Current research in deduction can be categorized in three main strands: SMT solvers, automated first-order provers, and interactive provers. Although dealing with arithmetic has been in focus of all three for some years, there is still need of much better support of arithmetic. Reasong about arithmetic will stay at the center of attention in all three main approaches to automated deduction during the coming five to ten years. The seminar was an important event for the subcommunities involved that made it possible to communicate with each other so as to avoid duplicate effort and to exploit synergies. It succeeded also in identifying a number of important trends and open problems.
  • Automated Deduction; Program Verification; Arithmetic Constraint Solving


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads