## Nachum Dershowitz

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

RTA, 1989.

@proceedings{RTA-1989, address = "Chapel Hill, North Carolina, USA", editor = "Nachum Dershowitz", isbn = "3-540-51081-8", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the Third International Conference on Rewriting Techniques and Applications}", volume = 355, year = 1989, }

### Contents (47 items)

- RTA-1989-Birkhoff #algebra #perspective #term rewriting
- Term Rewriting and Universal Algebra in Historical Perspective (GB), p. 1.
- RTA-1989-Baader #unification
- Characterization of Unification Type Zero (FB), pp. 2–14.
- RTA-1989-Bachmair #normalisation #proving
- Proof Normalization for Resolution and Paramodulation (LB), pp. 15–28.
- RTA-1989-BairdPW #commutative #reduction #set
- Complete Sets of Reductions Modulo Associativity, Commutativity and Identity (TBB, GEP, RWW), pp. 29–44.
- RTA-1989-BertlingG #optimisation
- Completion-Time Optimization of Rewrite-Time Goal Solving (HB, HG), pp. 45–58.
- RTA-1989-BundgenK
- Computing Ground Reducability and Inductively Complete Positions (RB, WK), pp. 59–75.
- RTA-1989-Comon #induction #proving #specification
- Inductive Proofs by Specification Transformation (HC), pp. 76–91.
- RTA-1989-DarlingtonG #abstraction #evaluation #functional #programming #set #unification
- Narrowing and Unification in Functional Programming — An Evaluation Mechanism for Absolute Set Abstraction (JD, YG), pp. 92–108.
- RTA-1989-Dauchet #linear #simulation #turing machine
- Simulation of Turing Machines by a Left-Linear Rewrite Rule (MD), pp. 109–120.
- RTA-1989-Elliott #higher-order #unification
- Higher-order Unification with Dependent Function Types (CE), pp. 121–136.
- RTA-1989-GarlandG #overview
- An Overview of LP, The Larch Power (SJG, JVG), pp. 137–151.
- RTA-1989-Gottler #graph grammar #implementation #visual notation
- Graph Grammars, A New Paradigma for Implementing Visual Languages (HG), pp. 152–166.
- RTA-1989-HofbauerL #proving #termination
- Termination Proofs and the Length of Derivations (DH, CL), pp. 167–177.
- RTA-1989-KaplanC
- Abstract Rewriting with Concrete Operations (SK, CC), pp. 178–186.
- RTA-1989-Lai #commutative #how #on the
- On How To Move Mountains “Associatively and Commutatively” (ML), pp. 187–202.
- RTA-1989-Lankford #theory and practice
- Generalized Gröbner Bases: Theory and Applications. A Condensation (DL), pp. 203–221.
- RTA-1989-LatchS #term rewriting #termination
- A Local Termination Property for Term Rewriting Systems (DML, RS), pp. 222–233.
- RTA-1989-McNulty #equation #logic
- An Equational Logic Sampler (GFM), pp. 234–262.
- RTA-1989-Middeldorp #aspect-oriented #composition #normalisation #term rewriting
- Modular Aspects of Properties of Term Rewriting Systems Related to Normal Forms (AM), pp. 263–277.
- RTA-1989-Mohan #confluence #semantics
- Priority Rewriting: Semantics, Confluence, and Conditional (CKM), pp. 278–291.
- RTA-1989-MohanS #logic
- Negation with Logical Variables in Conditional Rewriting (CKM, MKS), pp. 292–310.
- RTA-1989-NaoiI #algebra #complexity #semantics #term rewriting
- Algebraic Semantics and Complexity of Term Rewriting Systems (TN, YI), pp. 311–325.
- RTA-1989-Narain #lazy evaluation #nondeterminism #optimisation
- Optimization by Non-Deterministic, Lazy Rewriting (SN), pp. 326–342.
- RTA-1989-Nipkow #algorithm
- Combining Matching Algorithms: The Rectangular Case (TN), pp. 343–358.
- RTA-1989-Otto #canonical #congruence #finite #strict #string #term rewriting
- Restrictions of Congruence Generated by Finite Canonical String-Rewriting Systems (FO), pp. 359–370.
- RTA-1989-Puel #order #recursion
- Embedding with Patterns and Associated Recursive Path Ordering (LP), pp. 371–387.
- RTA-1989-Reddy #synthesis
- Rewriting Techniques for Program Synthesis (USR), pp. 388–403.
- RTA-1989-SekarPR #execution #parallel #performance #term rewriting
- Transforming Strongly Sequential Rewrite Systems with Constructors for Efficient parallel Execution (RCS, SP, IVR), pp. 404–418.
- RTA-1989-Snyder #algorithm #equation #generative #performance #set
- Efficient Ground Completion: An
*O(n log n)*Algorithm for Generating Reduced Sets of Ground Rewrite Rules Equivalent to a Set of Ground Equations E (WS), pp. 419–433. - RTA-1989-Steinbach #comparison #order
- Extensions and Comparison of Simplification Orderings (JS), pp. 434–448.
- RTA-1989-Strandh #equation #performance #source code
- Classes of Equational Programs that Compile into Efficient Machine Code (RS), pp. 449–461.
- RTA-1989-Tison #decidability #termination
- Fair Termination is Decidable for Ground Systems (ST), pp. 462–476.
- RTA-1989-ToyamaKB #linear #term rewriting #termination
- Termination for the Direct Sum of left-Linear Term Rewriting Systems -Preliminary Draft- (YT, JWK, HPB), pp. 477–491.
- RTA-1989-Vorobyov #induction
- Conditional Rewrite Rule Systems with Built-In Arithmetic and Induction (SGV), pp. 492–512.
- RTA-1989-ZhangK
- Consider Only General Superpositions in Completion Procedures (HZ, DK), pp. 513–527.
- RTA-1989-AbdulrabP #equation #linear #word
- Solving Systems of Linear Diophantine Equations and Word Equations (HA, JPP), pp. 530–532.
- RTA-1989-AnantharamanHM #named #term rewriting
- SbReve2: A Term Rewriting Laboratory with (AC-) Unfailing Completion (SA, JH, JM), pp. 533–537.
- RTA-1989-AvenhausDM #named #performance #proving #theorem proving
- THEOPOGLES — An efficient Theorem Prover based on Rewrite-Techniques (JA, JD, JM), pp. 538–541.
- RTA-1989-AvenhausMS #named #term rewriting
- COMTES — An Experimental Environment for the Completion of Term Rewriting Systems (JA, KM, JS), pp. 542–546.
- RTA-1989-BidoitCC #named #specification
- ASSPEGIQUE: An Integrated Specification Environment (MB, FC, CC), p. 547.
- RTA-1989-BonacinaS #equation #named #proving #theorem proving
- KBlab: An Equational Theorem Prover for the Macintosh (MPB, GS), pp. 548–550.
- RTA-1989-Christian #performance #summary
- Fast Knuth-Bendix Completion: Summary (JC), pp. 551–555.
- RTA-1989-DauchetD #compilation #term rewriting
- Compilation of Ground Term Rewriting Systems and Applications (MD, AD), pp. 556–558.
- RTA-1989-KapurZ #overview
- An Overview of Rewrite Rule Laboratory (RRL) (DK, HZ), pp. 559–563.
- RTA-1989-KhoshnevisanS #automation #named
- InvX: An Automatic Function Inverter (HK, KMS), pp. 564–568.
- RTA-1989-Lindenstrauss #implementation #parallel
- A Parallel Implementation of Rewriting and Narrowing (NL), pp. 569–573.
- RTA-1989-Pedersen #monad
- Morphocompletion for One-Relation Monoids (JP), pp. 574–578.

10 ×#term rewriting

6 ×#named

5 ×#equation

5 ×#performance

5 ×#proving

4 ×#termination

3 ×#linear

3 ×#set

3 ×#unification

2 ×#algebra

6 ×#named

5 ×#equation

5 ×#performance

5 ×#proving

4 ×#termination

3 ×#linear

3 ×#set

3 ×#unification

2 ×#algebra