## Hubert Comon

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

RTA, 1997.

@proceedings{RTA-1997, address = "Sitges, Spain", editor = "Hubert Comon", isbn = "3-540-62950-5", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the Eighth International Conference on Rewriting Techniques and Applications}", volume = 1232, year = 1997, }

### Contents (28 items)

- RTA-1997-McCune #problem
- Well-Behaved Search and the Robbins Problem (WM), pp. 1–7.
- RTA-1997-Lynch #graph #using
- Goal-Directed Completion Using SOUR Graphs (CL), pp. 8–22.
- RTA-1997-Kapur #congruence
- Shostak’s Congruence Closure as Completion (DK), pp. 23–37.
- RTA-1997-KuhlerW #data type #equation #induction #proving #specification #theorem proving
- Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving (UK, CPW), pp. 38–52.
- RTA-1997-OttoKK #decidability #monad #problem #word
- Cross-Sections for Finitely Presented Monoids with Decidable Word Problems (FO, MK, YK), pp. 53–67.
- RTA-1997-Sattler-Klein #monad
- New Undecidablility Results for Finitely Presented Monoids (ASK), pp. 68–82.
- RTA-1997-Otto #on the #string #term rewriting
- On the Property of Preserving Regularity for String-Rewriting Systems (FO), pp. 83–97.
- RTA-1997-ContejeanMR #term rewriting
- Rewrite Systems for Natural, Integral, and Rational Arithmetic (EC, CM, LR), pp. 98–112.
- RTA-1997-BachmairT #commutative #polynomial
- D-Bases for Polynomial Ideals over Commutative Noetherian Rings (LB, AT), pp. 113–127.
- RTA-1997-Struth #for free #on the #problem #word
- On the Word Problem for Free Lattices (GS), pp. 128–141.
- RTA-1997-KapurS #order #proving #term rewriting #termination
- A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems (DK, GS), pp. 142–156.
- RTA-1997-ArtsG #automation #normalisation #proving
- Proving Innermost Normalisation Automatically (TA, JG), pp. 157–171.
- RTA-1997-Zantema #termination
- Termination of Context-Sensitive Rewriting (HZ), pp. 172–186.
- RTA-1997-OyamaguchiO #linear #parallel #term rewriting
- A New Parallel Closed Condition for Church-Rossser of Left-Linear Term Rewriting Systems (MO, YO), pp. 187–201.
- RTA-1997-Dershowitz
- Innocuous Constructor-Sharing Combinations (ND), pp. 202–216.
- RTA-1997-Perlo-FreemanP
- Scott’s Conjecture is True, Position Sensitive Weights (SMHWPF, PP), pp. 217–227.
- RTA-1997-Lafont #2d
- Two-Dimensional Rewriting (YL), pp. 228–229.
- RTA-1997-BechetGR #axiom #partial order
- A Complete Axiomatisation for the Inclusion of Series-Parallel Partial Orders (DB, PdG, CR), pp. 230–240.
- RTA-1997-Marcinkowski #first-order
- Undecidability of the First Order Theory of One-Step Right Ground Rewriting (JM), pp. 241–253.
- RTA-1997-Vorobyov #decidability #first-order #linear
- The First-Order Theory of One Step Rewriting in Linear Noetherian Systems is Undecidable (SGV), pp. 254–268.
- RTA-1997-TomasF #equation #geometry #linear #using
- Solving Linear Diophantine Equations Using the Geometric Structure of the Solution Space (APT, MF), pp. 269–283.
- RTA-1997-Schulz #algorithm
- A Criterion for Intractability of E-unification with Free Function Symbols and Its Relevance for Combination Algorithms (KUS), pp. 284–298.
- RTA-1997-Statman #combinator #effectiveness #reduction
- Effective Reduction and Conversion Strategies for Combinators (RS), pp. 299–307.
- RTA-1997-Oostrom #finite #product line
- Finite Family Developments (VvO), pp. 308–322.
- RTA-1997-Ringeissen #algorithm #programming language #prototype #rule-based #unification
- Prototyping Combination of Unification Algorithms with the ELAN Rule-Based Programming Language (CR), pp. 323–326.
- RTA-1997-Gobel #invariant
- The Invariant Package of MAS (MG), pp. 327–330.
- RTA-1997-GreenHK #commutative #named
- Opal: A System for Computing Noncommutative Gröbner Bases (ELG, LSH, BJK), pp. 331–334.
- RTA-1997-OgataOF #automaton #named #order #term rewriting
- TRAM: An Abstract Machine for Order-Sorted Conditioned Term Rewriting Systems (KO, KO, KF), pp. 335–338.

5 ×#term rewriting

3 ×#linear

3 ×#problem

3 ×#proving

2 ×#algorithm

2 ×#commutative

2 ×#decidability

2 ×#equation

2 ×#first-order

2 ×#monad

3 ×#linear

3 ×#problem

3 ×#proving

2 ×#algorithm

2 ×#commutative

2 ×#decidability

2 ×#equation

2 ×#first-order

2 ×#monad