A formalization of diagrammatic proofs in abstract rewriting

Julien Narboux 1, 2
2 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : Diagrams are in common use in the rewriting community. In this paper, we present a formalization of this kind of diagrams. We give a formal definition for the diagrams used to state properties. We propose inference rules to formalize the reasoning depicted by some well known diagrammatic proofs : a transitivity property of some abstract rewriting systems and the Newman's lemma. We show that the system proposed is both correct and complete for a class of formulas called coherent logic.
Type de document :
Pré-publication, Document de travail
2006
Liste complète des métadonnées

https://hal.inria.fr/inria-00180065
Contributeur : Julien Narboux <>
Soumis le : mercredi 17 octobre 2007 - 15:44:09
Dernière modification le : mercredi 25 avril 2018 - 10:45:25
Document(s) archivé(s) le : dimanche 11 avril 2010 - 21:58:18

Fichier

diagrams_narboux.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00180065, version 1

Collections

Citation

Julien Narboux. A formalization of diagrammatic proofs in abstract rewriting. 2006. 〈inria-00180065〉

Partager

Métriques

Consultations de la notice

252

Téléchargements de fichiers

51