Abstract

Automated reasoning gained considerable interest over the last two decades and has by now a variety of applications in formal methods of computer science, such as formal specification of software and hardware systems or verification of cryptographic protocols. Automated reasoning systems are also used in mathematical research, where mathematical software provides proof assistance using automated reasoning techniques. Computing systems in automated reasoning are often based on decision calculi which require a well-founded term ordering as input. Such a term ordering is always critical for success, but an appropriate choice is hard to determine in advance. For standard Knuth-Bendix completion, different approaches to automate this choice were proposed by exploiting recent progress in research on automatic termination proving techniques on one hand, and satisfiability checking on the other hand. Since modern termination tools employ far more sophisticated techniques than classical term orderings, this approach contributes to more flexible and powerful automated reasoning and theorem proving technology. Automation techniques relying on satisfiability checkers allow for efficient implementations. This thesis explores the use of these approaches in different deduction calculi of equational reasoning. Besides standard Knuth-Bendix completion also ordered completion, normalized completion and rewriting induction are considered.

BibTeX

@phdthesis{SW13,
  author    = "Sarah Winkler",
  title     = "Termination Tools in Automated Reasoning",
  school    = "University of Innsbruck",
  year      = 2013
}