@InProceedings{KennawayKSV-RTA91,
author={Kennaway, R. and Klop, J. W. and Sleep, M. R. and de Vries, F.-J.},
title={{Transfinite Reductions in Orthogonal Term Rewriting Systems (Extended Abstract)}},
pages={1--12},
crossref={RTA91}
}

@InProceedings{FarmerW-RTA91,
author={Farmer, W. M. and Watro, R. J.},
title={{Redex Capturing in Term Graph Rewriting (Concise Version)}},
pages={13--24},
crossref={RTA91}
}

@InProceedings{Wolfram-RTA91,
author={Wolfram, D. A.},
title={{Rewriting, and Equational Unification: the Higher-Order Cases}},
pages={25--36},
crossref={RTA91}
}

@InProceedings{Dougherty-RTA91,
author={Dougherty, D. J.},
title={{Adding Algebraic Rewriting to the Untyped Lambda Calculus (Extended Abstract)}},
pages={37--48},
crossref={RTA91}
}

@InProceedings{DrewesL-RTA91,
author={Drewes, F. and Lautemann, C.},
title={{Incremental Termination Proofs and the Length of Derivations}},
pages={49--61},
crossref={RTA91}
}

@InProceedings{Hofbauer-RTA91,
author={Hofbauer, D.},
title={{Time Bounded Rewrite Systems and Termination Proofs by Generalized Embedding}},
pages={62--73},
crossref={RTA91}
}

@InProceedings{KrischerB-RTA91,
author={Krischer, S. and Bockmayr, A.},
title={{Detecting Redundant Narrowing Derivations by the LSE-SL Reducability Test}},
pages={74--85},
crossref={RTA91}
}

@InProceedings{Baader-RTA91,
author={Baader, F.},
title={{Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems}},
pages={86--97},
crossref={RTA91}
}

@InProceedings{Domenjoud-RTA91,
author={Domenjoud, E.},
title={{AC Unification Through Order-Sorted AC1 Unification}},
pages={98--111},
crossref={RTA91}
}

