Skip to main content
SpringerLink
Log in

Reasoning with Global Assumptions in Arithmetic Modal Logics

  • Conference paper
  • First Online:
Fundamentals of Computation Theory (FCT 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9210))

Included in the following conference series:

Abstract

We establish a generic upper bound \(\textsc {ExpTime} \) for reasoning with global assumptions in coalgebraic modal logics. Unlike earlier results of this kind, we do not require a tractable set of tableau rules for the instance logics, so that the result applies to wider classes of logics. Examples are Presburger modal logic, which extends graded modal logic with linear inequalities over numbers of successors, and probabilistic modal logic with polynomial inequalities over probabilities. We establish the theoretical upper bound using a type elimination algorithm. We also provide a global caching algorithm that offers potential for practical reasoning.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  2. Baader, F., Sattler, U.: Description logics with symbolic number restrictions. In: European Conference on Artificial Intelligence, ECAI 1996, pp. 283–287. Wiley (1996)

    Google Scholar 

  3. Bárcenas, E., Lavalle, J.: Expressive reasoning on tree structures: recursion, inverse programs, presburger constraints and nominals. In: Castro, F., Gelbukh, A., González, M. (eds.) MICAI 2013, Part I. LNCS, vol. 8265, pp. 80–91. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  4. Canny, J.: Some algebraic and geometric computations in PSPACE. In: Symposium on Theory of Computing, STOC 1988, pp. 460–467. ACM (1988)

    Google Scholar 

  5. D’Agostino, G., Visser, A.: Finality regained: A coalgebraic study of Scott-sets and multisets. Arch. Math. Logic 41, 267–298 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  6. Demri, S., Lugiez, D.: Presburger modal logic is PSPACE-complete. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 541–556. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Demri, S., Lugiez, D.: Complexity of modal logics with Presburger constraints. J. Appl. Logic 8, 233–252 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  8. Eisenbrand, F., Shmonin, G.: Carathéodory bounds for integer cones. Oper. Res. Lett. 34(5), 564–568 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  9. Elgesem, D.: The modal logic of agency. Nordic J. Philos. Logic 2, 1–46 (1997)

    MathSciNet  MATH  Google Scholar 

  10. Fagin, R., Halpern, J.: Reasoning about knowledge and probability. J. ACM 41, 340–367 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  11. Fagin, R., Halpern, J., Megiddo, N.: A logic for reasoning about probabilities. Inform. Comput. 87, 78–128 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  12. Fine, K.: In so many possible worlds. Notre Dame J. Form. Log. 13, 516–520 (1972)

    Article  MATH  Google Scholar 

  13. Goranko, V., Passy, S.: Using the universal modality: Gains and questions. J. Log. Comput. 2, 5–30 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  14. Goré, R., Kupke, C., Pattinson, D.: Optimal tableau algorithms for coalgebraic logics. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 114–128. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Goré, R., Nguyen, L.: EXPTIME tableaux for ALC using sound global caching. In: Description Logics, DL 2007, CEUR Workshop Proceedings, vol. 250 (2007)

    Google Scholar 

  16. Goré, R.P., Postniece, L.: An experimental evaluation of global caching for \(\cal {ALC}\) (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 299–305. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Heifetz, A., Mongin, P.: Probabilistic logic for type spaces. Games Econ. Behav. 35, 31–53 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  18. Kupke, C., Pattinson, D.: On modal logics of linear inequalities. In: Advances in Modal Logic, AiML 2010, pp. 235–255. College Publications (2010)

    Google Scholar 

  19. Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  20. Lutz, C., Schröder, L.: Probabilistic description logics for subjective uncertainty. In: Principles of Knowledge Representation and Reasoning, KR 2010, pp. 393–403. AAAI (2010)

    Google Scholar 

  21. Myers, R., Pattinson, D., Schröder, L.: Coalgebraic hybrid logic. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 137–151. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  22. Pacuit, E., Salame, S.: Majority logic. In: Principles of Knowledge Representation and Reasoning, KR 2004, pp. 598–605. AAAI Press (2004)

    Google Scholar 

  23. Papadimitriou, C.: On the complexity of integer programming. J. ACM 28, 765–768 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  24. Pratt, V.: Models of program logics. In: Foundations of Computer Science, FOCS 1979, pp. 115–122. IEEE Comp. Soc. (1979)

    Google Scholar 

  25. Schröder, L.: A finite model construction for coalgebraic modal logic. J. Log. Algebr. Prog. 73, 97–110 (2007)

    Article  MATH  Google Scholar 

  26. Schröder, L., Pattinson, D.: Shallow models for non-iterative modal logics. In: Dengel, A.R., Berns, K., Breuel, T.M., Bomarius, F., Roth-Berghofer, T.R. (eds.) KI 2008. LNCS (LNAI), vol. 5243, pp. 324–331. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  27. Schröder, L., Pattinson, D.: PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log. 10,13:1–13:33 (2009)

    Google Scholar 

  28. Schröder, L., Pattinson, D.: Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra. Math. Struct. Comput. Sci. 21, 235–266 (2011)

    Article  MATH  Google Scholar 

  29. Schröder, L., Pattinson, D., Kupke, C.: Nominals for everyone. In: International Joint Conference on Artificial Intelligence, IJCAI 2009, pp. 917–922 (2009)

    Google Scholar 

  30. Seidl, H., Schwentick, T., Muscholl, A.: Counting in trees. In: Logic and Automata: History and Perspectives (in Honor of Wolfgang Thomas), pp. 575–612. Amsterdam Univ. Press (2008)

    Google Scholar 

  31. Tobies, S.: Complexity results and practical algorithms for logics in knowledge representation. Ph.D. thesis, RWTH Aachen (2001)

    Google Scholar 

Download references

Acknowledgements

We wish to thank Erwin R. Catesbeiana for remarks on unsatisfiability. Work of the first author forms part of the DFG project GenMod2 (SCHR 1118/5-2).

Author information

Authors and Affiliations

  1. University of Strathclyde, Glasgow, UK

    Clemens Kupke

  2. Australian National University, Canberra, Australia

    Dirk Pattinson

  3. Friedrich-Alexander Universität Erlangen-Nürnberg, Erlangen, Germany

    Lutz Schröder

Authors
  1. Clemens Kupke
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dirk Pattinson
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lutz Schröder
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lutz Schröder .

Editor information

Editors and Affiliations

  1. Université Paris Diderot, Paris, France

    Adrian Kosowski

  2. Université Bordeaux 1, Talence, France

    Igor Walukiewicz

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Kupke, C., Pattinson, D., Schröder, L. (2015). Reasoning with Global Assumptions in Arithmetic Modal Logics. In: Kosowski, A., Walukiewicz, I. (eds) Fundamentals of Computation Theory. FCT 2015. Lecture Notes in Computer Science(), vol 9210. Springer, Cham. https://doi.org/10.1007/978-3-319-22177-9_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-22177-9_28

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-22176-2

  • Online ISBN: 978-3-319-22177-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation