Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000773
Contributor : Guillaume Burel <>
Submitted on : Thursday, November 17, 2005 - 4:29:14 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Tuesday, September 11, 2012 - 12:51:51 PM

File

Identifiers

  • HAL Id : inria-00000773, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

190

Files downloads

117