Rewriting Techniques And Applications: 10th International Conference, Rta'99, Trento, Italy, July 2-4, 1999, Proceedings (lecture Notes In Computer Science)

This book constitutes the refereed proceedings of the 10th International Conference on Rewriting Techniques and Applications, RTA-99, held in Trento, Italy in July 1999 as part of FLoC'99. The 23 revised full papers presented were carefully selected from a total of 53 submissions. Also included are four system descriptions as well as three invited contributions. Among the topics covered are constraint solving, termination, deduction and higher order rewriting, graphs, complexity, tree automata, context-sensitive rewriting, string rewriting and numeration systems, etc. Solved Forms for Path Ordering Constraints....Pages 1-15 Jeopardy....Pages 16-29 Strategic Pattern Matching....Pages 30-44 On the Strong Normalization of Natural Deduction with Permutation-Conversions....Pages 45-59 Normalisation in Weakly Orthogonal Rewriting....Pages 60-74 Strong Normalization of Proof Nets Modulo Structural Congruences....Pages 75-89 Hierarchical Graph Decompositions Defined by Grammars and Logical Formulas....Pages 90-91 Deciding the Satisfiability of Quantifier Free Formulae on One-Step Rewriting....Pages 92-102 A New Result about the Decidability of the Existential One-Step Rewriting Theory....Pages 103-117 A Fully Syntactic AC-RPO....Pages 118-132 Theory Path Orderings....Pages 133-147 A Characterisation of Multiply Recursive Functions with Higman’s Lemma....Pages 148-162 Deciding the Word Problem in the Union of Equational Theories Sharing Constructors....Pages 163-174 Normalization via Rewrite Closures....Pages 175-189 Test Sets for the Universal and Existential Closure of Regular Tree Languages....Pages 190-204 Higher-Order Rewriting....Pages 205-219 The Maude System....Pages 220-239 TOY : A Multiparadigm Declarative System....Pages 240-243 UniMoK: A System for Combining Equational Unification Algorithms....Pages 244-247 Decidability for Left-Linear Growing Term Rewriting Systems....Pages 248-251 Transforming Context-Sensitive Rewrite Systems....Pages 252-255 Context-Sensitive AC-rewriting....Pages 256-270 The Calculus of Algebraic Constructions....Pages 271-285 HOL-λσ: An Intentional First-Order Expression of Higher-Order Logic....Pages 286-300 On the Connections between Rewriting and Formal Language Theory....Pages 301-316 A Rewrite System Associated with Quadratic Pisot Units....Pages 317-331 Fast Rewriting of Symmetric Polynomials....Pages 332-355 On Implementation of Tree Synchronized Languages....Pages 356-370 ....Pages 371-381 Rewriting Techniques and Applications: 10th International Conference, RTA-99 Trento, Italy, July 2–4, 1999 Proceedings Author: Paliath Narendran, Michael Rusinowitch Published by Springer Berlin Heidelberg ISBN: 978-3-540-66201-3 DOI: 10.1007/3-540-48685-2 Table of Contents: Solved Forms for Path Ordering Constraints Jeopardy Strategic Pattern Matching On the Strong Normalization of Natural Deduction with Permutation-Conversions Normalisation in Weakly Orthogonal Rewriting Strong Normalization of Proof Nets Modulo Structural Congruences Hierarchical Graph Decompositions Defined by Grammars and Logical Formulas Undecidability of the Deciding the Satisfiability of Quantifier Free Formulae on One-Step Rewriting A New Result about the Decidability of the Existential One-Step Rewriting Theory A Fully Syntactic AC-RPO Theory Path Orderings A Characterisation of Multiply Recursive Functions with Higman’s Lemma Deciding the Word Problem in the Union of Equational Theories Sharing Constructors Normalization via Rewrite Closures Test Sets for the Universal and Existential Closure of Regular Tree Languages Higher-Order Rewriting The Maude System TOY: A Multiparadigm Declarative System UniMoK: A System for Combining Equational Unification Algorithms This volume covers the 10th International Conference on Rewriting Techniques and Applications held in July 1999. It includes such topics as constraint solving, termination, deduction and higher order rewriting, graphs, complexity, tree automata, context-sensitive rewriting and string rewriting. A usual technique in symbolic constraint solving is to apply transformation rules until a solved form is reached for which the problem becomes simple.