Abstract

This thesis contains selected contributions investigating various aspects regarding the automated analysis of rewrite systems. The main topics of confluence, complexity, termination, and automation itself are addressed.

For confluence and complexity analysis, frameworks are presented that admit the combination of different methods, resulting in significant gains in power. Termination criteria whose automation has been open for many years (interpretations using ordinals or exponentiation functions) are considered as well as the uncurrying transformation, which improves the power of first-order termination tools for applicative systems. Since verification is an essential part of automation we discuss our formalization of the decreasing diagrams method in the interactive theorem prover Isabelle. To highlight the results of successful automation efforts we present the tools CSI and KBCV.

BibTeX

@misc{HZ14,
  author    = "Harald Zankl",
  title     = "Challenges in Automation of Rewriting",
  school    = "University of Innsbruck",
  year      = 2014,
  note      = "Habilitation thesis"
}