## Leo Bachmair

*Proceedings of the 11th International Conference on Rewriting Techniques and Applications*

RTA, 2000.

@proceedings{RTA-2000, address = "Norwich, England, United Kingdom", editor = "Leo Bachmair", isbn = "3-540-67778-X", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the 11th International Conference on Rewriting Techniques and Applications}", volume = 1833, year = 2000, }

### Contents (20 items)

- RTA-2000-Meseguer #concept #logic #maude
- Rewriting Logic and Maude: Concepts and Applications (JM), pp. 1–26.
- RTA-2000-Tison #automaton #term rewriting
- Tree Automata and Term Rewrite Systems (ST), pp. 27–30.
- RTA-2000-BjornerM #unification
- Absolute Explicit Unification (NB, CM), pp. 31–46.
- RTA-2000-Blanqui #confluence #higher-order #term rewriting #termination
- Termination and Confluence of Higher-Order Rewrite Systems (FB), pp. 47–61.
- RTA-2000-BonelliKR #higher-order
- A de Bruijn Notation for Higher-Order Rewriting (EB, DK, AR), pp. 62–79.
- RTA-2000-ContejeanCM #physics
- Rewriting Techniques in Theoretical Physics (EC, AC, BM), pp. 80–94.
- RTA-2000-DoughertyG #normalisation #reduction
- Normal Forms and Reduction for Theories of Binary Relations (DJD, CG), pp. 95–109.
- RTA-2000-ErkN #constraints #parallel
- Parallelism Constraints (KE, JN), pp. 110–126.
- RTA-2000-Groote #higher-order #linear
- Linear Higher-Order Matching Is NP-Complete (PdG), pp. 127–140.
- RTA-2000-JoachimskiM #confluence #standard #λ-calculus
- Standardization and Confluence for a λ Calculus with Generalized Applications (FJ, RM), pp. 141–155.
- RTA-2000-LevyV #constraints #higher-order #linear #unification
- Linear Second-Order Unification and Context Unification with Tree-Regular Constraints (JL, MV), pp. 156–171.
- RTA-2000-Lohrey #confluence #problem #strict #word
- Word Problems and Confluence Problems for Restricted Semi-Thue Systems (ML), pp. 172–186.
- RTA-2000-Pichler
- The Explicit Representability of Implicit Generalizations (RP), pp. 187–202.
- RTA-2000-Statman #combinator #on the #problem #word
- On the Word Problem for Combinators (RS), pp. 203–213.
- RTA-2000-Struth #algebra
- An Algebra of Resolution (GS), pp. 214–228.
- RTA-2000-Stuber #calculus #convergence #term rewriting
- Deriving Theory Superposition Calculi from Convergent Term Rewriting Systems (JS), pp. 229–245.
- RTA-2000-TakaiKS #effectiveness #finite #linear #term rewriting
- Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability (TT, YK, HS), pp. 246–260.
- RTA-2000-Arts #dependence
- System Description: The Dependency Pair Method (TA), pp. 261–264.
- RTA-2000-Moreau #compilation
- REM (Reduce Elan Machine): Core of the New ELAN Compiler (PEM), pp. 265–269.
- RTA-2000-OhlebuschCM #analysis #logic programming #named #source code #termination
- TALP: A Tool for the Termination Analysis of Logic Programs (EO, CC, CM), pp. 270–273.

4 ×#higher-order

4 ×#term rewriting

3 ×#confluence

3 ×#linear

2 ×#constraints

2 ×#problem

2 ×#termination

2 ×#unification

2 ×#word

4 ×#term rewriting

3 ×#confluence

3 ×#linear

2 ×#constraints

2 ×#problem

2 ×#termination

2 ×#unification

2 ×#word