Term Rewriting and Applications: 17th International Conference, RTA 2006 Seattle, WA, USA, August 12-14, 2006 Proceedings

Randal E. Bryant (auth.), Frank Pfenning (eds.)3540368345, 9783540368342

This book constitutes the refereed proceedings of the 17th International Conference on Rewriting Techniques and Applications, RTA 2006, held in Seattle, WA, USA in August 2006 within the scope of FLoC 2006, the 2006 Federated Logic Conference.

The 23 revised full papers and 4 systems description papers carefully reviewed and selected from 52 initial submissions are presented together with 2 invited talks and a plenary talk of the hosting FLoC conference. The papers are organized in topical sections on constraints and optimization, equational reasoning, system verification, lambda calculus, theorem proving, system descriptions, termination, and higher-order rewriting and unification.

---

Table of contents :
Front Matter….Pages –
Formal Verification of Infinite State Systems Using Boolean Methods….Pages 1-3
Solving Partial Order Constraints for LPO Termination….Pages 4-18
Computationally Equivalent Elimination of Conditions….Pages 19-34
On the Correctness of Bubbling….Pages 35-49
Propositional Tree Automata….Pages 50-65
Generalizing Newman’s Lemma for Left-Linear Rewrite Systems….Pages 66-80
Unions of Equational Monadic Theories….Pages 81-95
Modular Church-Rosser Modulo….Pages 96-107
Hierarchical Combination of Intruder Theories….Pages 108-122
Feasible Trace Reconstruction for Rewriting Approximations….Pages 123-135
Rewriting Models of Boolean Programs….Pages 136-150
Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear λ -Calculus….Pages 151-165
A Terminating and Confluent Linear Lambda Calculus….Pages 166-180
A Lambda-Calculus with Constructors….Pages 181-196
Structural Proof Theory as Rewriting….Pages 197-211
Checking Conservativity of Overloaded Definitions in Higher-Order Logic….Pages 212-226
Certified Higher-Order Recursive Path Ordering….Pages 227-241
Dealing with Non-orientable Equations in Rewriting Induction….Pages 242-256
TPA: Termination Proved Automatically….Pages 257-266
RAPT : A Program Transformation System Based on Term Rewriting….Pages 267-276
The CL-Atse Protocol Analyser….Pages 277-286
Slothrop : Knuth-Bendix Completion with a Modern Termination Checker….Pages 287-296
Automated Termination Analysis for Haskell : From Term Rewriting to Programming Languages….Pages 297-312
Predictive Labeling….Pages 313-327
Termination of String Rewriting with Matrix Interpretations….Pages 328-342
Decidability of Termination for Semi-constructor TRSs, Left-Linear Shallow TRSs and Related Systems….Pages 343-356
Proving Positive Almost Sure Termination Under Strategies….Pages 357-371
A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property….Pages 372-386
Higher-Order Orderings for Normal Rewriting….Pages 387-399
Bounded Second-Order Unification Is NP-Complete….Pages 400-414
Back Matter….Pages –