First-Order Formative Rules
Authors: Carsten Fuhs and Cynthia Kop
Paper Information
| Title: | First-Order Formative Rules |
| Authors: | Carsten Fuhs and Cynthia Kop |
| Proceedings: | RTA-TLCA 2014 LNCS Proceedings |
| Editor: | Gilles Dowek |
| Keywords: | termination analysis, usable rules, first-order term rewriting, higher-order term rewriting |
| Abstract: | ABSTRACT. This paper discusses the method of formative rules for first-order rewriting, which was previously defined for a class of higher-order rewriting. Dual to the well-known notion of usable rules, this technique allows for further simplifications of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, we can obtain significant improvements in the first-order setting, with or without types. |
| Pages: | 15 |
| Talk: | Jul 15 11:45 |
| Paper: |  |