Rewriting techniques and applications : 4th International Conference, RTA-91 Como, Italy, April 10 12, 1991 : proceedings
This volume contains the proceedings of the Fourth International Conference on Rewriting Techniques and Applications (RTA-91), held in Como, Italy, April 10-12, 1991. The volume includes 40 papers on a wide variety of topics including: term rewriting systems, equational unification, algebraic rewrit...
Enregistré dans:
| Collectivité auteur: | |
|---|---|
| Autres auteurs: | |
| Format: | Livre numérique |
| Langue: | Anglais |
| Publié: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Collection: | Lecture notes in computer science
488 |
| Sujets: | |
| Accès en ligne: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Note: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Rewriting techniques and applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, proceedings, Ronald V. Book, ed., Berlin, Springer-Verlag, 1991, 1 vol. (vii, 458 p.), Lecture notes in computer science, 0-387-53904-2 • Rewriting Techniques and Applications, Texte imprimé, 9783662181737 |
Table des matières:
- Transfinite reductions in orthogonal term rewriting systems
- Redex capturing in term graph rewriting (concise version)
- Rewriting, and equational unification: the higher-order cases
- Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
- Incremental termination proofs and the length of derivations
- Time bounded rewrite systems and termination proofs by generalized embedding
- Detecting redundant narrowing derivations by the LSE-SL reducibility test
- Unification, weak unification, upper bound, lower bound, and generalization problems
- AC unification through order-sorted AC1 unification
- Narrowing directed by a graph of terms
- Adding homomorphisms to commutative/monoidal theories or how algebra can help in equational unification
- Undecidable properties of syntactic theories
- Goal directed strategies for paramodulation
- Minimal solutions of linear diophantine systems : bounds and algorithms
- Proofs in parameterized specifications
- Completeness of combinations of constructor systems
- Modular higher-order E-unification
- On confluence for weakly normalizing systems
- Program transformation and rewriting
- An efficient representation of arithmetic for term rewriting
- Query optimization using rewrite rules
- Boolean algebra admits no convergent term rewriting system
- Decidability of confluence and termination of monadic term rewriting systems
- Bottom-up tree pushdown automata and rewrite systems
- On relationship between term rewriting systems and regular tree languages
- The equivalence of boundary and confluent graph grammars on graph languages of bounded degree
- Left-to-right tree pattern matching
- Incremental techniques for efficient normalization of nonlinear rewrite systems
- On fairness of completion-based theorem proving strategies
- Proving equational and inductive theorems by completion and embedding techniques
- Divergence phenomena during completion
- Simulating Buchberger's algorithm by Knuth-Bendix completion
- On proving properties of completion strategies
- On ground AC-completion
- Any ground associative-commutative theory has a finite canonical system
- A narrowing-based theorem prover
- ANIGRAF: An interactive system for the animation of graph rewriting systems with priorities
- Emmy: A refutational theorem prover for first-order logic with equations
- The tecton proof system
- Open problems in rewriting.