Abstract

The topic of this thesis is confluence of first-order term rewriting systems, both its theory and its automation. Term rewrite systems are a model of computation in which terms are successively modified by replacing instances of left-hand sides of equations by the corresponding instance of the right-hand side. Confluence is an important property of rewrite systems which is intimately connected to uniqueness of normal forms, and therefore well-definedness of functions. In the absence of termination, confluence expresses a kind of deterministic behavior: for any two computations starting at the same initial state, it is always possible to continue both of them until they reach a common state again. Like most interesting properties in computer science, confluence is an undecidable property of term rewrite systems. Therefore, determining whether a system is confluent is often challenging. Nevertheless, there are automated confluence provers that attempt to solve this task automatically. The goal of this thesis is to advance the state of the art of the field of automated confluence proving. To this end, we extend the theory of confluence in several areas to obtain confluence criteria that are both powerful and implementable.

BibTeX

@phdthesis{BF15,
  author    = "Bertram Felgenhauer",
  title     = "Confluence for Term Rewriting: Theory and Automation",
  school    = "University of Innsbruck",
  year      = 2015
}