Logo image
Back
Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)
Journal article   Open access

Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)

Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans and Cesare Tinelli
Dagstuhl Reports, Vol.7(9), pp.26-46
2018
DOI: 10.4230/dagrep.7.9.26
url
https://doi.org/10.4230/dagrep.7.9.26View
Published (Version of record) Open Access

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.
Program Verification Automated Deduction Certification

Details

Metrics

19 Record Views
Logo image