Certification of classical confluence results for left-linear term rewrite systems

DOI10.1007/978-3-319-43144-4_18zbMATH Open1478.68117OpenAlexW2489846514MaRDI QIDQ2829264FDOQ2829264

Authors: Julian Nagele, Aart Middeldorp 

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

Recommendations

• Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
• Certifying confluence of almost orthogonal CTRSs via exact tree automata completion
• Layer systems for confluence -- formalized
• Certifying confluence proofs via relative termination and rule labeling
• Certified rule labeling

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)

Cites Work

• Certification of Termination Proofs Using CeTA
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
• Isabelle/HOL. A proof assistant for higher-order logic
• Term Rewriting and All That
• Title not available (Why is that?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Developing developments
• Proving Confluence of Term Rewriting Systems Automatically
• CSI -- a confluence tool
• Automated certified proofs with CiME3
• Reachability Analysis with State-Compatible Automata
• 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
• Title not available (Why is that?)
• Certified Rule Labeling

Cited In (5)

• Confluence by critical pair analysis revisited
• Title not available (Why is that?)
• Title not available (Why is that?)
• From LCF to Isabelle/HOL
• Confluence Criteria for Logically Constrained Rewrite Systems

Uses Software

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

This page was built for publication: Certification of classical confluence results for left-linear term rewrite systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829264)