Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Open Access
- 10 January 2025
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 156-170
Abstract
We report on the formalization of a sufficient condition for confluence of first-order left-linear rewrite systems within the proof assistant Isabelle/HOL. This criterion, originally proposed by Okui (1998), is based on simultaneous critical pairs, which finitely represent peaks consisting of a multi-step and a normal step. It properly subsumes the formalized result on development-closed critical pairs.Keywords
Funding Information
- FWF (I5943)
This publication has 21 references indexed in Scilit:
- CSI: New Evidence – A Progress Report2017
- Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems2016
- Sledgehammer: Judgement Day2010
- A Formalization of the Knuth–Bendix(–Huet) Critical Pair TheoremJournal of Automated Reasoning, 2010
- Proving Confluence of Term Rewriting Systems Automatically2009
- Locales and Locale Expressions in Isabelle/Isar2004
- Isabelle/HOL2002
- Simultaneous critical pairs and Church-Rosser property1998
- Development closed critical pairs1996
- Confluence without termination via parallel critical pairs1996