Skip to main content
SpringerLink
Log in

Solving Graded/Probabilistic Modal Logic via Linear Inequalities (System Description)

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2012)

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

Abstract

We present the experience gained from implementing a new decision procedure for both graded and probabilistic modal logic. While our approach uses standard tableaux for propositional connectives, modal rules are given by linear constraints on the arguments of operators. The implementation uses binary decision diagrams for propositional connectives and a linear programming library for the modal rules. We compare our implementation, for graded modal logic, with other tools, showing average performance. Due to lack of other implementations, no comparison is provided for probabilistic modal logic, the main new feature of our implementation.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baader, F., Nutt, W.: Basic description logics. In: Baader, F., et. al. (ed.) Description Logic Handbook, pp. 43–95. Cambridge University Press (2003)

    Google Scholar 

  2. Bryant, R.E.: Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams. ACM Computing Surveys 24(3), 293–317 (1992)

    Article  Google Scholar 

  3. BuDDy, http://sourceforge.net/projects/buddy/

  4. Calin, G., Myers, R., Pattinson, D., Schröder, L.: COLOSS: The coalgebraic logic satisfiability solver. In: Proc. M4M 5 (2007). ENTCS, vol. 231, pp. 41–54 (2009)

    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. Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled markov processes. Inf. Comput. 179(2), 163–193 (2002)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  8. Farsiniamarj, N., Haarslev, V.: Practical reasoning with qualified number restrictions: a hybrid Abox calculus for the description logic SHQ. AI Comms. 23(2–3), 205–240 (2010)

    MathSciNet  MATH  Google Scholar 

  9. Fine, K.: In so many possible worlds. Notre Dame J. Formal Logic 13, 516–520 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  10. GNU linear programming kit (glpk), http://www.gnu.org/s/glpk/

  11. Haarslev, V., Möller, R.: RACER System Description. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 701–705. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  12. Haarslev, V., Sebastiani, R., Vescovi, M.: Automated Reasoning in \(\mathcal{ALCQ}\) via SMT. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 283–298. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Klinov, P.: Practical Reasoning in Probabilistic Description Logic. PhD thesis, University of Manchester, Manchester, UK (2011)

    Google Scholar 

  15. Kupke, C., Pattinson, D.: On modal logics of linear inequalities. In: Goranko, V., Shehtman, V. (eds.) Proc. AiML 2010. College Publications (2010)

    Google Scholar 

  16. Motik, B., Shearer, R., Horrocks, I.: Hypertableau Reasoning for Description Logics. Journal of Artificial Intelligence Research 36, 165–228 (2009)

    MathSciNet  MATH  Google Scholar 

  17. Parma, A., Segala, R.: Logical Characterizations of Bisimulations for Discrete Probabilistic Systems. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 287–301. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Schrijver, A.: Theory of linear and integer programming. Wiley Interscience (1986)

    Google Scholar 

  19. Schröder, L., Pattinson, D.: PSPACE bounds for rank-1 modal logics. ACM Transactions on Computational Logics 10(2) (2009)

    Google Scholar 

  20. Sirin, E., Parsia, B., Cuenca Grau, B., Kalyanpur, A., Katz, Y.: Pellet: A practical OWL-DL reasoner. Journal of Web Semantics (2006)

    Google Scholar 

  21. Tsarkov, D., Horrocks, I.: FaCT++ Description Logic Reasoner: System Description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 292–297. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computing, Imperial College, London, UK

    William Snell, Dirk Pattinson & Florian Widmann

Authors
  1. William Snell
    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. Florian Widmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, One Microsoft Way, 98052-6399, Redmond, WA, USA

    Nikolaj Bjørner

  2. School of computer Science, University of Manchester, Kilburn Building, Oxford Road, MP13 9PL, Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Snell, W., Pattinson, D., Widmann, F. (2012). Solving Graded/Probabilistic Modal Logic via Linear Inequalities (System Description). In: Bjørner, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2012. Lecture Notes in Computer Science, vol 7180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28717-6_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-28717-6_30

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-28716-9

  • Online ISBN: 978-3-642-28717-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation