Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
DOI10.1007/978-3-319-43144-4_18zbMATH Open1478.68117OpenAlexW2489846514MaRDI QIDQ2829264FDOQ2829264
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
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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Certification of Termination Proofs Using CeTA
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification 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
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Developing developments
- Proving Confluence of Term Rewriting Systems Automatically
- CSI – A Confluence Tool
- 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
- Certified Rule Labeling
Cited In (5)
Uses Software
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)
