Confluent and coherent equational term rewriting systems application to proofs in abstract data types
- 1 January 1983
- book chapter
- Published by Springer Nature
- p. 269-283
- https://doi.org/10.1007/3-540-12727-5_16
Abstract
No abstract availableKeywords
This publication has 12 references indexed in Scilit:
- Computer experiments with the REVE term rewriting system generatorPublished by Association for Computing Machinery (ACM) ,1983
- Orderings for term-rewriting systemsTheoretical Computer Science, 1982
- Proofs by induction in equational theories with constructorsJournal of Computer and System Sciences, 1982
- A complete proof of correctness of the Knuth-Bendix completion algorithmJournal of Computer and System Sciences, 1981
- Complete Sets of Reductions for Some Equational TheoriesJournal of the ACM, 1981
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- Canonical Forms and Unification.Published by Defense Technical Information Center (DTIC) ,1980
- On proving inductive properties of abstract data typesPublished by Association for Computing Machinery (ACM) ,1980
- How to prove algebraic inductive hypotheses without inductionPublished by Springer Nature ,1980
- Deciding unique termination of permutative rewriting systems: Choose your term algebra carefullyPublished by Springer Nature ,1980