Abstract

Ground-confluence and confluence do not coincide. However, for the class of left-linear right-ground TRSs confluence can be reduced to ground-confluence by extending the signature with fresh constants. We present a formalization in Isabelle/HOL of a more general result, for linear variable-separated rewrite systems. From this formalization we obtain a sound procedure to decide confluence, commutation and unique normal forms of such systems. We implemented this procedure in the decision tool FORT-h, which also can produce machine checkable proofs, and in the certifier FORTify to validate these.

BibTeX Entry

@inproceedings{LMM-IWC21,
 author    = "Alexander Lochmann and Fabian Mitterwallner and Aart
              Middeldorp",
 title     = "Formalized Signature Extension Results for Confluence,
              Commutation and Unique Normal Forms",
 booktitle = "Proceedings of the 10th International Workshop on Confluence",
 editor    = "Samuel Mimram and Camilo Rocha",
 pages     = "25--30",
 year      = 2021
}