Confluence by decreasing diagrams – Formalized

PorJosé A. Alonso

Se ha publicado un trabajo de formalización de sistemas de reescritura en Isabelle/HOL titulado Confluence by decreasing diagrams – formalized.

Su autor es Harald Zankl (de la Universidad de Insbruck, Austria).

Su resumen es

Decreasing diagrams are a complete characterization of confluence for abstract rewrite systems whose convertibility classes are countable. In this paper we present a formalization of decreasing diagrams in the theorem prover Isabelle. The main contribution is a formal proof that any locally decreasing abstract rewrite system is confluent.

Las teorías Isabelle/HOL correspondiente al trabajo se encuentran aquí.