Contents of the Proceedings of the
2nd International Workshop on Conditional Term Rewriting Systems.
Montreal, Canada, June 11-14, 1990.
Lecture Notes in Computer Science, Vol. 516, Springer Verlag.

Editors: Stéphane Kaplan and Mitsuhiro Okada.

• F. Bronsard and U. S. Reddy, Conditional Rewriting in Focus (pages 2-13).
• N. Dershowitz, A Maximal-Literal Unit Strategy for Horn Clauses (pages 14-25).
• J. W. Klop and R. de Vrijer, Extended Term Rewriting Systems (invited paper) (pages 26-50).
• E. Kounalis and M. Rusinowitch, A Proof System for Conditional Algebraic Specifications (pages 51-63).
• J. Meseguer, Conditional Rewriting Logic: Deduction, Models and Concurrency (invited paper) (pages 64-91).
• C. K. Mohan, Equivalences of Rewrite Programs (pages 92-99).
• H. Chen, J. Hsiang and H.-C. Kong, On Finite Representations of Infinite Sequences of Terms (pages 100-114).
• Y. Chen and M. J. O'Donnell, Infinite Terms and Infinite Rewritings (pages 115-126).
• Y. Chen and M. J. O'Donnell, Testing Confluence of Nonterminating Rewriting Systems (pages 127-136).
• B. R. Hodgson and C. F. Kent, A Survey of Ordinal Interpretations of Type \epsilon_0 for Termination of Rewriting Systems (pages 137-142).
• H. Kirchner and M. Hermann, Meta-rule Synthesis from Crossed Rewrite Systems (pages 143-155).
• S. Anantharaman and M. P. Bonacina, An Application of Automated Equational Reasoning to Many-Valued Logic (pages 156-161).
• L. Bachmair and H. Ganzinger, Completion of First-Order Clauses with Equality by Strict Superposition (invited paper) (pages 162-180).
• H. Bertling, Knuth-Bendix Completion of Horn Clause Programs for Restricted Linear Resolution and Paramodulation (pages 181-193).
• E. Bevers and J. Lewi, Proof by Consistency in Conditional Equational Theories (pages 194-205).
• M. P. Bonacina and J. Hsiang, Completion Procedures as Semi-Decision Procedures (invited paper) (pages 206-232).
• H. Devie, Linear Completion (pages 233-245).
• R. Nieuwenhuis and F. Orejas, Clausal Rewriting (pages 246-261).
• F. Barbanera, Adding Algebraic Rewriting to the Calculus of Constructions: Strong Normalization Preserved (pages 262-271).
• W. Bousdira and J.-L. Rémy, On Sufficient Completeness of Conditional Specifications (pages 272-286).
• N. Lichtenstein and S. Kaplan, FPL: Functional Plus Logic Programming. An Integration of the FP and Prolog Languages (pages 287-294).
• A. Middeldorp, Confluence of the Disjoint Union of Conditional Term Rewriting Systems (pages 295-306).
• D. Plump, Implementing Term Rewriting by Graph Reduction: Termination of Combined Systems (pages 307-319).
• H. Aida, J. Goguen and J. Meseguer, Compiling Concurrent Rewriting onto the Rewrite Rule Machine (pages 320-332).
• S. Antoy, Design Strategies for Rewrite Rules (pages 333-341).
• L. Galbiati and C. Talcott, A Simplifier for Untyped Lambda Expressions (pages 342-353).
• M. C. J. D. van Eekelen, M. J. Plasmeijer and J. E. W. Smetsers, Parallel Graph Rewriting on Loosely Coupled Machine Architectures (pages 354-371).
• R. M. Amadio, Typed Equivalence, Type Assignment and Type Containment (pages 372-382).
• M. Emele and R. Zajac, A Fixed-Point Semantics for Feature Type Systems (pages 383-388).
• J. G. Stell, Unique-Sort Order-Sorted Theories: A Description as Monad Morphisms (pages 389-400).
• Y. Sun, Equational Logics (Birkhoff's Method Revisited) (pages 401-406).
• U. Waldmann, Compatibility of Order-Sorted Rewrite Rules (pages 407-417).
• G. Aguzzi, U. Modigliani and M. C. Verri, A Universal Termination Condition for Solving Goals in Equational Languages (pages 418-423).
• J. Darlington and Y. Guo, Constrained Equational Deduction (pages 424-435).
• T. Nipkow, Higher-Order Unification, Polymorphism, and Subsorts (pages 436-447).
• Z. Qian, Second-Order Unification in the Presence of Linear Shallow Algebraic Equations (pages 448-453).
• W. Snyder and C. Lynch, An Inference System for Horn Clause Logic with Equality: A Foundation for Conditional E-Unification and for Logic Programming in the Presence of Equality (pages 454-461).