Conditional and Typed Rewriting Systems

1. Front Matter

   PDF

2. Conditional rewriting in focus

   • Francois Bronsard, Uday S. Reddy

   Pages 1-13

3. A maximal-literal unit strategy for horn clauses

   • Nachum Dershowitz

   Pages 14-25

4. Extended term rewriting systems

   • Jan Willem Klop, Roel de Vrijer

   Pages 26-50

5. A proof system for conditional algebraic specifications

   • Emmanuel Kounalis, Michaël Rusinowitch

   Pages 51-63

6. Conditional rewriting logic: Deduction, models and concurrency

   • José Meseguer

   Pages 64-91

7. Equivalences of rewrite programs

   • Chilukuri K. Mohan

   Pages 92-97

8. On finite representations of infinite sequences of terms

   • Hong Chen, Jieh Hsiang, Hwa-Chung Kong

   Pages 99-114

9. Infinite terms and infinite rewritings

   • Yiyun Chen, Michael J. O'Donnell

   Pages 115-126

10. Testing confluence of nonterminating rewriting systems

    • Yiyun Chen, Michael J. O'Donnell

    Pages 127-136

11. A survey of ordinal interpretations of type ɛ0 for termination of rewriting systems

    • Bernard R. Hodgson, Clement F. Kent

    Pages 137-142

12. Meta-rule synthesis from crossed rewrite systems

    • Hélène Kirchner, Miki Hermann

    Pages 143-154

13. An application of automated equational reasoning to many-valued logic

    • Siva Anantharaman, Maria Paola Bonacina

    Pages 155-161

14. Completion of first-order clauses with equality by strict superposition

    • Leo Bachmair, Harald Ganzinger

    Pages 162-180

15. Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation

    • Hubert Bertling

    Pages 181-193

16. Proof by consistency in conditional equational theories

    • Eddy Bevers, Johan Lewi

    Pages 194-205

17. Completion procedures as semidecision procedures

    • Maria Paola Bonacina, Jieh Hsiang

    Pages 206-232

18. Errata corrige

    Pages 232-232

19. Linear completion

    • Hervé Devie

    Pages 233-245

20. Clausal rewriting

    • Robert Nieuwenhuis, Fernando Orejas

    Pages 246-258

In recent years, extensions of rewriting techniques that go beyond the traditional untyped algebraic rewriting framework have been investigated and developed. Among these extensions, conditional and typed systems are particularly important, as are higher-order systems, graph rewriting systems, etc. The international CTRS (Conditional and Typed Rewriting Systems) workshops are intended to offer a forum for researchers on such extensions of rewriting techniques. This volume presents the proceedings of the second CTRS workshop, which contributed to discussion and evaluation of new directions of research. (The proceedings of the first CTRS workshop are in Lecture Notes in Computer Science, Vol. 308.) Several important directions for extensions of rewriting techniques were stressed, which are reflected in the organization of the chapters in this volume: - Theory of conditional and Horn clause systems, - Infinite terms, non-terminating systems, and termination, - Extension of Knuth-Bendix completion, - Combined systems, combined languages and modularity, - Architecture, compilers and parallel computation, - Basic frameworks for typed and order-sorted systems, - Extension of unification and narrowing techniques.

• Automated Deduction
• Automatisches Schließen
• Parallel Architecture
• Parallel Computing
• Parallele Architekturen
• Paralleles Rechnen
• Parallelverarbeitung (EDV)
• Programmiersprache
• Programming Languages
• Rechnerarchitektur
• Resolution
• Term Rewriting Systems
• logic
• programming
• semantics

Policies and ethics