@InProceedings{Kapur-RTA96,
author={Kapur, D.},
title={{Rewrite-Based Automated Reasoning: Challenges Ahead (invited lecture)}},
pages={1--2},
crossref={RTA96}
}

@InProceedings{KirchnerLS-RTA96,
author={Kirchner, C. and Lynch, C. and Scharff, C.},
title={{Fine-Grained Concurrent Completion}},
pages={3--17},
crossref={RTA96}
}

@InProceedings{BoudetCM-RTA96,
author={Boudet, A. and Contejean, E. and March{\'e}, C.},
title={{AC-Complete Unification and its Application to Theorem Proving}},
pages={18--32},
crossref={RTA96}
}

@InProceedings{Stuber-RTA96,
author={Stuber, J.},
title={{Superposition Theorem Proving for Albelian Groups Represented as Integer Modules}},
pages={33--47},
crossref={RTA96}
}

@InProceedings{Goebel-RTA96,
author={G{\"o}bel, M.},
title={{Symideal Gr\"obner Bases}},
pages={48--62},
crossref={RTA96}
}

@InProceedings{ArtsG-RTA96,
author={Arts, T. and Giesl, J.},
title={{Termination of Constructor Systems}},
pages={63--77},
crossref={RTA96}
}

@InProceedings{Ferreira-RTA96,
author={Ferreira, M. C. F.},
title={{Dummy Elimination in Equational Rewriting}},
pages={78--92},
crossref={RTA96}
}

@InProceedings{Gramlich-RTA96,
author={Gramlich, B.},
title={{On Proving Termination by Innermost Termination}},
pages={93--107},
crossref={RTA96}
}

@InProceedings{JouannaudR-RTA96,
author={Jouannaud, J.-P. and Rubio, A.},
title={{A Recursive Path Ordering for Higher-Order Terms in eta-Long beta-Normal Form}},
pages={108--122},
crossref={RTA96}
}

@InProceedings{Virga-RTA96,
author={Virga, R.},
title={{Higher-Order Superposition for Dependent Types}},
pages={123--137},
crossref={RTA96}
}

@InProceedings{HanusP-RTA96,
author={Hanus, M. and Prehofer, C.},
title={{Higher-Order Narrowing with Definitional Trees}},
pages={138--152},
crossref={RTA96}
}

@InProceedings{Huet-RTA96,
author={Huet, G. P.},
title={{Design Proof Assistant (invited lecture)}},
pages={153},
crossref={RTA96}
}

@InProceedings{Vittek-RTA96,
author={Vittek, M.},
title={{A Compiler for Nondeterministic Term Rewriting Systems}},
pages={154--167},
crossref={RTA96}
}

@InProceedings{BlooR-RTA96,
author={Bloo, R. and Rose, K. H.},
title={{Combinatory Reduction Systems with Explicit Substitution that Preserve Strong Nomalisation}},
pages={169--183},
crossref={RTA96}
}

@InProceedings{Kesner-RTA96,
author={Kesner, D.},
title={{Confluence Properties of Extensional and Non-Extensional lambda-Calculi with Explicit Substitutions (Extended Abstract)}},
pages={184--199},
crossref={RTA96}
}

@InProceedings{DiCosmo-RTA96,
author={Di Cosmo, R.},
title={{On the Power of Simple Diagrams}},
pages={200--214},
crossref={RTA96}
}

@InProceedings{GuerriniMM-RTA96,
author={Guerrini, S. and Martini, S. and Masini, A.},
title={{Coherence for Sharing Proof Nets}},
pages={215--229},
crossref={RTA96}
}

@InProceedings{KrishnaRao-RTA96,
author={Krishna Rao, M. R. K.},
title={{Modularity of Termination in Term Graph Rewriting}},
pages={230--244},
crossref={RTA96}
}

@InProceedings{GramlichW-RTA96,
author={Gramlich, B. and Wirth, C.-P.},
title={{Confluence of Terminating Conditional Rewrite Systems Revisited}},
pages={245--259},
crossref={RTA96}
}

@InProceedings{Madlener-RTA96,
author={Madlener, K.},
title={{Applications of Rewrite Techniques in Monoids and Rings (invited lecture)}},
pages={260},
crossref={RTA96}
}

@InProceedings{Lueth-RTA96,
author={L{\"u}th, C.},
title={{Compositional Term Rewriting: An Algebraic Proof of Toyama's Theorem}},
pages={261--275},
crossref={RTA96}
}

@InProceedings{Treinen-RTA96,
author={Treinen, R.},
title={{The First-Order Theory of One-Step Rewriting is Undecidable}},
pages={276--286},
crossref={RTA96}
}

@InProceedings{SchmidtSchauss-RTA96,
author={Schmidt-Schau\ss, M.},
title={{An Algorithm for Distributive Unification}},
pages={287--301},
crossref={RTA96}
}

@InProceedings{Senizergues-RTA96,
author={S{\'e}nizergues, G.},
title={{On the Termination Problem for One-Rule Semi-Thue System}},
pages={302--316},
crossref={RTA96}
}

@InProceedings{CurienQS-RTA96,
author={Curien, R. and Qian, Z. and Shi, H.},
title={{Efficient Second-Order Matching}},
pages={317--331},
crossref={RTA96}
}

@InProceedings{Levy-RTA96,
author={Levy, J.},
title={{Linear Second-Order Unification}},
pages={332--346},
crossref={RTA96}
}

@InProceedings{FettigL-RTA96,
author={Fettig, R. and L{\"o}chner, B.},
title={{Unification of Higher-Order patterns in a Simply Typed Lambda-Calculus with Finite Products and terminal Type}},
pages={347--361},
crossref={RTA96}
}

@InProceedings{Jacquemard-RTA96,
author={Jacquemard, F.},
title={{Decidable Approximations of Term Rewriting Systems}},
pages={362--376},
crossref={RTA96}
}

@InProceedings{SakaiT-RTA96,
author={Sakai, M. and Toyama, Y.},
title={{Semantics and Strong Sequentiality of Priority Term Rewriting Systems}},
pages={377--391},
crossref={RTA96}
}

@InProceedings{vanOostrom-RTA96,
author={van Oostrom, V.},
title={{Higher-Order Families}},
pages={392--407},
crossref={RTA96}
}

@InProceedings{Voisin-RTA96,
author={Voisin, F.},
title={{A New Proof Manager and Graphic Interface for Larch Prover (system description)}},
pages={408--411},
crossref={RTA96}
}

@InProceedings{BuendgenSW-RTA96,
author={B{\"u}ndgen, R. and Sinz, C. and Walter, J.},
title={{ReDuX 1.5: New Facets of Rewriting (system description)}},
pages={412--415},
crossref={RTA96}
}

@InProceedings{ContejeanM-RTA96,
author={Contejean, E. and March{\'e}, C.},
title={{CiME: Completion Modulo E (system description)}},
pages={416--419},
crossref={RTA96}
}

@InProceedings{VandevoordeK-RTA96,
author={Vandevoorde, M. T. and Kapur, D.},
title={{Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite-Rule Based Prover (system description)}},
pages={420--423},
crossref={RTA96}
}

@InProceedings{WaltersK-RTA96,
author={Walters, H. R. and Kamperman, J. F. Th.},
title={{EPIC: An Equational Language -Abstract Machine Supporting Tools- (system description)}},
pages={424--427},
crossref={RTA96}
}

@InProceedings{BerregebBR-RTA96,
author={Berregeb, N. and Bouhoula, A. and Rusinowitch, M.},
title={{SPIKE-AC: A System for Proofs by Induction in Associative-Commutative Theories (system description)}},
pages={428--431},
crossref={RTA96}
}

@InProceedings{HillenbrandBF-RTA96,
author={Hillenbrand, T. and Buch, A. and Fettig, R.},
title={{On Gaining Efficiency in Completion-Based Theorem Proving (system description)}},
pages={432--435},
crossref={RTA96}
}


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

@Proceedings{RTA96,
year={1996},
month=jul # {~27--30,},
editor={Ganzinger, Harald},
title={{Rewriting Techniques and Applications, 7th International Conference, RTA-96}},
booktitle={{Rewriting Techniques and Applications, 7th International Conference, RTA-96}},
address={New Brunswick, NJ, USA},
series={LNCS 1103},
publisher={Springer-Verlag}
}