## 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)

- 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.

9 ×#proving

9 ×#term rewriting

5 ×#on the

4 ×#bound

4 ×#equation

4 ×#unification

3 ×#algebra

3 ×#confluence

3 ×#graph grammar

3 ×#termination

9 ×#term rewriting

5 ×#on the

4 ×#bound

4 ×#equation

4 ×#unification

3 ×#algebra

3 ×#confluence

3 ×#graph grammar

3 ×#termination