Contact Logic is Finitary for Unification with Constants

  • Conference paper
  • First Online:
Nonclassical Logics and Their Applications

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

  • 142 Accesses

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 85.59
Price includes VAT (France)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 105.49
Price includes VAT (France)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info
Hardcover Book
EUR 147.69
Price includes VAT (France)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  • Baader, F. 1998. On the complexity of Boolean unification. Information Processing Letters 67: 215–220.

    Article  Google Scholar 

  • 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 

  • Baader, F., and S. Ghilardi. 2011. Unification in modal and description logics. Logic Journal of the IGPL 19: 705–730.

    Article  Google Scholar 

  • Baader, F., and B. Morawska. 2009. Unification in the description logic \(\cal{EL}\). In Rewriting Techniques and Applications, ed. R. Treinen, 350–364. Berlin: Springer

    Google Scholar 

  • Balbiani, P., and Ç. Gencer. 2015. Admissibility and unifiability in contact logics. In Logic, Language, and Computation, 44–60. Berlin: Springer

    Chapter  Google Scholar 

  • Balbiani, P., and Ç. Gencer. 2017. \(KD\) is nullary. Journal of Applied Non-Classical Logics 27: 196–205.

    Article  Google Scholar 

  • Balbiani, P., T. Tinchev, and D. Vakarelov. 2007. Modal logics for region-based theories of space. Fundamenta Informaticæ 81: 29–82.

    Google Scholar 

  • Cohn, A., and J. Renz. 2008. Qualitative spatial representation and reasoning. In Handbook of Knowledge Representation, 551–596. Elsevier.

    Google Scholar 

  • 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 

  • Dimov, G., and D. Vakarelov. 2006b. Contact algebras and region-based theory of space: proximity approach—II. Fundamenta Informaticæ 74: 251–282.

    Google Scholar 

  • Düntsch, I., and M. Winter. 2005. A representation theorem for Boolean contact algebras. Theoretical Computer Science 347: 498–512.

    Article  Google Scholar 

  • Dzik, W.: Unification Types in Logic. Wydawnicto Uniwersytetu Slaskiego (2007).

    Google Scholar 

  • Galton, A. 2000. Qualitative Spatial Change. Oxford University Press.

    Google Scholar 

  • Gencer, Ç. 2002. Description of modal logics inheriting admissible rules for \(K4\). Logic Journal of the IGPL 10: 401–411.

    Google Scholar 

  • Gencer, Ç., and D. de Jongh. 2009. Unifiability in extensions of \(K4\). Logic Journal of the IGPL 17: 159–172.

    Google Scholar 

  • Ghilardi, S. 2000. Best solving modal equations. Annals of Pure and Applied Logic 102: 183–198.

    Article  Google Scholar 

  • Ghilardi, S., and L. Sacchetti. 2004. Filtering unification and most general unifiers in modal logic. The Journal of Symbolic Logic 69: 879–906.

    Article  Google Scholar 

  • Jer̆ábek, E. 2015. Blending margins: the modal logic \(K\) has nullary unification type. Journal of Logic and Computation 25: 1231–1240.

    Google Scholar 

  • Kontchakov, R., Y. Nenov, I. Pratt-Hartmann, and M. Zakharyaschev. 2013. Topological logics with connectedness over Euclidean spaces. ACM Transactions on Computational Logic 14. https://doi.org/10.1145/2480759.2480765.

    Article  Google Scholar 

  • 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 

  • 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 

  • Renz, J. 2002. Qualitative Spatial Reasoning with Topological Information. Berlin: Springer.

    Book  Google Scholar 

  • Rybakov, V. 1997. Admissibility of Logical Inference Rules. Elsevier.

    Google Scholar 

  • 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 

  • 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 

  • 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 

Download references

Acknowledgements

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.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Philippe Balbiani .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Singapore Pte Ltd.

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Balbiani, P., Gencer, Ç. (2020). Contact Logic is Finitary for Unification with Constants. In: Ju, S., Palmigiano, A., Ma, M. (eds) Nonclassical Logics and Their Applications. Logic in Asia: Studia Logica Library. Springer, Singapore. https://doi.org/10.1007/978-981-15-1342-8_4

Download citation

Publish with us

Policies and ethics

Navigation