hide
Free keywords:
-
Abstract:
Disunification is an extension of unification to first-order formulae over
syntactic equality atoms. Instead of considering only syntactic equality, I
extend a disunification algorithm by Comon and Delor to ultimately periodic
interpretations, i.e.~minimal many-sorted Herbrand models of predicative Horn
clauses and, for some sorts, equations of the form $s^\upmb(x)\eq s^\upma(x)$.
The extended algorithm is terminating and correct for ultimately periodic
interpretations over a finite signature and gives rise to a decision procedure
for the satisfiability of equational formulae in ultimately periodic
interpretations.
As an application, I show how to apply disunification to compute the completion
of predicates with respect to an ultimately periodic interpretation. Such
completions are a key ingredient to several inductionless induction methods.
