Automating coherent logic

30Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.
Get full text

Abstract

First-order coherent logic (CL) extends resolution logic in that coherent formulas allow certain existential quantifications. A substantial number of reasoning problems (e.g., in confluence theory, lattice theory and projective geometry) can be formulated directly in CL without any clausification or Skolemization. CL has a natural proof theory, reasoning is constructive and proof objects can easily be obtained. We prove completeness of the proof theory and give a linear translation from FOL to CL that preserves logical equivalence. These properties make CL well-suited for providing automated reasoning support to logical frameworks. The proof theory has been implemented in Prolog, generating proof objects that can be verified directly in the proof assistant Coq. The prototype has been tested on the proof of Hessenberg's Theorem, which could be automated to a considerable extent. Finally, we compare the prototype to some automated theorem provers on selected problems. © Springer-Verlag Berlin Heidelberg 2005.

Cite

CITATION STYLE

APA

Bezem, M., & Coquand, T. (2005). Automating coherent logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3835 LNAI, pp. 246–260). https://doi.org/10.1007/11591191_18

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free