License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagRep.3.10.1
URN: urn:nbn:de:0030-drops-44250
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4425/
Go back to Dagstuhl Reports

Bjorner, Nikolaj ; Hähnle, Reiner ; Nipkow, Tobias ; Weidenbach, Christoph
Weitere Beteiligte (Hrsg. etc.): Nikolaj Bjorner and Reiner Hähnle and Tobias Nipkow and Christoph Weidenbach

Deduction and Arithmetic (Dagstuhl Seminar 13411)

pdf-format:
dagrep_v003_i010_p001_s13411.pdf (1 MB)

Abstract

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.

BibTeX - Entry

@Article{bjorner_et_al:DR:2014:4425,
  author =	{Nikolaj Bjorner and Reiner H{\"a}hnle and Tobias Nipkow and Christoph Weidenbach},
  title =	{{Deduction and Arithmetic (Dagstuhl Seminar 13411)}},
  pages =	{1--24},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{3},
  number =	{10},
  editor =	{Nikolaj Bjorner and Reiner H{\"a}hnle and Tobias Nipkow and Christoph Weidenbach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4425},
  URN =		{urn:nbn:de:0030-drops-44250},
  doi =		{10.4230/DagRep.3.10.1},
  annote =	{Keywords: Automated Deduction; Program Verification; Arithmetic Constraint Solving}
}

Keywords: Automated Deduction; Program Verification; Arithmetic Constraint Solving
Collection: Dagstuhl Reports, Volume 3, Issue 10
Issue Date: 2014
Date of publication: 07.02.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI