Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems

DOI10.1007/978-3-319-43144-4_18zbMath1478.68117OpenAlexW2489846514MaRDI QIDQ2829264

Aart Middeldorp, Julian Nagele

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: http://qmro.qmul.ac.uk/xmlui/handle/123456789/37303

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Unnamed Item ⋮ Unnamed Item ⋮ From LCF to Isabelle/HOL ⋮ Confluence by critical pair analysis revisited

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• CeTA
• CSI
• CoLoR
• CiME
• Saigawa
• IsaFoR
• CoLL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Developing developments
• Isabelle/HOL. A proof assistant for higher-order logic
• Relative undecidability in term rewriting. II: The confluence hierarchy
• Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering
• Confluence of Non-Left-Linear TRSs via Relative Termination
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• Certification of Termination Proofs Using CeTA
• CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
• Proving Confluence of Term Rewriting Systems Automatically
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Term Rewriting and All That
• CSI – A Confluence Tool
• Certified Rule Labeling
• Reachability Analysis with State-Compatible Automata