This book constitutes the refereed proceedings of the 20th International Conference on Rewriting Techniques and Applications, RTA 2009, held in Brasília, Brazil, during June 29 - July 1, 2009. The 22 revised full papers and four system descriptions presented were carefully reviewed and selected from 59 initial submissions. The papers cover current research on all aspects of rewriting including typical areas of interest such as applications, foundational issues, frameworks, implementations, and semantics.
Table of Contents
Cover
Rewriting Techniques and Applications, 20th International Conference,
RTA 2009, Brasília, Brazil, June 29-July 1, 2009, Proceedings
ISBN-10 3642023479 ISBN-13 9783642023477
Preface
Organization
Table of Contents
Automatic Termination
\* Introduction
\* Automata, Rewriting, ...and Termination?
\* Weighted Automata ...
\* ... for Termination of Rewriting
\* Matrix Interpretations
\* Weighted Tree Automata
\* Half-Strict Semirings
\* Match Heights
\* Constraint Solving
\* Automata Completion
\* Matrix Termination Hierarchy
\* Weighted Automata for Derivational Complexity
\* References
Loops under Strategies
\* Introduction
\* Loops
\* Deciding Outermost Loops
\* Deciding Solvability of Extended Matching Problems
\* Deciding Solvability of Extended Identity Problems
\* Empirical Results
\* Conclusion and Future Work
\* References
Proving Termination of Integer Term Rewriting
\* Introduction
\* Integer Term Rewriting
\* Integer Dependency Pair Framework
\* Conditional Constraints
\* Generating I-Interpretations
\* Experiments and Conclusion
\* References
Dependency Pairs and Polynomial Path Orders
\* Introduction
\* The Polynomial Path Order on Sequences
\* Complexity Analysis Based on the Dependency Pair Method
\* The Polynomial Path Order over Quasi-precedences
\* Dependency Pairs and Polynomial Path Orders
\* Experimental Results
\* Conclusion
\* References
Unique Normalization for Shallow TRS
\* Preliminaries
\* Decidability of UN for Shallow and Linear TRS
+ Preliminary Results
+ Necessary and Sufficient Conditions for UN
+ Decision of UN
\* Undecidability of UN for Flat and Right-Linear TRS
\* References
The Existential Fragment of the One-Step Parallel Rewriting Theory
\* Introduction
\* Preliminaries
+ One-Step Parallel Rewriting Theory
\* The Undecidability Construction
+ Left-Terminal Turing Machines
+ Rewriting and LTTM
\* Discussion
\* References
Proving Confluence of Term Rewriting Systems Automatically
\* Introduction
\* Preliminaries
\* Direct Methods
\* Divide and Conquer Methods
+ Persistent Decomposition
+ Layer-Preserving Decomposition
+ Commutative Decomposition
\* Implementation and Experiments
\* Conclusion
\* References
A Proof Theoretic Analysis of Intruder Theories
\* Introduction
\* Intruder Deduction Under AC Convergent Theories
\* Cut Elimination for {\mathcal S}
\* Normal Derivations and Decidability
\* Some Example Theories
\* Combining Disjoint Convergent Theories
\* Conclusion and Related Work
\* References
Flat and One-Variable Clauses for Single Blind Copying Protocols: The
XOR Case
\* Introduction
\* Modeling and Some Undecidability Results
+ Protocols
+ Related classes
\* Results on Unification
\* The Normalization Algorithm
\* Conclusion
\* References
Protocol Security and Algebraic Properties: Decision Results for a
Bounded Number of Sessions
\* Introduction
\* Rewriting and Security
+ Term Rewriting
+ A Relevant Equational Theory
+ Semantic Subterms
+ Deducibility Constraints
\* The Four Main Properties
+ Locality
+ Conservativity
+ Finite Variant Property
+ A Decision Algorithm for Deducibility Constraints
\* Pure Deducibility Constraints
+ Reduction to Three Recipe Types
+ Guessing Top Symbols and Equalities
+ Stabilizing the Root Symbol
+ Eliminating Variables from Left Hand Sides: Reducing
Deducibility Constraints to Linear Diophantine Equations
+ Turning Deduction Constraints into Linear Diophantine
Equations
+ Solving the System of Equations
\* Conclusion
\* References
YAPA: A Generic Tool for Computing Intruder Knowledge
\* Introduction
\* Preliminaries
+ Term Algebra
+ Rewriting
+ Equational Theories
\* Deducibility and Static Equivalence
+ Deducibility, Recipes
+ Static Equivalence, Visible Equations
\* Main Procedure
+ Decompositions of Rewrite Rules
+ Transformation Rules
+ Application to Deduction and Static Equivalence
\* Soundness and Completeness of the Saturation
\* Termination and Non-failure
+ A Syntactic Criterion to Prevent Failure
+ Termination
\* Implementation: The YAPA Tool
\* References
Well-Definedness of Streams by Termination
\* Introduction
\* Streams: Specifications and Models
\* The Observational Variant
\* The Main Theorem
\* Data Independent Stream Functions
\* Fixpoints
\* Conclusions
\* References
Modularity of Convergence in Infinitary Rewriting
\* Introduction
\* Basic Definitions and Results about Convergence
\* Infinitary Term Rewriting
\* Counterexamples and Near Counterexamples
\* Definitions and Observations Useful for Both Proofs
\* Modularity of Convergence
\* Modularity of Strong Convergence
\* Conclusion
\* References
A Heterogeneous Pushout Approach to Term-Graph Transformation
\* Introduction
\* Graphs
\* Rewriting
\* Examples
\* Related Work
\* Conclusion
\* References
An Explicit Framework for Interaction Nets
\* Introduction
\* Permutations and Partial Injections
+ Permutations
+ Partial Injections
+ Execution
+ $w$-Permutations and Ex-Composition
\* The Statics of Interaction Nets
+ Representation
+ Morphisms of Nets and Renaming
\* Tools of the Trade
+ Gluing and Cutting
+ Interfaces and Contexts
\* Dynamics
\* Interaction Nets are the {\sf E}x-Collapse of Axiom/Cut Nets
+ Definition and Juxtaposition
+ {\sf E}x-collapse
\* Conclusion
\* References
Dual Calculus with Inductive and Coinductive Types
\* Introduction
\* Dual Calculus {\tt DC}
\* Dual Calculus {\sf DC}$\_{\mu\nu} with Inductive and Coinductive
Types
\* Examples
\* Second-Order Dual Calculus {\tt DC}2
\* Strong Normalization of {\tt DC}$\_{\mu\nu}
\* References
Comparing Böhm-Like Trees
\* Introduction
\* Preliminaries
\* Infinitary Rewriting
+ Axioms
+ Meaningful Terms
+ Böhm-Like Trees
+ Extending $U$ with $\perp$
+ Examples
\* Comparison
+ From Infinitary Rewriting to Direct Approximants
+ From Direct Approximants to Infinitary Rewriting
\* Conclusion
\* References
The Derivational Complexity Induced by the Dependency Pair Method
\* Introduction
\* Dependency Pairs
\* Progenitor and Progeny
\* Dependency Pairs and Complexity
\* The Lower Bound
\* Conclusion
\* References
Local Termination
\* Introduction
\* Preliminaries
\* Local Termination
\* Local Relative Termination
\* Stepwise Removal of Rules
\* Via Models from Local to Global Termination
\* Quasi-models for Local Termination
\* Conclusion
\* References
VMTL-A Modular Termination Laboratory
\* Introduction and Overview
\* Preliminaries
+ The Context-Sensitive Dependency Pair Framework
\* User Interface
+ User Defined Strategies
\* VMTL API
+ Adding New Dependency Pair Processors
+ Adding New Transformations
+ Customizing Output Formatting
\* Termination of CTRSs
\* Implementation Details and Benchmarks
\* Conclusion, Related and Future Work
\* References
Tyrolean Termination Tool 2
\* Introduction
\* Design
+ Command Line Interface
+ Web Interface
\* The Strategy Language
+ Syntax
+ Semantics
+ Specification and Configuration
\* A Selection of Implemented Techniques
\* ${\sf T\_{T}T}\_{2}$ in Action
\* Future Work
\* Conclusion
\* References
From Outermost to Context-Sensitive Rewriting
\* Introduction
\* Preliminaries
\* Transformation by Dynamic Labeling
\* Constructing Suitable Algebras
\* Minimizing Algebras
\* Two Versions of Dynamic Labeling
\* Discussion
\* References
A Fully Abstract Semantics for Constructor Systems
\* Introduction
\* Preliminaries
\* A Semantics for CS
+ SCTerms: The Pieces of the Semantics
+ A Proof Calculus
+ Relation with Rewriting
\* Full Abstraction
\* Conclusions
\* References
The $\Pi^{0}\_{2}$-Completeness of Most of the Properties of Rewriting
Systems You Care About (and Productivity)
\* (Uniform) Undecidability in Term Rewriting
\* Preliminaries
+ Turing Machines
+ The Arithmetical Hierarchy and $\Pi^{0}\_{2}$
\* Encoding Turing Machines
+ Adding Rules for Ground-WCR and CR: the Encoding
$\triangle$g(M)
\* $\Pi^{0}\_{2}$-Completeness of the Standard Properties
+ (Ground-)Local Confluence
+ (Ground-)Confluence
+ Normalization
+ Termination
+ Completeness
\* $\Pi^{0}\_{2}$-Completeness of Productivity (of Stream
Specifications)
\* References
Unification in the Description Logic EL
\* Introduction
\* Unification in {\mathcal EL}
\* Equivalence and Subsumption in {\mathcal EL}
\* An {\mathcal EL}-Unification Problem of Type Zero
\* The Decision Problem
\* Unification in Semilattices with Monotone Operators
\* Conclusion
\* References
Unification with Singleton Tree Grammars
\* Introduction
+ Outline of the Algorithm
\* Preliminaries
\* Basic Operations with STG and SCFG
+ Known Results
+ Finding the First Different Position of Two Terms
+ Application of Substitutions and a Notion of Restricted Depth
\* A Polynomial Time Algorithm for First-Order Unification with STG
\* Conclusion and Further Research
\* References
Unification and Narrowing in Maude 2.4
\* Introduction
\* Unification
\* Narrowing
\* Other Available Features
\* Some Applications
\* References
Author Index

