Disunification for Ultimately Periodic Interpretations

  • Matthias Horbach
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


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.


Normal Form Function Symbol Horn Clause Equational Formula Periodic Decomposition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, ch. 8, pp. 445–532. Elsevier and MIT Press (2001)Google Scholar
  2. 2.
    Bachmair, L., Plaisted, D.A.: Associative path orderings. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 241–254. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  3. 3.
    Caferra, R., Zabel, N.: A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation 13(6), 613–642 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293–322. Plenum Press, New York (1977)Google Scholar
  5. 5.
    Colmerauer, A.: Equations and inequations on finite and infinite trees. In: FGCS, vol. 5, pp. 85–99 (1984)Google Scholar
  6. 6.
    Comon, H.: Unification et Disunification: Théorie et applications. PhD thesis, Institut National Polytechnique de Grenoble (July 1988)Google Scholar
  7. 7.
    Comon, H.: Disunification: A survey. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 322–359. MIT Press, Cambridge (1991)Google Scholar
  8. 8.
    Comon, H., Delor, C.: Equational formulae with membership constraints. Information and Computation 112(2), 167–216 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation 7(3-4), 371–425 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Comon, H., Nieuwenhuis, R.: Induction = I-axiomatization + first-order consistency. Information and Computation 159(1/2), 151–186 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science 17, 279–301 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Fermüller, C.G., Leitsch, A.: Hyperresolution and automated model building. Journal of Logic and Computation 6(2), 173–203 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Fernández, M.: Narrowing based procedures for equational disunification. Applicable Algebra in Engineering, Communication and Computing 3, 1–26 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Horbach, M., Weidenbach, C.: Decidability results for saturation-based model building. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 404–420. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  15. 15.
    Horbach, M., Weidenbach, C.: Deciding the inductive validity of ∀ ∃ * queries. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 332–347. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. 16.
    Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: A rule-based survey of unification. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic - Essays in Honor of Alan Robinson, pp. 257–321. MIT Press, Cambridge (1991)Google Scholar
  17. 17.
    Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Lassez, J.-L., Maher, M.J., Marriott, K.: Unification revisited. In: Boscarol, M., Levi, G., Aiello, L.C. (eds.) Foundations of Logic and Functional Programming. LNCS, vol. 306, pp. 67–113. Springer, Heidelberg (1988)CrossRefGoogle Scholar
  19. 19.
    Ludwig, M., Hustadt, U.: Resolution-based model construction for PLTL. In: Lutz, C., Raskin, J.-F. (eds.) TIME, pp. 73–80. IEEE Computer Society, Los Alamitos (2009)Google Scholar
  20. 20.
    Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: LICS, pp. 348–357. IEEE Computer Society, Los Alamitos (1988)Google Scholar
  21. 21.
    Mal’cev, A.I.: Axiomatizable classes of locally free algebra of various type. In: Wells, B.F. (ed.) The Metamathematics of Algebraic Systems: Collected Papers 1936–1967, ch. 23, pp. 262–281. North Holland, Amsterdam (1971)Google Scholar
  22. 22.
    Plotkin, G.: Building in equational theories. In: Meltzer, B.N., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 73–90. Edinburgh University Press (1972)Google Scholar
  23. 23.
    Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23–41 (1965)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Sutcliffe, G.: The TPTP problem library and associated infrastructure. Journal of Automomated Reasoning 43(4), 337–362 (2009)CrossRefzbMATHGoogle Scholar
  25. 25.
    Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) Automated Deduction – CADE-22. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Matthias Horbach
    • 1
    • 2
  1. 1.Max-Planck-Institut für InformatikSaarbrückenGermany
  2. 2.Saarland UniversitySaarbrückenGermany

Personalised recommendations