eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Reports
2192-5283
2018-03-07
26
46
10.4230/DagRep.7.9.26
article
Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)
Blanchette, Jasmin Christian
Fuhs, Carsten
Sofronie-Stokkermans, Viorica
Tinelli, Cesare
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.
https://drops.dagstuhl.de/storage/04dagstuhl-reports/volume07/issue09/17371/DagRep.7.9.26/DagRep.7.9.26.pdf
Automated Deduction
Program Verification
Certification