First-Order Formative Rules
Logic in Computer Science
2014-05-01 v1
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.
Cite
@article{arxiv.1404.7695,
title = {First-Order Formative Rules},
author = {Carsten Fuhs and Cynthia Kop},
journal= {arXiv preprint arXiv:1404.7695},
year = {2014}
}
Comments
Extended version of a paper which is to appear in the proceedings of RTA-TLCA 2014 (Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications)