## Tobias Nipkow

*Proceedings of the Ninth International Conference on Rewriting Techniques and Applications*

RTA, 1998.

@proceedings{RTA-1998, address = "Tsukuba, Japan", editor = "Tobias Nipkow", isbn = "3-540-64301-X", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the Ninth International Conference on Rewriting Techniques and Applications}", volume = 1379, year = 1998, }

### Contents (25 items)

- RTA-1998-Klop #term rewriting
- Origin Tracking in Term Rewriting (JWK), p. 1.
- RTA-1998-Okui
- Simultaneous Critical Pairs and Church-Rosser Property (SO), pp. 2–16.
- RTA-1998-Ohlebusch #equivalence #reduction #theorem
- Church-Rosser Theorems for Abstract Reduction Modulo an Equivalence Relation (EO), pp. 17–31.
- RTA-1998-OttoSM #automation #convergence #finite #monad
- Automatic Monoids Versus Monoids with Finite Convergent Presentations (FO, ASK, KM), pp. 32–46.
- RTA-1998-Levy #decidability #higher-order #problem #unification
- Decidable and Undecidable Second-Order Unification Problems (JL), pp. 47–60.
- RTA-1998-Schmidt-SchaussS #equation #on the
- On the Exponent of Periodicity of Minimal Solutions of Context Equation (MSS, KUS), pp. 61–75.
- RTA-1998-JacquemardMW #equation #unification
- Unification in Extension of Shallow Equational Theories (FJ, CM, CW), pp. 76–90.
- RTA-1998-GuoNS #algebra #process #unification
- Unification and Matching in Process Algebras (QG, PN, SKS), pp. 91–105.
- RTA-1998-Schmidt
*E*-Unification for Subsystems of*S4*(RAS), pp. 106–120.- RTA-1998-LimetR #equation #term rewriting
- Solving Disequations Modulo Some Class of Rewrite Systems (SL, PR), pp. 121–135.
- RTA-1998-Comon #consistency #proving
- About Proofs by Consistency (HC), pp. 136–137.
- RTA-1998-Waldmann #decidability #normalisation
- Normalization of S-Terms is Decidable (JW), pp. 138–150.
- RTA-1998-Genet #approximate #decidability #normalisation #set
- Decidable Approximations of Sets of Descendants and Sets of Normal Forms (TG), pp. 151–165.
- RTA-1998-VermaRL #algorithm #problem #reduction
- Algorithms and Reductions for Rewriting Problems (RMV, MR, DL), pp. 166–180.
- RTA-1998-DegtyarevGNVV #decidability
- The Decidability of Simultaneous Rigid
*E*-Unification with One Variable (AD, YG, PN, MV, AV), pp. 181–195. - RTA-1998-MullerN #constraints #higher-order #logic #monad
- Ordering Constraints over Feature Trees Expressed in Second-Order Monadic Logic (MM, JN), pp. 196–210.
- RTA-1998-CharatonikP #constraints #set
- Co-definite Set Constraints (WC, AP), pp. 211–225.
- RTA-1998-ArtsG #composition #dependence #termination #using
- Modularity of Termination Using Dependency pairs (TA, JG), pp. 226–240.
- RTA-1998-MarcheU #commutative #dependence #termination
- Termination of Associative-Commutative Rewriting by Dependency Pairs (CM, XU), pp. 241–255.
- RTA-1998-AotoT #termination
- Termination Transformation by Tree Lifting Ordering (TA, YT), pp. 256–270.
- RTA-1998-Xi #automation #proving #termination #towards
- Towards Automated Termination Proofs through “Freezing” (HX), pp. 271–285.
- RTA-1998-DanvyR #higher-order #partial evaluation
- Higher-Order Rewriting and Partial Evaluation (OD, KHR), pp. 286–301.
- RTA-1998-Akama #algebra #combinator
- SN Combinators and Partial Combinatory Algebras (YA), pp. 302–316.
- RTA-1998-Fuchs #information management #proving
- Coupling Saturation-Based Provers by Exchanging Positive/Negative Information (DF), pp. 317–331.
- RTA-1998-DershowitzT #database #online #problem
- An On-line Problem Database (ND, RT), pp. 332–342.

4 ×#decidability

4 ×#termination

3 ×#equation

3 ×#higher-order

3 ×#problem

3 ×#proving

3 ×#unification

2 ×#algebra

2 ×#automation

2 ×#constraints

4 ×#termination

3 ×#equation

3 ×#higher-order

3 ×#problem

3 ×#proving

3 ×#unification

2 ×#algebra

2 ×#automation

2 ×#constraints