lgrsnf/Cs_Computer science/CsLn_Lecture notes/R/Rewriting Techniques and Applications, 20 conf., RTA 2009(LNCS5595, Springer, 2009)(ISBN 3642023479)(O)(400s).pdf

nexusstc/Rewriting Techniques and Applications: 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009 Proceedings/fb50481c98d0df041483342bcdbcc352.pdf

scihub/10.1007/978-3-642-02348-4.pdf

Rewriting techniques and applications : 20th International Conference, RTA 2009 Brasilia, Brazil, June 29 - July 1, 2009 ; proceedings

edited by David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Doug Tygar, Moshe Y. Vardi, Gerhard Weikum, Ralf Treinen

David Hutchison; Moni Naor; C Pandu Rangan; Madhu Sudan; Doug Tygar; Bernhard Steffen; Takeo Kanade; Josef Kittler; Jon M Kleinberg; John C Mitchell; Oscar Nierstrasz; Moshe Y Vardi; Demetri Terzopoulos; Ralf Treinen; Gerhard Weikum; Friedemann Mattern

International Conference on Rewriting Techniques and Applications

Hutchison, David - undifferentiated

Ralf Treinen; RTA

Spektrum Akademischer Verlag. in Springer-Verlag GmbH

Springer Berlin Heidelberg : Imprint: Springer