@InProceedings{ChabinR-RTA91,
author={Chabin, J. and R{\'e}ty, P.},
title={{Narrowing Directed by a Graph of Terms}},
pages={112--123},
crossref={RTA91}
}

@InProceedings{BaaderN-RTA91,
author={Baader, F. and Nutt, W.},
title={{Adding Homomorphisms to Commutative/Monoidal Theories or How Algebra Can Help in Equational Unification}},
pages={124--135},
crossref={RTA91}
}

@InProceedings{Klay-RTA91,
author={Klay, F.},
title={{Undecidable Properties of Syntactic Theories}},
pages={136--149},
crossref={RTA91}
}

@InProceedings{SnyderL-RTA91,
author={Snyder, W. and Lynch, C.},
title={{Goal Directed Strategies for Paramodulation}},
pages={150--161},
crossref={RTA91}
}

@InProceedings{Pottier-RTA91,
author={Pottier, L.},
title={{Minimal Solutions of Linear Diophantine Systems: Bounds and Algorithms}},
pages={162--173},
crossref={RTA91}
}

@InProceedings{Kirchner-RTA91,
author={Kirchner, H.},
title={{Proofs in Parameterized Specification}},
pages={174--187},
crossref={RTA91}
}

@InProceedings{MiddeldorpT-RTA91,
author={Middeldorp, A. and Toyama, Y.},
title={{Completeness of Combinations of Constructor Systems}},
pages={188--199},
crossref={RTA91}
}

@InProceedings{NipkowQ-RTA91,
author={Nipkow, T. and Qian, Z.},
title={{Modular Higher-Order E-Unification}},
pages={200--214},
crossref={RTA91}
}

@InProceedings{CurienG-RTA91,
author={Curien, P.-L. and Ghelli, G.},
title={{On Confluence for Weakly Normalizing Systems}},
pages={215--225},
crossref={RTA91}
}

@InProceedings{Bellegarde-RTA91,
author={Bellegarde, F.},
title={{Program Transformation and Rewriting}},
pages={226--239},
crossref={RTA91}
}

@InProceedings{CohenW-RTA91,
author={Cohen, D. and Watson, P.},
title={{An Efficient Representation of Arithmetic for Term Rewriting}},
pages={240--251},
crossref={RTA91}
}

@InProceedings{vanDenneheuvelKRS-RTA91,
author={van Denneheuvel, S. and Kwast, K. L. and Renardel de Lavalette, G. R. and Spaan, E.},
title={{Query Optimization Using Rewrite Rules}},
pages={252--263},
crossref={RTA91}
}

@InProceedings{Socher-Ambrosius-RTA91,
author={Socher-Ambrosius, R.},
title={{Boolean Algebra Admits No Convergent Term Rewriting System}},
pages={264--274},
crossref={RTA91}
}

@InProceedings{Salomaa-RTA91,
author={Salomaa, K.},
title={{Decidability of Confluence and Termination of Monadic Term Rewriting Systems}},
pages={275--286},
crossref={RTA91}
}

@InProceedings{CoquideDGV-RTA91,
author={Coquid{\'e}, J.-L. and Dauchet, M. and Gilleron, R. and V{\'a}gv{\"o}lgyi S.},
title={{Bottom-Up Tree Pushdown Automata and Rewrite Systems}},
pages={287--298},
crossref={RTA91}
}

@InProceedings{Kucherov-RTA91,
author={Kucherov, G. A.},
title={{On Relationship Between Term Rewriting Systems and Regular Tree Languages}},
pages={299--311},
crossref={RTA91}
}

@InProceedings{Brandenburg-RTA91,
author={Brandenburg, F.-J.},
title={{The Equivalence of Boundary and Confluent Graph Grammars on Graph Languages of Bounded Degree}},
pages={312--322},
crossref={RTA91}
}

@InProceedings{Graef-RTA91,
author={Gr{\"a}f, A.},
title={{Left-to-Right Tree Pattern Matching}},
pages={323--334},
crossref={RTA91}
}

@InProceedings{RameshR-RTA91,
author={Ramesh, R. and Ramakrishnan, I. V.},
title={{Incremental Techniques for Efficient Normalization of Nonlinear Rewrite Systems}},
pages={335--347},
crossref={RTA91}
}

@InProceedings{BonacinaH-RTA91,
author={Bonacina, M. P. and Hsiang, J.},
title={{On Fairness of Completion-Based Theorem Proving Strategies}},
pages={348--360},
crossref={RTA91}
}

@InProceedings{Avenhaus-RTA91,
author={Avenhaus, J.},
title={{Proving Equational and Inductive Theorems by Completion and Embedding Techniques}},
pages={361--373},
crossref={RTA91}
}

@InProceedings{Sattler-Klein-RTA91,
author={Sattler-Klein, A.},
title={{Divergence Phenomena during Completion}},
pages={374--385},
crossref={RTA91}
}

@InProceedings{Buendgen-RTA91,
author={B{\"u}ndgen, R.},
title={{Simulation Buchberger's Algorithm by Knuth-Bendix Completion}},
pages={386--397},
crossref={RTA91}
}

@InProceedings{Hermann-RTA91,
author={Hermann, M.},
title={{On Proving Properties of Completion Strategies}},
pages={398--410},
crossref={RTA91}
}

@InProceedings{Marche-RTA91,
author={March{\'e}, C.},
title={{On Ground AC-Completion}},
pages={411--422},
crossref={RTA91}
}

@InProceedings{NarendranR-RTA91,
author={Narendran, P. and Rusinowitch, M.},
title={{Any Gound Associative-Commutative Theory Has a Finite Canonical System}},
pages={423--434},
crossref={RTA91}
}

@InProceedings{Fraus-RTA91,
author={Fraus, U.},
title={{A Narrowing-Based Theorem Prover (system description)}},
pages={435--436},
crossref={RTA91}
}

@InProceedings{Billaud-RTA91,
author={Billaud, M.},
title={{ANIGRAF: An Interactive System for the Animation of Graph Rewriting Systems with Priorities (system description)}},
pages={437--438},
crossref={RTA91}
}

@InProceedings{Deruyver-RTA91,
author={Deruyver, A.},
title={{EMMY: A Refutational Theorem Prover for First-Order Logic with Equation (system description)}},
pages={439--441},
crossref={RTA91}
}

@InProceedings{AgarwalMKN-RTA91,
author={Agarwal, R. and Musser, D. R. and Kapur, D. and Nie, X.},
title={{The Tecton Proof System (system description)}},
pages={442--444},
crossref={RTA91}
}

@InProceedings{DershowitzJK-RTA91,
author={Dershowitz, N. and Jouannaud, J.-P. and Klop, J. W.},
title={{Open Problems in Rewriting}},
pages={445--456},
crossref={RTA91}
}


% CROSSREFERENCES
% These must remain at the end of this file.

@Proceedings{RTA91,
year={1991},
month=apr # {~10--12,},
editor={Book, Ronald V.},
title={{Rewriting Techniques and Applications, 4th International Conference, RTA-91}},
booktitle={{Rewriting Techniques and Applications, 4th International Conference, RTA-91}},
address={Como, Italy},
series={LNCS 488},
publisher={Springer-Verlag}
}