First-order formative rules

DOI10.1007/978-3-319-08918-8_17MaRDI QIDQ5170820zbMATH OpenOpenAlexFDO

Authors Carsten Fuhs, Cynthia Kop

Publication date 24 July 2014

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1404.7695, https://eprints.bbk.ac.uk/id/eprint/13547/1/RTATLCA14-formative.pdf

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Abstract: This paper discusses the method of formative rules for first-order term rewriting, which was previously defined for a higher-order setting. Dual to the well-known usable rules, formative rules allow dropping some of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, the first-order setting allows for significant improvements of the technique.

Recommendations

• scientific article; zbMATH DE number 1405629
• Higher-Order Orderings for Normal Rewriting
• scientific article; zbMATH DE number 3930339
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• scientific article; zbMATH DE number 794239

This page was built for publication: First-order formative rules

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