Layer Systems for Confluence — Formalized

Bertram Felgenhauer and Franziska Rapp

Proceedings of the 15th International Colloquium on Theoretical Aspects of Computing (ICTAC 2018), Lecture Notes in Computer Science 11187, pp. 173 – 190, 2018..


Toyama’s theorem states that the union of two confluent term rewrite systems with disjoint signatures is again confluent. This is a fundamental result in term rewriting, and several proofs appear in the literature. The underlying proof technique has been adapted to prove further results like persistence of confluence (if a many-sorted term rewrite system is confluent, then the underlying unsorted system is confluent) or the preservation of confluence by currying.

In this paper we present a formalization of modularity and related results in Isabelle/HOL. The formalization is based on layer systems, which cover modularity, persistence, currying (and more) in a single framework. The persistence result has been integrated into the certifier CeTA and the confluence tool CSI, allowing us to check confluence proofs based on persistent decomposition, of which modularity is a special case.


  PDF |    doi:10.1007/978-3-030-02508-3_10 |  © Creative Commons License – CC BY 4.0  


author = "Bertram Felgenhauer and Franziska Rapp",
title = "Layer Systems for Confluence---Formalized",
booktitle = "Proceedings of the 15th International Colloquium on Theoretical
Aspects of Computing -- ICTAC 2018",
editor = "Bernd Fischer and Tarmo Uustalu",
series = "Lecture Notes in Computer Science",
volume = 11187,
oages = "173--190",
year = 2018,
doi = "10.1007/978-3-030-02508-3_10"
Nach oben scrollen