Formalized Signature Extension Results for Equivalence
Alexander Lochmann, Fabian Mitterwallner, Aart MiddeldorpProceedings of the 11th International Workshop on Confluence (IWC 2022), pp. 42-47, 2022.
Abstract
Conversion equivalence and normalization equivalence are important properties of two rewrite systems. We investigate how many constants are needed to reduce these properties to their ground versions for linear variable-separated rewrite systems. Our results are implemented in the decision tool FORT-h and formalized in Isabelle/HOL. The latter enables the validation of the proofs produced by the former in the certifier FORTify.
BibTeX
@inproceedings{ALFMAM-IWC22, author = "Alexander Lochmann and Fabian Mitterwallner and Aart Middeldorp", title = "Formalized Signature Extension Results for Equivalence", booktitle = "Proceedings of the 11th International Workshop on Confluence", pages = "42--47", year = 2022 }