A formalization of diagrammatic proofs in abstract rewriting

Julien Narboux (1, 2)

1 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
2 LOGICAL - Logic and computing

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.

Mots clés: formalization; diagrammatic proofs; rewriting

Domaines: Logique en informatique [cs.LO]

Julien Narboux. A formalization of diagrammatic proofs in abstract rewriting. 2006. ⟨inria-00180065⟩