Completion is an Instance of Abstract Canonical System Inference

Guillaume Burel 1 Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Abstract canonical systems and inference (ACSI) were introduced to formalize the intuitive notions of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedures. Since this abstract framework is intended to be generic, it is of fundamental interest to show its adequacy to represent the main systems of interest. This has been done for ground completion (where all equational axioms are ground) but was still an open question for the general completion process. By showing that the standard completion is an instance of the ACSI framework we close the question. For this purpose, two proof representations, proof terms and proofs by replacement, are compared to built a proof ordering that provides an instantiation adapted to the abstract canonical system framework.
Type de document :
Communication dans un congrès
Kokichi Futatsugi and Jean-Pierre Jouannaud and José Meseguer. Algebra, Meaning, and Computation: A Festschrift Symposium in Honor of Joseph Goguen, Jun 2006, San Diego/USA, Springer Verlag, 4060, pp.497-520, 2006, Lecture Notes in Computer Science. 〈10.1007/11780274_26〉
Liste complète des métadonnées

Littérature citée [39 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00000775
Contributeur : Guillaume Burel <>
Soumis le : mardi 12 septembre 2006 - 17:54:51
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : lundi 20 septembre 2010 - 16:56:41

Identifiants

Collections

Citation

Guillaume Burel, Claude Kirchner. Completion is an Instance of Abstract Canonical System Inference. Kokichi Futatsugi and Jean-Pierre Jouannaud and José Meseguer. Algebra, Meaning, and Computation: A Festschrift Symposium in Honor of Joseph Goguen, Jun 2006, San Diego/USA, Springer Verlag, 4060, pp.497-520, 2006, Lecture Notes in Computer Science. 〈10.1007/11780274_26〉. 〈inria-00000775v2〉

Partager

Métriques

Consultations de la notice

122

Téléchargements de fichiers

97