Document Open Access Logo

Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)

Authors Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, Cesare Tinelli and all authors of the abstracts in this report



PDF
Thumbnail PDF

File

DagRep.7.9.26.pdf
  • Filesize: 2.46 MB
  • 21 pages

Document Identifiers

Author Details

Jasmin Christian Blanchette
Carsten Fuhs
Viorica Sofronie-Stokkermans
Cesare Tinelli
and all authors of the abstracts in this report

Cite AsGet BibTex

Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli. Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). In Dagstuhl Reports, Volume 7, Issue 9, pp. 26-46, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/DagRep.7.9.26

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

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail