Ronald V. Book
Proceedings of the Fourth International Conference on Rewriting Techniques and Applications
RTA, 1991.

@proceedings{RTA-1991,
	address       = "Como, Italy",
	editor        = "Ronald V. Book",
	isbn          = "3-540-53904-2",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fourth International Conference on Rewriting Techniques and Applications}",
	volume        = 488,
	year          = 1991,
}

Contents (40 items)

9 ×#proving
9 ×#term rewriting
5 ×#on the
4 ×#bound
4 ×#equation
4 ×#unification
3 ×#algebra
3 ×#confluence
3 ×#graph grammar
3 ×#termination

RTA-1991-KennawayKSV #orthogonal #reduction #term rewriting

Transfinite Reductions in Orthogonal Term Rewriting Systems (RK, JWK, MRS, FJdV), pp. 1–12.

RTA-1991-FarmerW #graph grammar

Redex Capturing in Term Graph Rewriting (WMF, RJW), pp. 13–24.

RTA-1991-Wolfram #equation #higher-order #unification

Rewriting, and Equational Unification: the Higher-Order Cases (DAW), pp. 25–36.

RTA-1991-Dougherty #algebra #λ-calculus

Adding Algebraic Rewriting to the Untyped λ Calculus (DJD), pp. 37–48.

RTA-1991-DrewesL #incremental #proving #termination

Incremental Termination Proofs and the Length of Derivations (FD, CL), pp. 49–61.

RTA-1991-Hofbauer #bound #proving #term rewriting #termination

Time Bounded Rewrite Systems and Termination Proofs by Generalized Embedding (DH), pp. 62–73.

RTA-1991-KrischerB #detection

Detecting Redundant Narrowing Derivations by the LSE-SL Reducability Test (SK, AB), pp. 74–85.

RTA-1991-Baader #bound #problem #unification

Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems (FB), pp. 86–97.

RTA-1991-Domenjoud #order #unification

AC Unification Through Order-Sorted AC1 Unification (ED), pp. 98–111.

RTA-1991-ChabinR #graph

Narrowing Directed by a Graph of Terms (JC, PR), pp. 112–123.

RTA-1991-BaaderN #algebra #commutative #equation #how #morphism #unification

Adding Homomorphisms to Commutative/Monoidal Theories or How Algebra Can Help in Equational Unification (FB, WN), pp. 124–135.

RTA-1991-Klay #decidability

Undecidable Properties of Syntactic Theories (FK), pp. 136–149.

RTA-1991-SnyderL

Goal Directed Strategies for Paramodulation (WS, CL), pp. 150–161.

RTA-1991-Pottier #algorithm #bound #linear

Minimal Solutions of Linear Diophantine Systems: Bounds and Algorithms (LP), pp. 162–173.

RTA-1991-Kirchner #proving #specification

Proofs in Parameterized Specification (HK), pp. 174–187.

RTA-1991-MiddeldorpT

Completeness of Combinations of Constructor Systems (AM, YT), pp. 188–199.

RTA-1991-NipkowQ #composition #higher-order

Modular Higher-Order E-Unification (TN, ZQ), pp. 200–214.

RTA-1991-CurienG #confluence #normalisation #on the

On Confluence for Weakly Normalizing Systems (PLC, GG), pp. 215–225.

RTA-1991-Bellegarde #program transformation

Program Transformation and Rewriting (FB), pp. 226–239.

RTA-1991-CohenW #performance #representation #term rewriting

An Efficient Representation of Arithmetic for Term Rewriting (DC, PW), pp. 240–251.

RTA-1991-DenneheuvelKLS #optimisation #query #using

Query Optimization Using Rewrite Rules (SvD, KLK, GRRdL, ES), pp. 252–263.

RTA-1991-Socher-Ambrosius #algebra #convergence #term rewriting

Boolean Algebra Admits No Convergent Term Rewriting System (RSA), pp. 264–274.

RTA-1991-Salomaa #confluence #decidability #monad #term rewriting #termination

Decidability of Confluence and Termination of Monadic Term Rewriting Systems (KS), pp. 275–286.

RTA-1991-CoquideDGV #automaton #bottom-up #term rewriting

Bottom-Up Tree Pushdown Automata and Rewrite Systems (JLC, MD, RG, SV), pp. 287–298.

RTA-1991-Kucherov #on the #term rewriting

On Relationship Between Term Rewriting Systems and Regular Tree Languages (GK), pp. 299–311.

RTA-1991-Brandenburg #bound #confluence #equivalence #graph grammar

The Equivalence of Boundary and Confluent Graph Grammars on Graph Languages of Bounded Degree (FJB), pp. 312–322.

RTA-1991-Graf #pattern matching

Left-to-Right Tree Pattern Matching (AG), pp. 323–334.

RTA-1991-RameshR #incremental #normalisation #performance #term rewriting

Incremental Techniques for Efficient Normalization of Nonlinear Rewrite Systems (RR, IVR), pp. 335–347.

RTA-1991-BonacinaH #on the #proving #theorem proving

On Fairness of Completion-Based Theorem Proving Strategies (MPB, JH), pp. 348–360.

RTA-1991-Avenhaus #equation #induction #proving #theorem

Proving Equational and Inductive Theorems by Completion and Embedding Techniques (JA), pp. 361–373.

RTA-1991-Sattler-Klein

Divergence Phenomena during Completion (ASK), pp. 374–385.

RTA-1991-Bundgen #algorithm #simulation

Simulation Buchberger’s Algorithm by Knuth-Bendix Completion (RB), pp. 386–397.

RTA-1991-Hermann #on the #proving

On Proving Properties of Completion Strategies (MH), pp. 398–410.

RTA-1991-Marche #on the

On Ground AC-Completion (CM), pp. 411–422.

RTA-1991-NarendranR #canonical #commutative #finite

Any Gound Associative-Commutative Theory Has a Finite Canonical System (PN, MR), pp. 423–434.

RTA-1991-Fraus #proving #theorem proving

A Narrowing-Based Theorem Prover (UF), pp. 435–436.

RTA-1991-Billaud #animation #graph grammar #interactive #named #term rewriting

ANIGRAF: An Interactive System for the Animation of Graph Rewriting Systems with Priorities (MB), pp. 437–438.

RTA-1991-Deruyver #equation #first-order #logic #named #proving #theorem proving

EMMY: A Refutational Theorem Prover for First-Order Logic with Equation (AD), pp. 439–441.

RTA-1991-AgarwalMKN #proving

The Tecton Proof System (RA, DRM, DK, XN), pp. 442–444.

RTA-1991-DershowitzJK #problem

Open Problems in Rewriting (ND, JPJ, JWK), pp. 445–456.