License
When quoting this document, please refer to the following
DOI: 10.4230/DagRep.7.9.26
URN: urn:nbn:de:0030-drops-85872
URL: http://drops.dagstuhl.de/opus/volltexte/2018/8587/
Go back to Dagstuhl Reports


Blanchette, Jasmin Christian ; Fuhs, Carsten ; Sofronie-Stokkermans, Viorica ; Tinelli, Cesare
Weitere Beteiligte (Hrsg. etc.): Jasmin Christian Blanchette and Carsten Fuhs and Viorica Sofronie-Stokkermans and Cesare Tinelli

Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)

pdf-format:
dagrep_v007_i009_p026_17371.pdf (2 MB)


Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 17371 "Deduction Beyond First-Order Logic." Much research in the past two decades was dedicated to automating first-order logic with equality. However, applications often need reasoning beyond this logic. This includes genuinely higher-order reasoning, reasoning in theories that are not finitely axiomatisable in first-order logic (such as those including transitive closure operators or standard arithmetic on integers or reals), or reasoning by mathematical induction. Other practical problems need a mixture of first-order proof search and some more advanced reasoning (for instance, about higher-order formulas), or simply higher-level reasoning steps. The aim of the seminar was to bring together first-order automated reasoning experts and researchers working on deduction methods and tools that go beyond first-order logic. The seminar was dedicated to the exchange of ideas to facilitate the transition from first-order to more expressive settings.

BibTeX - Entry

@Article{blanchette_et_al:DR:2018:8587,
  author =	{Jasmin Christian Blanchette and Carsten Fuhs and Viorica Sofronie-Stokkermans and Cesare Tinelli},
  title =	{{Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)}},
  pages =	{26--46},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{9},
  editor =	{Jasmin Christian Blanchette and Carsten Fuhs and Viorica Sofronie-Stokkermans and Cesare Tinelli},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8587},
  URN =		{urn:nbn:de:0030-drops-85872},
  doi =		{10.4230/DagRep.7.9.26},
  annote =	{Keywords: Automated Deduction, Program Verification, Certification}
}

Keywords: Automated Deduction, Program Verification, Certification
Seminar: Dagstuhl Reports, Volume 7, Issue 9
Issue Date: 2018
Date of publication: 07.03.2018


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