HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Systèmes Canoniques Abstraits : Application à la Déduction Naturelle et à la Complétion

Guillaume Burel 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Canonical Systems and Inference (ACSI) were introduced by N. Dershowitz and C. Kirchner to formalize the intuitive notion of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedures. Since this abstract framework, based on proof orderings, is intended to be generic, it is of fundamental interest to show its adequacy to represent the main systems of interest. It is here done for minimal propositional natural deduction, and for the standard (Knuth-Bendix) completion, closing an open question. For the first proof system, a generalisation of the ACSI is needed. We provide here a conservative one, in the sense that all results of the original framework still hold. For the second one, two proof representations, proof terms and proofs by replacement, are compared to built a proof ordering that provides an instantiation adapted to the ACSI framework.
Document type :
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

Contributor : Guillaume Burel Connect in order to contact the contributor
Submitted on : Thursday, November 17, 2005 - 4:29:14 PM
Last modification on : Friday, February 4, 2022 - 3:31:27 AM
Long-term archiving on: : Tuesday, September 11, 2012 - 12:51:51 PM



  • HAL Id : inria-00000773, version 1



Guillaume Burel. Systèmes Canoniques Abstraits : Application à la Déduction Naturelle et à la Complétion. [Travaux universitaires] Rapport de stage de master 2 annee MPRI / Universite Paris 7, 2005, pp.93. ⟨inria-00000773⟩



Record views


Files downloads