A formalization of diagrammatic proofs in abstract rewriting
Résumé
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.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)