Rewriting Techniques and Applications

1. An efficient representation of arithmetic for term rewriting

   • Dave Cohen, Phil Watson

   Pages 240-251

2. Query optimization using rewrite rules

   • Sieger van Denneheuvel, Karen Kwast, Gerard R. Renardel de Lavalette, Edith Spaan

   Pages 252-263

3. Boolean algebra admits no convergent term rewriting system

   • Rolf Socher-Ambrosius

   Pages 264-274

4. Decidability of confluence and termination of monadic term rewriting systems

   • Kai Salomaa

   Pages 275-286

5. Bottom-up tree pushdown automata and rewrite systems

   • J-L. Coquidé, M. Dauchet, R. Gilleron, S. Vàgvölgyi

   Pages 287-298

6. On relationship between term rewriting systems and regular tree languages

   • G. A. Kucherov

   Pages 299-311

7. The equivalence of boundary and confluent graph grammars on graph languages of bounded degree

   • Franz J. Brandenburg

   Pages 312-322

8. Left-to-right tree pattern matching

   • Albert Gräf

   Pages 323-334

9. Incremental techniques for efficient normalization of nonlinear rewrite systems

   • R. Ramesh, I. V. Ramakrishnan

   Pages 335-347

10. On fairness of completion-based theorem proving strategies

    • Maria Paola Bonacina, Jieh Hsiang

    Pages 348-360

11. Proving equational and inductive theorems by completion and embedding techniques

    • J. Avenhaus

    Pages 361-373

12. Divergence phenomena during completion

    • Andrea Sattler-Klein

    Pages 374-385

13. Simulating Buchberger's algorithm by Knuth-Bendix completion

    • Reinhard Bündgen

    Pages 386-397

14. On proving properties of completion strategies

    • Miki Hermann

    Pages 398-410

15. On ground AC-completion

    • Claude Marché

    Pages 411-422

16. Any ground associative-commutative theory has a finite canonical system

    • Paliath Narendran, Michaël Rusinowitch

    Pages 423-434

17. A narrowing-based theorem prover

    • Ulrich Fraus, Heinrich Hußmann

    Pages 435-436

18. ANIGRAF: An interactive system for the animation of graph rewriting systems with priorities

    • Michel Billaud

    Pages 437-438

19. Emmy: A refutational theorem prover for first-order logic with equations

    • Aline Deruyver

    Pages 439-441

20. The tecton proof system

    • Raj Agarwal, David R. Musser, Deepak Kapur, Xumin Nie

    Pages 442-444

This volume contains the proceedings of the Fourth International Conference on Rewriting Techniques and Applications (RTA-91), held in Como, Italy, April 10-12, 1991. The volume includes 40 papers on a wide variety of topics including: term rewriting systems, equational unification, algebraic rewriting, termination proofs, generalization problems, undecidable properties, parametrized specifications, normalizing systems, program transformation, query optimization, tree languages, graph languages, theorem proving systems, completion, graph rewriting systems, and open problems.

• Automatisches Schließen
• Beweissysteme
• Programmiersprache
• Rechnergestützte Entscheidung
• Term rewriting systems
• Verifikation
• optimization
• proving
• reasoning
• term rewriting
• theorem proving
• theorem proving systems
• verification
• algorithm analysis and problem complexity

Policies and ethics