Rewriting techniques and applications : 7th international conference, RTA-96, New Brunswick, NJ, USA, July 27 30, 1996 : proceedings
This book constitutes the refereed proceedings of the 7th International Conference on Rewriting Techniques and Applications, RTA-96, held in New Brunswick, NJ, USA, in July 1996. The 27 revised full papers presented in this volume were selected from a total of 84 submissions, also included are six s...
Salvato in:
| Ente Autore: | |
|---|---|
| Altri autori: | |
| Natura: | Livre numérique |
| Lingua: | Anglais |
| Pubblicazione: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serie: | Lecture notes in computer science
1103 |
| Soggetti: | |
| Accesso online: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Nota: |
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, 7th international conference, RTA-96, New Brunswick, NJ, USA, July 1996, proceedings, Harald Ganzinger (ed.), 1996, New York, Springer, 1 vol. (XI-435 p.), Lecture notes in computer science, 3-540-61464-8 • Rewriting Techniques and Applications, Texte imprimé, 9783662207376 |
Sommario:
- Rewrite-based automated reasoning: Challenges ahead
- Fine-grained concurrent completion
- AC-complete unification and its application to theorem proving
- Superposition theorem proving for abelian groups represented as integer modules
- Symideal Gröbner bases
- Termination of constructor systems
- Dummy elimination in equational rewriting
- On proving termination by innermost termination
- A recursive path ordering for higher-order terms in ?-long ?-normal form
- Higher-order superposition for dependent types
- Higher-order narrowing with definitional trees
- Design of a proof assistant
- A compiler for nondeterministic term rewriting systems
- Combinatory reduction systems with explicit substitution that preserve strong normalisation
- Confluence properties of extensional and non-extensional ?-calculi with explicit substitutions (extended abstract)
- On the power of simple diagrams
- Coherence for sharing proof nets
- Modularity of termination in term graph rewriting
- Confluence of terminating conditional rewrite systems revisited
- Applications of rewrite techniques in monoids and rings
- Compositional term rewriting: An algebraic proof of Toyama's theorem
- The first-order theory of one-step rewriting is undecidable
- An algorithm for distributive unification
- On the termination problem for one-rule semi-Thue system
- Efficient second-order matching
- Linear second-order unification
- Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
- Decidable approximations of term rewriting systems
- Semantics and strong sequentially of priority term rewriting systems
- Higher-order families
- A new proof manager and graphic interface for the larch prover
- ReDuX 1.5: New facets of rewriting
- CiME: Completionmodulo E
- Distributed larch prover (DLP): An experiment in parallelizing a rewrite-rule based prover
- EPIC: An equational language Abstract machine and supporting tools
- SPIKE-AC: A system for proofs by induction in Associative-Commutative theories
- On gaining efficiency in completion-based theorem proving.