Abstract

This thesis is devoted to the mechanized confluence analysis of rewrite systems. Rewrite systems consist of directed equations and computation is performed by successively replacing instances of left-hand sides of equations by the corresponding instance of the right-hand side. Confluence is a fundamental property of rewrite systems, which ensures that different computation paths produce the same result. Since rewriting is Turing-complete, confluence is undecidable in general. Nevertheless, techniques have been developed that can be used to determine confluence for many rewrite systems and several automatic confluence provers are under active development. Our goal is to improve three aspects of automatic confluence analysis, namely (a) reliability, (b) power, and© versatility. The importance of these aspects is witnessed by the annual international confluence competition, where the leading automated tools analyze confluence of rewrite systems. To improve the reliability of automatic confluence analysis, we formalize confluence criteria for rewriting in the proof assistant Isabelle/HOL, resulting in a verified, executable checker for confluence proofs. To enhance the power of confluence tools, we present a remarkably simple technique, based on the addition and removal of redundant equations, that strengthens existing techniques. To make automatic confluence analysis more versatile, we develop a higher-order confluence tool, making automatic confluence analysis applicable to systems with functional and bound variables.

BibTeX

@phdthesis{JN17,
  author    = "Julian Nagele",
  title     = "Mechanizing Confluence: Automated and Certified Analysis of
               First- and Higher-Order Rewrite Systems",
  school    = "University of Innsbruck",
  year      = 2017
}