Certified subterm criterion and certified usable rules

DOI10.4230/LIPICS.RTA.2010.325MaRDI QIDQ5389153zbMATH OpenOpenAlexFDO

Authors Christian Sternagel, René Thiemann

Publication date 25 April 2012

Full work available at URL http://subs.emis.de/LIPIcs/frontdoor_9fe0.html

zbMATH Keywords

certificationterm rewritingterminationtheorem proving

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Certification of Termination Proofs Using CeTA
• Certification of nontermination proofs
• Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
• Certification of complexity proofs using CeTA
• Certified rule labeling

Cited in

(3)

• Termination of Isabelle functions via termination of rewriting
• Certification of Termination Proofs Using CeTA
• Certification of complexity proofs using CeTA

Describes a project that uses

Uses Software

• A3PAT
• CeTA
• CoLoR
• Isabelle/HOL
• Tyrolean

This page was built for publication: Certified subterm criterion and certified usable rules

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