Claude Kirchner
Proceedings of the Fifth International Conference on Rewriting Techniques and Applications
RTA, 1993.

@proceedings{RTA-1993,
	address       = "Montreal, Canada",
	editor        = "Claude Kirchner",
	isbn          = "3-540-56868-9",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fifth International Conference on Rewriting Techniques and Applications}",
	volume        = 690,
	year          = 1993,
}

Contents (39 items)

5 ×#equation
5 ×#problem
5 ×#term rewriting
5 ×#termination
4 ×#named
4 ×#order
3 ×#constraints
3 ×#proving
2 ×#algebra
2 ×#algorithm

RTA-1993-Bachmair #proving #theorem proving

Rewrite Techniques in Theorem Proving (LB), p. 1.

RTA-1993-LynchS

Redundancy Criteria for Constrained Completion (CL, WS), pp. 2–16.

RTA-1993-LevyA #order #term rewriting

Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations (JL, JAC), pp. 17–31.

RTA-1993-Zhang #case study

A Case Study of Completion Modulo Distributivity and Abelian Groups (HZ), pp. 32–46.

RTA-1993-Werner #approach #order #semantics

A Semantic Approach to Order-Sorted Rewriting (AW), pp. 47–61.

RTA-1993-AvenhausD #equation #proving #theorem proving

Distributing Equational Theorem Proving (JA, JD), pp. 62–76.

RTA-1993-ChakrabartiY #algorithm #correctness #distributed #memory management #on the

On the Correctness of a Distributed Memory Gröbner basis Algorithm (SC, KAY), pp. 77–91.

RTA-1993-Moser

Improving Transformation Systems for General E-Unification (MM), pp. 92–105.

RTA-1993-NiehrenPT #constraints #equation #finite

Equational and Membership Constraints for Finite Trees (JN, AP, RT), pp. 106–120.

RTA-1993-Backofen #logic

Regular Path Expression in Feature Logic (RB), pp. 121–135.

RTA-1993-Gallier #proving

Proving Properties of Typed λ Terms: Realizability, Covers, and Sheaves (JHG), p. 136.

RTA-1993-Dougherty #λ-calculus

Some λ Calculi with Categorial Sums and Products (DJD), pp. 137–151.

RTA-1993-AspertiL #λ-calculus

Paths, Computations and Labels in the λ-Calculus (AA, CL), pp. 152–167.

RTA-1993-Raamsdonk #confluence

Confluence and Superdevelopments (FvR), pp. 168–182.

RTA-1993-Ariola #graph #modelling #term rewriting

Relating Graph and Term Rewriting via Böhm Models (ZMA), pp. 183–197.

RTA-1993-DershowitzH #termination #topic

Topics in Termination (ND, CH), pp. 198–212.

RTA-1993-FerreiraZ #term rewriting #termination

Total Termination of Term Rewriting (MCFF, HZ), pp. 213–227.

RTA-1993-MiddeldorpG #termination

Simple Termination is Difficult (AM, BG), pp. 228–242.

RTA-1993-Khasidashvili #normalisation #orthogonal #term rewriting

Optimal Normalization in Orthogonal Term Rewriting Systems (ZK), pp. 243–258.

RTA-1993-Field #approach #graph #incremental #reduction #term rewriting

A Graph Reduction Approach to Incremental Term Rewriting (JF), pp. 259–273.

RTA-1993-Lippe #bottom-up #generative

Generating Tables for Bottom-Up Matching (EL), pp. 274–288.

RTA-1993-Adian #algorithm #monad #on the #problem

On some Algorithmic Problems for Groups and Monoids (SIA), pp. 289–300.

RTA-1993-BaaderS #problem

Combination Techniques and Decision Problems for Disunification (FB, KUS), pp. 301–315.

RTA-1993-Tajine #decidability #equation

The Negation Elimination from Syntactic Equational Formula is Decidable (MT), pp. 316–327.

RTA-1993-CaronCD #automaton #constraints

Encompassment Properties and Automata with Constraints (ACC, JLC, MD), pp. 328–342.

RTA-1993-Raoult #recursion

Recursively Defined Tree Transductions (JCR), pp. 343–357.

RTA-1993-Fernandez #problem #satisfiability

AC Complement Problems: Satisfiability and Negation Elimination (MF), pp. 358–373.

RTA-1993-RubioN #order

A Precedence-Based Total AC-Compatible Ordering (AR, RN), pp. 374–388.

RTA-1993-DelorP #commutative #order

Extension of the Associative Path Ordering to a Chain of Associative Commutative Symbols (CD, LP), pp. 389–404.

RTA-1993-Plaisted #constraints #polynomial #termination #testing

Polynomial Time Termination and Constraint Satisfaction Tests (DAP), pp. 405–420.

RTA-1993-Martin #linear

Linear Interpretations by Counting Patterns (UM), pp. 421–433.

RTA-1993-Senizergues #decidability #problem #termination

Some Undecidable Termination Problems for Semi-Thue Systems (GS), p. 434.

RTA-1993-NivelaN #first-order

Saturation of First-Order (Constrained) Clauses with the Saturate System (PN, RN), pp. 436–440.

RTA-1993-Matthews #equation #ml #named #reasoning #standard

MERILL: An Equational Reasoning System in Standard ML (BM), pp. 441–445.

RTA-1993-Bundgen

Reduce the Redex → ReDuX (RB), pp. 446–450.

RTA-1993-LoweB #algebra #graph grammar #implementation #named

AGG — An Implementation of Algebraic Graph Rewriting (ML, MB), pp. 451–456.

RTA-1993-Verma #equation #named

Smaran: A Congruence-Closure Based System for Equational Computations (RMV), pp. 457–461.

RTA-1993-GuiO #algebra #higher-order #named #specification

LAMBDALG: Higher Order Algebraic Specification Language (YG, MO), pp. 462–466.

RTA-1993-DershowitzJK #problem

More Problems in Rewriting (ND, JPJ, JWK), pp. 468–487.