# Item

ITEM ACTIONSEXPORT

Released

Journal Article

#### Superposition for Fixed Domains

##### Locator

There are no locators available

##### Fulltext (public)

There are no public fulltexts available

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Horbach, M., & Weidenbach, C. (2010). Superposition for Fixed Domains.*
ACM Transactions on Computational Logic,* *11*(4): 27, pp. 27,1-27,35. doi:10.1145/1805950.1805957.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-14C3-6

##### 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.