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.7.9.26
URN: urn:nbn:de:0030-drops-85872
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8587/
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)
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 |
|
Collection: |
|
Dagstuhl Reports, Volume 7, Issue 9 |
|
Issue Date: |
|
2018 |
|
Date of publication: |
|
07.03.2018 |
