A formalization of diagrammatic proofs in abstract rewritingReportar como inadecuado

A formalization of diagrammatic proofs in abstract rewriting - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LIX - Laboratoire d-informatique de l-École polytechnique Palaiseau 2 LOGICAL - Logic and computing UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, Polytechnique - X, 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.

Keywords : formalization diagrammatic proofs rewriting

Autor: Julien Narboux -

Fuente: https://hal.archives-ouvertes.fr/


Documentos relacionados