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

lgli/rewriting-techniques-and-applications-proceedings-20th-international-conference-rta-2009-brasilia-brazil-20090629.pdf

lgrsnf/rewriting-techniques-and-applications-proceedings-20th-international-conference-rta-2009-brasilia-brazil-20090629.pdf

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

zlib/Computers/Networking/Ralf Treinen/Rewriting Techniques and Applications: 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009 Proceedings_1312332.pdf

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

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

Steinkopff. in Springer-Verlag GmbH

Springer-Verlag New York Inc

Springer Nature

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

Correct order of pages, correct bookmarks, cover, pagination

0

lg870273

{"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

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

2012-12-12