JAIST Repository
https://dspace.jaist.ac.jp/Title

Equational Reasoning and Completion

Author(s)Klein, Dominik

CitationIssue Date

2012‑06

TypeThesis or Dissertation

Text version

author

URL

http://hdl.handle.net/10119/10560

RightsDescription

Supervisor: Mizuhito Ogawa, 情報科学研究科, 博士

Japan Advanced Institute of Science and Technology

Abstract
Equations are a versatile and natural tool for various reasoning tasks. This thesis investigates how to fully
automate equational reasoning. Central to automation is Knuth and Bendix’ ground-breaking completion
procedure, which searches for a complete term rewriting system (TRS) for a given system of equations. It
was originally formulated as an algorithm, and requires a user-provided reduction order. The choice of thereduction order is non-trivial in general and heavily affects the success of the procedure.
During the early 2000’s, significant progress has been made in automated constraint solving. Very often
it turned out that encoding a problem to boolean constraints and using a SAT solver is more effective thandeveloping a dedicated algorithm. However since the search space for a completion problem is not known inadvance, it is not possible to directly encode it to constraints and benefit from the success of SAT solvers.
We show that completion can be characterized as an optimization problem. Using this formulation, called
Maximal Completion, algorithmic aspects can be abstracted away by encoding the optimization problem toboolean constraints, and employing a MaxSAT solver to find a solution. Full automation of the completion
procedure can then be achieved by constructing a suitable order from the solution of the constraint problem.
The success of Knuth and Bendix’ procedure has led to several adaptations to related reasoning tasks, such
as Inductionless Induction or Rewriting Induction. We propose a new uniform framework based on constrained equalities, which allows to easily express several different joinability requirements that are needed by
the different procedures. Soundness proofs are vastly simplified, since all necessary conditions are encodedin the constraint part. Similar to Maximal Completion, an encoding as an optimization problem over boolean
constraints can be used to automatically find a solution, i.e. a suitable order, for the joinability requirements.
Experiments show that this approach is especially effective for the above mentioned methods for inductive
reasoning.
Lastly we investigate confluence of TRSs. Testing confluence automatically is a central property not only
for completion, but in other applications as well, such as narrowing or type theory. While confluence forterminating TRSs is decidable, finding confluence criteria for non-terminating and non-left-linear TRSs isvery challenging and few criteria exist. Moreover very often these criteria face the issue of computability. We
present a new confluence criterion for non-left-linear and non-terminating TRSs. Since it requires joinability ofuncomputable extended critical pairs, we provide a new result on unification, which enables full automationof our criterion.
All results have been implemented and experimentally evaluated to show their effectiveness. Moreover, weprovide the free completion tool Maxcomp which is based on Maximal Completion.