Systèmes Canoniques Abstraits : Application à la Déduction Naturelle et à la Complétion - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2005

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

Résumé

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.
Fichier principal
Vignette du fichier
aacs.pdf (615.26 Ko) Télécharger le fichier
Loading...

Dates et versions

inria-00000773 , version 1 (17-11-2005)

Identifiants

  • HAL Id : inria-00000773 , version 1

Citer

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⟩
92 Consultations
74 Téléchargements

Partager

Gmail Facebook X LinkedIn More