Contact Logic is Finitary for Unification with Constants

Conference paper
Part of the Logic in Asia: Studia Logica Library book series (LIAA)


Contact Logic is a formalism for reasoning about the relation of contact between regions. We introduce a new inference problem for Contact Logic, the unification problem, which extends the validity problem by allowing one to replace variables by terms before testing for validity. Our main result is the proof that unification with constants in Contact Logic is finitary.


Contact Logic Unification with constants Unification type 



Special acknowledgement is heartily granted to Tinko Tinchev (Sofia University, Bulgaria) for his valuable remarks. We also make a point of thanking the referees for their feedback: their helpful comments and their useful suggestions have been essential for improving the correctness and the readability of a preliminary version of this paper.


  1. Baader, F. 1998. On the complexity of Boolean unification. Information Processing Letters 67: 215–220.CrossRefGoogle Scholar
  2. Baader, F., S. Borgwardt, and B. Morawska. 2012. Extending unification in \(\cal{EL}\) towards general TBoxes. In Principles of Knowledge Representation and Reasoning, 568–572. AAAI Press.Google Scholar
  3. Baader, F., and S. Ghilardi. 2011. Unification in modal and description logics. Logic Journal of the IGPL 19: 705–730.CrossRefGoogle Scholar
  4. Baader, F., and B. Morawska. 2009. Unification in the description logic \(\cal{EL}\). In Rewriting Techniques and Applications, ed. R. Treinen, 350–364. Berlin: SpringerGoogle Scholar
  5. Balbiani, P., and Ç. Gencer. 2015. Admissibility and unifiability in contact logics. In Logic, Language, and Computation, 44–60. Berlin: SpringerCrossRefGoogle Scholar
  6. Balbiani, P., and Ç. Gencer. 2017. \(KD\) is nullary. Journal of Applied Non-Classical Logics 27: 196–205.CrossRefGoogle Scholar
  7. Balbiani, P., T. Tinchev, and D. Vakarelov. 2007. Modal logics for region-based theories of space. Fundamenta Informaticæ 81: 29–82.Google Scholar
  8. Cohn, A., and J. Renz. 2008. Qualitative spatial representation and reasoning. In Handbook of Knowledge Representation, 551–596. Elsevier.Google Scholar
  9. Dimov, G., and D. Vakarelov. 2006a. Contact algebras and region-based theory of space: a proximity approach—I. Fundamenta Informaticæ 74: 209–249.Google Scholar
  10. Dimov, G., and D. Vakarelov. 2006b. Contact algebras and region-based theory of space: proximity approach—II. Fundamenta Informaticæ 74: 251–282.Google Scholar
  11. Düntsch, I., and M. Winter. 2005. A representation theorem for Boolean contact algebras. Theoretical Computer Science 347: 498–512.CrossRefGoogle Scholar
  12. Dzik, W.: Unification Types in Logic. Wydawnicto Uniwersytetu Slaskiego (2007).Google Scholar
  13. Galton, A. 2000. Qualitative Spatial Change. Oxford University Press.Google Scholar
  14. Gencer, Ç. 2002. Description of modal logics inheriting admissible rules for \(K4\). Logic Journal of the IGPL 10: 401–411.Google Scholar
  15. Gencer, Ç., and D. de Jongh. 2009. Unifiability in extensions of \(K4\). Logic Journal of the IGPL 17: 159–172.Google Scholar
  16. Ghilardi, S. 2000. Best solving modal equations. Annals of Pure and Applied Logic 102: 183–198.CrossRefGoogle Scholar
  17. Ghilardi, S., and L. Sacchetti. 2004. Filtering unification and most general unifiers in modal logic. The Journal of Symbolic Logic 69: 879–906.CrossRefGoogle Scholar
  18. Jer̆ábek, E. 2015. Blending margins: the modal logic \(K\) has nullary unification type. Journal of Logic and Computation 25: 1231–1240.Google Scholar
  19. Kontchakov, R., Y. Nenov, I. Pratt-Hartmann, and M. Zakharyaschev. 2013. Topological logics with connectedness over Euclidean spaces. ACM Transactions on Computational Logic 14. Scholar
  20. Kontchakov, R., I. Pratt-Hartmann, F. Wolter, and M. Zakharyaschev. 2010a. Spatial logics with connectedness predicates. Logical Methods in Computer Science 6: 1–43.Google Scholar
  21. Kontchakov, R., I. Pratt-Hartmann, and M. Zakharyaschev. 2010b. Interpreting topological logics over Euclidean spaces. In Proceedings of the Twelfth International Conference on the Principles of Knowledge Representation and Reasoning, 534–544. AAAI Press.Google Scholar
  22. Renz, J. 2002. Qualitative Spatial Reasoning with Topological Information. Berlin: Springer.CrossRefGoogle Scholar
  23. Rybakov, V. 1997. Admissibility of Logical Inference Rules. Elsevier.Google Scholar
  24. Tinchev, T., and D. Vakarelov. 2010. Logics of space with connectedness predicates: complete axiomatizations. In Advances in Modal Logic, 434–453. College Publications.Google Scholar
  25. Vakarelov, D. 2007. Region-based theory of space: algebras of regions, representation theory, and logics. In Mathematical Problems from Applied Logic. Logics for the XXIst Century. II, 267–348. Berlin: Springer.Google Scholar
  26. Wolter, F., and M. Zakharyaschev. 2000. Spatio-temporal representation and reasoning based on \(RCC\)-\(8\). In Proceedings of the Seventh International Conference on Principles of Knowledge Representation and Reasoning, 3–14. Morgan Kaufmann.Google Scholar

Copyright information

© Springer Nature Singapore Pte Ltd. 2020

Authors and Affiliations

  1. 1.Institut de recherche en informatique de ToulouseCNRS—Toulouse UniversityToulouseFrance
  2. 2.Faculty of Engineering and Natural SciencesSabancı UniversityIstanbulTurkey
  3. 3.Faculty of Arts and SciencesAydın UniversityIstanbulTurkey

Personalised recommendations