ISR 2010

ISR 2010
introduction literature schedule tools

Introduction in Term Rewriting  –  Further Reading

Day 1

Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
Gérard Huet
Journal of the ACM 27(4), pp. 797 – 821, 1980
Proving Termination with Multiset Orderings
Nachum Dershowitz and Zohar Manna
Communications of the ACM 22(8), pp. 465 – 476, 1979
Confluence by Decreasing Diagrams
Vincent van Oostrom
Theoretical Computer Science 126(2), pp. 259 – 280, 1994
On the Uniform Halting Problem for Term Rewriting Systems
Gérard Huet and Dallas Lankford
technical report 283, INRIA, 1978
Termination of Linear Rewriting Systems (Preliminary Version)
Nachum Dershowitz
Proceedings of the 8th International Colloquium on Automata, Languages and Programming (ICALP 1981), pp. 448 –458, 1981
Fast Congruence Closure and Extensions
Robert Nieuwenhuis and Albert Oliveras
Information and Computation 205(4), pp. 557 –580, 2007

Day 2

Termination of Term Rewriting: Interpretation and Type Elimination
Hans Zantema
Journal of Symbolic Computation 17(1), pp. 23 – 50, 1994
Mechanically Proving Termination Using Polynomial Interpretations
Evelyne Contejean, Claude Marché, Ana Paula Tomás, and Xavier Urbain
Journal of Automated Reasoning 34(4), pp. 325 – 363, 2006
Orderings for Term-Rewriting Systems
Nachum Dershowitz
Theoretical Computer Science 17(3), pp. 279 – 301, 1982
Simple Word Problems in Universal Algebras
Donald E. Knuth and Peter Bendix
in: Computational Problems in Abstract Algebra, Pergamon Press, pp. 263 – 297, 1970

Day 3

Canonical Equational Proofs
Leo Bachmair
Progress in Theoretical Computer Science, Birkhäuser, 1991
Equational Inference, Canonical Proofs, and Proof Orderings
Leo Bachmair and Nachum Dershowitz
Journal of the ACM 41(2), pp. 236– 276, 1994
KBO Orientability
Harald Zankl, Nao Hirokawa and Aart Middeldorp
Journal of Automated Reasoning 43(2), pp. 173 – 201, 2009
Termination of Term Rewriting using Dependency Pairs
Thomas Arts and Jürgen Giesl
Theoretical Computer Science 236(1,2), pp. 133 – 178, 2000

Day 4

Developing Developments
Vincent van Oostrom
Theoretical Computer Science 175(1), pp. 159 – 181, 1997
Modular Termination of r-Consistent and Left-Linear Term Rewriting Systems
Manfred Schmidt-Schauß, Massimo Marchiori, and Sven Eric Panitz
Theoretical Computer Science 149(2), pp. 361 – 374, 1995
Modularity of Confluence – Constructed
Vincent van Oostrom
Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), LNAI 5195, pp. 348 – 363, 2008
Just-in-Time: On Strategy Annotations
Jaco van de Pol
Proceedings of the 1st International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2001), Electronic Notes in Theoretical Computer Science 57, pp. 41–63, 2001
A Sequential Reduction Strategy
Sergio Antoy and Aart Middeldorp
Theoretical Computer Science 165(1), pp. 75 – 95, 1996

Day 5

Matrix Interpretations for Proving Termination of Term Rewriting
Jörg Endrullis, Johannes Waldmann and Hans Zantema
Journal of Automated Reasoning 40(2,3), pp. 195 – 220, 2008
Mechanizing and Improving Dependency Pairs
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp and Stephan Falke
Journal of Automated Reasoning 37(3), pp. 155 – 203, 2006
Tyrolean Termination Tool: Techniques and Features
Nao Hirokawa and Aart Middeldorp
Information and Computation 205(4), pp. 474 – 511, 2007
Termination of Term Rewriting by Semantic Labelling
Hans Zantema
Fundamenta Informatica (1,2), pp. 89 – 105, 1995
Root-Labeling
Christian Sternagel and Aart Middeldorp
Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), LNCS 5117, pp. 336 – 350, 2008
Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations
Georg Moser, Andreas Schnabl and Johannes Waldmann
Proceedings of the 28th Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), Leibniz International Proceedings in Informatics 2, pp. 304 – 315, 2008