Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)
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.
Automated Deduction
Program Verification
Certification
26-46
Regular Paper
Jasmin Christian
Blanchette
Jasmin Christian Blanchette
Carsten
Fuhs
Carsten Fuhs
Viorica
Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Cesare
Tinelli
Cesare Tinelli
10.4230/DagRep.7.9.26
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode