Disunification for Ultimately Periodic Interpretations

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 sl (x) sk (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.

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Matthias Horbach
• Keywords: Automated Reasoning, LPAR 2010, Periodic Interpretation, Syntactic Equality, Syntactic Equality Atoms