User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Journal Article

Superposition for Fixed Domains


Horbach,  Matthias
Automation of Logic, MPI for Informatics, Max Planck Society;


Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

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