Rewriting Techniques and Applications: 6th International Conference, RTA-95 Kaiserslautern, Germany, April 5–7, 1995 Proceedings

On some mathematical logic contributions to rewriting techniques: Lost heritage....Pages 1-1
Modularity of completeness revisited....Pages 2-10
Automatic termination proofs with transformation orderings....Pages 11-25
A termination ordering for higher order rewrite systems....Pages 26-40
A complete characterization of termination of 0 p 1 q →1 r 0 s ....Pages 41-55
On narrowing, refutation proofs and constraints....Pages 56-70
Completion for multiple reduction orderings....Pages 71-85
Towards an efficient construction of test sets for deciding ground reducibility....Pages 86-100
Term rewriting in contemporary resolution theorem proving....Pages 101-101
 δ ο!∈=1 Optimizing optimal λ-calculus implementations....Pages 102-116
Substitution tree indexing....Pages 117-131
Concurrent garbage collection for concurrent rewriting....Pages 132-146
Lazy rewriting and eager machinery....Pages 147-162
A rewrite mechanism for logic programs with negation....Pages 163-178
Level-confluence of conditional rewrite systems with extra variables in right-hand sides....Pages 179-193
A polynomial algorithm testing partial confluence of basic semi-Thue systems....Pages 194-209
Problems in rewriting applied to categorical concepts by the example of a computational comonad....Pages 210-224
Relating two categorical models of term rewriting....Pages 225-240
Towards a domain theory for termination proofs....Pages 241-255
Higher-order rewrite systems....Pages 256-256
Infinitary lambda calculi and böhm models....Pages 257-270
Proving the genericity lemma by leftmost reduction is simple....Pages 271-278
(Head-)normalization of typeable rewrite systems....Pages 279-293
Explicit substitutions with de bruijn's levels....Pages 294-308
A restricted form of higher-order rewriting applied to an HDL semantics....Pages 309-323
Rewrite systems for integer arithmetic....Pages 324-338
General solution of systems of linear diophantine equations and inequations....Pages 339-351
Combination of constraint solving techniques: An algebraic point of view....Pages 352-366
Some independence results for equational unification....Pages 367-381
Regular substitution sets: A means of controlling E-unification....Pages 382-396
DISCOUNT: A system for distributed equational deduction....Pages 397-402
ASTRE: Towards a fully automated program transformation system....Pages 403-407
Parallel ReDuX → PaReDuX....Pages 408-413
STORM: A many-to-one associative-commutative matcher....Pages 414-419
LEMMA: A system for automated synthesis of recursive programs in equational theories....Pages 420-425
Generating polynomial orderings for termination proofs....Pages 426-431
Disguising recursively chained rewrite rules as equational theorems, as implemented in the prover EFTTP Mark 2....Pages 432-437
Prototyping completion with constraints using computational systems....Pages 438-443
Guiding term reduction through a neural network: Some preliminary results for the group theory....Pages 444-449
Studying quasigroup identities by rewriting techniques: Problems and first results....Pages 450-456
Problems in rewriting III....Pages 457-471