Theorems used by Jambox

Matrix Interpretations

• Dieter Hofbauer and Johannes Waldmann
  Proving Termination with Matrix Interpretations
  RTA 2006, LNCS, to appear
  
  
• Jörg Endrullis, Johannes Waldmann and Hans Zantema
  Matrix Interpretations for Proving Termination of Term Rewriting
  • Theorem 2
  IJCAR 2006, to appear.
  
  

Match-bounds and RFC-match-bounds

• Alfons Geser, Dieter Hofbauer and Johannes Waldmann
  Match bounded string rewriting systems
  • Theorem 6
  Applicable Algebra in Engineering, Communication and Computing 15(3-4):149-171, 2004.
  
  
• Alfons Geser, Dieter Hofbauer, Johannes Waldmann and Hans Zantema
  Finding finite automata that certify termination of string rewriting systems
  • Theorem 2
  International Journal of Foundations of Computer Science 16(3):471-486, 2005.
  
  

Dependency Pairs Transformation and Subterm Criterion

• Jürgen Giesl, René Thiemann and Peter Schneider-Kamp
  Proving and Disproving Termination of Higher-Order Functions
  
  • Definition 12 (Improved Estimated Dependency Graph)
  In Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS '05), Vienna, Austria,
  Lecture Notes in Artificial Intelligence 3717, pages 216-231, Springer-Verlag, 2005.
  
  
• Nao Hirokawa and Aart Middeldorp
  Dependency Pairs Revisited
  
  • Theorem 11 (Subterm Criterion)
  Proceedings of the 15th International Conference on Rewriting Techniques and Applications, Aachen,
  Lecture Notes in Computer Science 3091, pp. 249-268, 2004.
  
  
• Nao Hirokawa and Aart Middeldorp
  Automating the Dependency Pair Method
  
  • Corollary 18 (Recursive SCC Algorithm)
  Information and Computation 199(1,2), pp. 172-199, 2005.
  
  
• Jürgen Giesl, René Thiemann and Peter Schneider-Kamp
  The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs
  In Proceedings of the 11th International Conference on Logic for Programming,
  Artificial Intelligence, and Reasoning (LPAR 2004), Montevideo, Uruguay,
  Lecture Notes in Artificial Intelligence 3452, pages 301-331, Springer-Verlag, 2005.
  
  

Self-Labeling/ Removing Self-Labeling and
Semantic Labeling/ Removing Semantic Labeling

• Hans Zantema
  Termination of Term Rewriting by Semantic Labelling
  • Theorem 4 ('if' of labeling, 'only if' for removing the labeling)
  Fundamenta Informaticae, 1995, volume 24, pages 89-105
  
  
• Aart Middeldorp, Hitoshi Ohsaki and Hans Zantema
  Transforming Termination by Self-Labelling
  Proceedings of the 13th International Conference on Automated Deduction, New Brunswick,
  Lecture Notes in Artificial Intelligence 1104, pp. 373-387, 1996.
  
  

Applicative Transformation

• Nao Hirokawa and Aart Middeldorp
  Uncurrying for Termination
  
  • Theorem 14
  HOR 2006, to appear
  
  

Reducing Right-Hand Sides

• Hans Zantema
  Reducing Right-Hand Sides for Termination
  • Theorem 4
  Processes, Terms and Cycles: Steps on the Road to Infinity:
  Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday, 2005,
  editors: A. Middeldorp, V. van Oostrom, F. van Raamsdonk, R. de Vrijer,
  Springer Lecture Notes in Computer Science, volume 3838, pages 173 - 197.
  
  

Reverse

• A SRS R is terminating if and only if R^rev is terminating.
  Where R^rev = {(l^rev -> r^rev)  |  (l -> r) in R}.
  
  

Strip First/Last Symbol

• Let R' be a SRS obtained from R by replacing rules of the form
    (al -> ar) by (l -> r) (strip first symbol) or
    (la -> ra) by (l -> r) (strip last symbol)
  then termination of R' implies termination of R.
  
  

Loop

• Let R be a SRS. If there exists a derivation u -> lur, then R is non-terminating.