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.
CITATION STYLE
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
Mendeley helps you to discover research relevant for your work.