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. © 2014 Springer International Publishing Switzerland.
Cite
CITATION STYLE
Fuhs, C., & Kop, C. (2014). First-order formative rules. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8560 LNCS, pp. 240–256). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_17
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
