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

DOI10.1007/978-3-319-43144-4_18MaRDI QIDQ2829264zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 6744203 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Automated certified proofs with CiME3
• CSI -- a confluence tool
• Certification of Termination Proofs Using CeTA
• Certified rule labeling
• CoLL: a confluence tool for left-linear term rewrite systems
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Confluence of non-left-linear TRSs via relative termination
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Developing developments
• Disproving confluence of term rewriting systems by interpretation and ordering
• Isabelle/HOL. A proof assistant for higher-order logic
• Proving Confluence of Term Rewriting Systems Automatically
• Reachability Analysis with State-Compatible Automata
• Relative undecidability in term rewriting. II: The confluence hierarchy
• Term Rewriting and All That

Cited in

(8)

• From LCF to Isabelle/HOL
• Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
• Confluence Criteria for Logically Constrained Rewrite Systems
• CoLL: a confluence tool for left-linear term rewrite systems
• Certifying confluence proofs via relative termination and rule labeling
• Confluence by critical pair analysis revisited
• Certifying confluence of almost orthogonal CTRSs via exact tree automata completion
• ProTeM: a proof term manipulator (system description)

Describes a project that uses

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)