Certified rule labeling

DOI10.4230/LIPICS.RTA.2015.269MaRDI QIDQ5277884zbMATH OpenOpenAlexFDO

Authors Julian Nagele, Harald Zankl

Publication date 12 July 2017

Full work available at URL https://dx.doi.org/10.4230/LIPIcs.RTA.2015.269

zbMATH Keywords

certificationconfluencedecreasing diagramsterm rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Certifying confluence proofs via relative termination and rule labeling
• Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
• Automated confluence proof by decreasing diagrams based on rule-labelling
• Labelings for Decreasing Diagrams.
• Labelings for decreasing diagrams

Cited in

(4)

• Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
• Certification of classical confluence results for left-linear term rewrite systems
• Certifying confluence proofs via relative termination and rule labeling
• Certified subterm criterion and certified usable rules

Describes a project that uses

Uses Software

• CiME
• ACL2
• Isabelle
• CeTA
• CSI

This page was built for publication: Certified rule labeling

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