User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse





Deduction and Arithmetic


Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

External Ressource
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Bjørner, N., Hähnle, R., Nipkow, T., & Weidenbach, C. (Eds.). (2014). Deduction and Arithmetic. Wadern: Schloss Dagstuhl. doi:10.4230/DagRep.3.10.1.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0024-C36B-3
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.