Abstract

This thesis is concerned with investigations into the complexity of term rewriting systems. Moreover the majority of the presented work
deals with the automation of such a complexity analysis.

A term rewrite system is considered of higher complexity, if the number of possible rewrite steps is larger. In line with earlier results
presented in the literature the study is performed as an analysis of termination methods. I.e., instead of directly seeking techniques to
establish the complexity of a given term rewrite system I have studied the complexity induced by termination methods. These
investigations cover well-established termination orders as well as modern (automatable) termination techniques.

BibTeX

@misc{GM09,
  author    = "Georg Moser",
  title     = "Proof Theory at Work: Complexity Analysis of Term Rewrite
               Systems",
  school    = "University of Innsbruck",
  year      = 2009,
  note      = "Habilitation thesis"
}