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)

4 ×#decidability
4 ×#termination
3 ×#equation
3 ×#higher-order
3 ×#problem
3 ×#proving
3 ×#unification
2 ×#algebra
2 ×#automation
2 ×#constraints

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.