Steinkopff. in Springer-Verlag GmbH

Springer-Verlag New York Inc

Springer Nature

Lecture Notes in Computer Science 5595 : Theoretical Computer Science and General Issues, 1, 2009

Theoretical Computer Science and General Issues, 1. ed. 2009, Berlin, Heidelberg, 2009

Lecture Notes in Computer Science -- 5595, Berlin, Heidelberg, Germany, 2009

Lecture notes in computer science, 5595, Berlin ; New York, ©2009

Springer Nature, Berlin, Heidelberg, 2009

Germany, Germany

2009, July 2009

2013

Pages in wrong order: paper "The Derivational Complexity Induced by the Dependency Pair Method" at wrong position in document.

Kolxo3 -- 2009 new

sm22676795

{"container_title":"Lecture Notes in Computer Science","edition":"1","isbns":["3642023479","3642023487","9783642023477","9783642023484"],"issns":["0302-9743","1611-3349"],"last_page":404,"publisher":"Springer","series":"Lecture Notes in ... Computer Science and General Issues","volume":"5595"}

MiU

Front Matter....Pages -
Automatic Termination....Pages 1-16
Loops under Strategies....Pages 17-31
Proving Termination of Integer Term Rewriting....Pages 32-47
Dependency Pairs and Polynomial Path Orders....Pages 48-62
Unique Normalization for Shallow TRS....Pages 63-77
The Existential Fragment of the One-Step Parallel Rewriting Theory....Pages 78-92
Proving Confluence of Term Rewriting Systems Automatically....Pages 93-102
A Proof Theoretic Analysis of Intruder Theories....Pages 103-117
Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case....Pages 118-132
Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions....Pages 133-147
YAPA: A Generic Tool for Computing Intruder Knowledge....Pages 148-163
Well-Definedness of Streams by Termination....Pages 164-178
Modularity of Convergence in Infinitary Rewriting....Pages 179-193
A Heterogeneous Pushout Approach to Term-Graph Transformation....Pages 194-208
An Explicit Framework for Interaction Nets....Pages 209-223
Dual Calculus with Inductive and Coinductive Types....Pages 224-238
Comparing Böhm-Like Trees....Pages 239-254
The Derivational Complexity Induced by the Dependency Pair Method....Pages 255-269
Local Termination....Pages 270-284
VMTL–A Modular Termination Laboratory....Pages 285-294
Tyrolean Termination Tool 2....Pages 295-304
From Outermost to Context-Sensitive Rewriting....Pages 305-319
A Fully Abstract Semantics for Constructor Systems....Pages 320-334
The $\Pi^0_2$ -Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity)....Pages 335-349
Unification in the Description Logic $\mathcal{EL}$ ....Pages 350-364
Unification with Singleton Tree Grammars....Pages 365-379
Unification and Narrowing in Maude 2.4....Pages 380-390
Back Matter....Pages -

Constitutes the refereed proceedings of the 20th International Conference on Rewriting Techniques and Applications, RTA 2009, held in Brasilia, Brazil, during June 29 - July 1, 2009. This work covers research on various aspects of rewriting including typical areas of interest such as applications, foundational issues, frameworks and semantics.

Keine Beschreibung vorhanden.
Erscheinungsdatum: 09.06.2009

2009-12-04