Advertisement
Published in:
2010 | OriginalPaper | Chapter
Disunification for Ultimately Periodic Interpretations
Author : Matthias Horbach
Published in: Logic for Programming, Artificial Intelligence, and Reasoning
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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
l
(
x
) ≃
s
k
(
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.