Fuhs, C;
Kop, C;
(2014)
First-Order Formative Rules.
In: Dowek, G, (ed.)
Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings.
(pp. 240 - 256).
Springer International Publishing: Switzerland.
![[thumbnail of RTATLCA14-formative.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
RTATLCA14-formative.pdf Available under License : See the attached licence file. Download (454kB) |
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.
| Type: | Proceedings paper |
|---|---|
| Title: | First-Order Formative Rules |
| Event: | Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014 |
| ISBN-13: | 9783319089171 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-319-08918-8_17 |
| Publisher version: | http://dx.doi.org/10.1007/978-3-319-08918-8_17 |
| Language: | English |
| Additional information: | This is the authors' accepted version of this published paper. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-08918-8_17 |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1455005 |
Archive Staff Only
 |
View Item |
