Skip to main content
SpringerLink
Log in
Book cover

International Joint Conference on Automated Reasoning

IJCAR 2014: Automated Reasoning pp 381–395Cite as

Terminating Minimal Model Generation Procedures for Propositional Modal Logics

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 8562))

Abstract

Model generation and minimal model generation are useful for tasks such as model checking and for debugging of logical specifications. This paper presents terminating procedures for the generation of models minimal modulo subset-simulation for the modal logic K and all combinations of extensions with the axioms T, B, D, 4 and 5. Our procedures are minimal model sound and complete. Compared with other minimal model generation procedures, they are designed to have smaller search space and return fewer models. In order to make the models more effective for users, our minimal model criterion is aimed to be semantically meaningful, intuitive and contain a minimal amount of information. Depending on the logic, termination is ensured by a variation of equality blocking.

The first author is supported by an EPSRC EU Doctoral Training Award. The research was partially supported by EPSRC research grant EP/H043748/1.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baumgartner, P., Fürbach, U., Niemelä, I.: Hyper tableaux. In: Orłowska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS, vol. 1126, pp. 1–17. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  2. Bry, F., Yahya, A.: Positive unit hyperresolution tableaux and their application to minimal model generation. J. Automat. Reason. 25(1), 35–82 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  3. Cialdea Mayer, M.: A proof procedure for hybrid logic with binders, transitivity and relation hierarchies. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 76–90. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  4. Clarke, E.M., Schlingloff, B.: Model checking. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1635–1790. Elsevier (2001)

    Google Scholar 

  5. Denecker, M., De Schreye, D.: On the duality of abduction and model generation in a framework for model generation with equality. Theoret. Computer Sci. 122(1&2), 225–262 (1994)

    Article  MATH  Google Scholar 

  6. Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. FCS-36, pp. 453–462. IEEE Comput. Soc. (1995)

    Google Scholar 

  7. Hintikka, J.: Model minimization—An alternative to circumscription. J. Automat. Reason. 4(1), 1–13 (1988)

    Article  MathSciNet  Google Scholar 

  8. Horridge, M., Parsia, B., Sattler, U.: Extracting justifications from bioportal ontologies. In: Cudré-Mauroux, P., Heflin, J., Sirin, E., Tudorache, T., Euzenat, J., Hauswirth, M., Parreira, J.X., Hendler, J., Schreiber, G., Bernstein, A., Blomqvist, E. (eds.) ISWC 2012, Part II. LNCS, vol. 7650, pp. 287–299. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  9. Horrocks, I., Hustadt, U., Sattler, U., Schmidt, R.A.: Computational modal logic. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 181–245. Elsevier (2007)

    Google Scholar 

  10. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Logic Comput. 9(3), 385–410 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  11. Lorenz, S.: A tableaux prover for domain minimization. J. Automat. Reason. 13(3), 375–390 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  12. Massacci, F.: Single step tableaux for modal logics. J. Automat. Reason. 24(3), 319–364 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  13. Nguyen, L.A.: Constructing finite least Kripke models for positive logic programs in serial regular grammar logics. Logic J. IGPL 16(2), 175–193 (2008)

    Article  MATH  Google Scholar 

  14. Niemelä, I.: Implementing circumscription using a tableau method. In: Proc. ECAI 1996, pp. 80–84. Wiley (1996)

    Google Scholar 

  15. Niemelä, I.: A tableau calculus for minimal model reasoning. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol. 1071, pp. 278–294. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  16. Papacchini, F., Schmidt, R.A.: A tableau calculus for minimal modal model generation. Electr. Notes Theoret. Computer Sci. 278(3), 159–172 (2011)

    Article  MathSciNet  Google Scholar 

  17. Papacchini, F., Schmidt, R.A.: Computing minimal models modulo subset-simulation for propositional modal logics. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 279–294. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  18. Reiter, R.: A theory of diagnosis from first principles. Artificial Intelligence 32(1), 57–95 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  19. Schlobach, S., Huang, Z., Cornet, R., van Harmelen, F.: Debugging incoherent terminologies. J. Automat. Reason. 39(3), 317–349 (2007)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The University of Manchester, UK

    Fabio Papacchini & Renate A. Schmidt

Authors
  1. Fabio Papacchini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Renate A. Schmidt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS,, New York University &amp, USA

    Stéphane Demri

  2. Department of Computer Science, University of New Mexico, 87131-0001, Albuquerque, NM, USA

    Deepak Kapur

  3. Max Planck Institute for Informatics, Campus E1 4, 66123, Saarbrücken, Germany

    Christoph Weidenbach

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Papacchini, F., Schmidt, R.A. (2014). Terminating Minimal Model Generation Procedures for Propositional Modal Logics. In: Demri, S., Kapur, D., Weidenbach, C. (eds) Automated Reasoning. IJCAR 2014. Lecture Notes in Computer Science(), vol 8562. Springer, Cham. https://doi.org/10.1007/978-3-319-08587-6_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08587-6_30

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08586-9

  • Online ISBN: 978-3-319-08587-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation