## Jieh Hsiang

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

RTA, 1995.

@proceedings{RTA-1995, address = "Kaiserslautern, Germany", editor = "Jieh Hsiang", isbn = "3-540-59200-8", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the Sixth International Conference on Rewriting Techniques and Applications}", volume = 914, year = 1995, }

### Contents (41 items)

- RTA-1995-Matiyasevich #logic #on the
- On Some Mathematical Logic Contributions to Rewriting Techniques: Lost Heritage (YM), p. 1.
- RTA-1995-Marchiori #composition #revisited
- Modularity of Completeness Revisited (MM), pp. 2–10.
- RTA-1995-Steinbach #automation #order #proving #termination
- Automatic Termination Proofs With Transformation Orderings (JS), pp. 11–25.
- RTA-1995-LysneP #higher-order #term rewriting #termination
- A Termination Ordering for Higher Order Rewrite System (OL, JP), pp. 26–40.
- RTA-1995-ZantemaG #termination
- A Complete Characterization of Termination of O
^{p}1^{q}-> 1^{r}O^{s}(HZ, AG), pp. 41–55. - RTA-1995-Nieuwenhuis #constraints #on the #proving
- On Narrowing, Refutation Proofs and Constraints (RN), pp. 56–70.
- RTA-1995-KuriharaKO #multi #order #reduction
- Completion for Multiple Reduction Orderings (MK, HK, AO), pp. 71–85.
- RTA-1995-SchmidF #performance #testing #towards
- Towards an Efficient Construction of Test Sets for Deciding Ground Reducability (KS, RF), pp. 86–100.
- RTA-1995-Stickel #proving #term rewriting #theorem proving
- Term Rewriting in Contemporary Resolution Theorem Proving (MES), p. 101.
- RTA-1995-Asperti #exclamation #implementation #optimisation #λ-calculus
*delta*o!*Epsilon*= 1 — Optimizing Optimal*λ*-Calculus Implementations (AA), pp. 102–116.- RTA-1995-Graf
- Substitution Tree Indexing (PG), pp. 117–131.
- RTA-1995-Alouini #concurrent #garbage collection
- Concurrent Garbage Collection for Concurrent Rewriting (IA), pp. 132–146.
- RTA-1995-KampermanW #lazy evaluation
- Lazy Rewriting and Eager Machinery (JFTK, HRW), pp. 147–162.
- RTA-1995-AnantharamanR #logic programming #source code
- A Rewrite Mechanism for Logic Programs with Negation (SA, GR), pp. 163–178.
- RTA-1995-SuzukiMI #term rewriting
- Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides (TS, AM, TI), pp. 179–193.
- RTA-1995-Senizergues #algorithm #confluence #polynomial #testing
- A Polynomial Algorithm Testing Partial Confluence of Basic Semi-Thue Systems (GS), pp. 194–209.
- RTA-1995-Gehrke #category theory #concept #monad #problem
- Problems in Rewriting Applied to Categorical Concepts by the Example of a Computational Comonad (WG), pp. 210–224.
- RTA-1995-CorradiniGM #modelling #term rewriting
- Relating Two Categorial Models of Term Rewriting (AC, FG, UM), pp. 225–240.
- RTA-1995-Kahrs #proving #termination #towards
- Towards a Domain Theory for Termination Proofs (SK), pp. 241–255.
- RTA-1995-Nipkow #higher-order #term rewriting
- Higher-Order Rewrite Systems (TN), p. 256.
- RTA-1995-KennawayKSV #modelling #λ-calculus
- Infinitary λ Calculi and Böhm Models (RK, JWK, MRS, FJdV), pp. 257–270.
- RTA-1995-Kuper #proving #reduction
- Proving the Genericity Lemma by Leftmost Reduction is Simple (JK), pp. 271–278.
- RTA-1995-BakelF #normalisation #term rewriting #type system
- (Head-) Normalization of Typeable Rewrite Systems (SvB, MF), pp. 279–293.
- RTA-1995-LescanneR
- Explicit Substitutions with de Bruijn’s Levels (PL, JRD), pp. 294–308.
- RTA-1995-Boulton #higher-order #semantics #strict
- A Restricted Form on Higher-Order Rewriting Applied to an HDL Semantics (RJB), pp. 309–323.
- RTA-1995-WaltersZ #integer #term rewriting
- Rewrite Systems for Integer Arithmetic (HRW, HZ), pp. 324–338.
- RTA-1995-AbdulrabM #equation #linear
- General Solution of Systems of Linear Diophantine Equations and Inequations (HA, MM), pp. 339–351.
- RTA-1995-BaaderS #algebra #constraints #perspective #theorem proving
- Combination of Constraint Solving Techniques: An Algebraic POint of View (FB, KUS), pp. 352–366.
- RTA-1995-OttoND #equation #independence #unification
- Some Independent Results for Equational Unification (FO, PN, DJD), pp. 367–381.
- RTA-1995-Burghardt #set
- Regular Substitution Sets: A Means of Controlling E-Unification (JB), pp. 382–396.
- RTA-1995-AvenhausDF #deduction #distributed #equation #named
- DISCOUNT: A SYstem for Distributed Equational Deduction (JA, JD, MF), pp. 397–402.
- RTA-1995-Bellegarde #automation #named #program transformation #towards
- ASTRE: Towards a Fully Automated Program Transformation System (FB), pp. 403–407.
- RTA-1995-BundgenGK #parallel
- Parallel ReDuX -> PaReDuX (RB, MG, WK), pp. 408–413.
- RTA-1995-ChenA #commutative #named
- STORM: A MAny-to-One Associative-Commutative Matcher (TC, SA), pp. 414–419.
- RTA-1995-ChazarainM #automation #equation #named #recursion #source code #synthesis
- LEMMA: A System for Automated Synthesis of Recursive Programs in Equational Theories (JC, SM), pp. 420–425.
- RTA-1995-Giesl #generative #order #polynomial #proving #termination
- Generating Polynomial Orderings for Termination Proofs (JG), pp. 426–431.
- RTA-1995-Holmes #equation #proving #recursion #theorem
- Disguising Recursively Chained Rewrite Rules as Equational Theorems, as Implemented in the Prover EFTTP Mark 2 (MRH), pp. 432–437.
- RTA-1995-KirchnerM #constraints #prototype #using
- Prototyping Completion with Constraints Using Computational Systems (HK, PEM), pp. 438–443.
- RTA-1995-Paccanaro #network #reduction
- Guiding Term Reduction Through a Neural Network: Some Prelimanary Results for the Group Theory (AP), pp. 444–449.
- RTA-1995-StickelZ #problem
- Studying Quasigroup Identities by Rewriting Techniques: Problems and First Results (MES, HZ), pp. 450–456.
- RTA-1995-DershowitzJK #problem
- Problems in Rewriting III (ND, JPJ, JWK), pp. 457–471.

7 ×#proving

7 ×#term rewriting

5 ×#equation

5 ×#termination

4 ×#named

3 ×#automation

3 ×#constraints

3 ×#higher-order

3 ×#order

3 ×#problem

7 ×#term rewriting

5 ×#equation

5 ×#termination

4 ×#named

3 ×#automation

3 ×#constraints

3 ×#higher-order

3 ×#order

3 ×#problem