Skip to main content
SpringerLink
Log in

Using Resolution for Testing Modal Satisfiability and Building Models

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

This paper presents a translation-based resolution decision procedure for the multimodal logic K (m)(∩,∪,⌣) defined over families of relations closed under intersection, union, and converse. The relations may satisfy certain additional frame properties. Different from previous resolution decision procedures that are based on ordering refinements, our procedure is based on a selection refinement, the derivations of which correspond to derivations of tableaux or sequent proof systems. This procedure has the advantage that it can be used both as a satisfiability checker and as a model builder. We show that tableaux and sequent-style proof systems can be polynomially simulated with our procedure. Furthermore, the finite model property follows for a number of extended modal logics.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Andréka, H., van Benthem, J. and Németi, I.: Back and forth between modal logic and classical logic, Bull. IGPL 3(5) (1995), 685–720.

    Google Scholar 

  2. Auffray, Y. and Enjalbert, P.: Modal theorem proving: An equational viewpoint, J. Logic Comput. 2(3) (1992), 247–297.

    Google Scholar 

  3. Baader, F., Hollunder, B., Nebel, B., Profitlich, H.-J. and Franconi, E.: An empirical analysis of optimization techniques for terminological representation systems, or: Making KRIS get

  4. Horrocks, I. and Patel-Schneider, P. F.: FaCT and DLP, in H. de Swart (ed.), Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX'98, Lecture Notes in Comput. Sci. 1397, Springer, 1998, pp. 27–30.

  5. Hustadt, U. and Schmidt, R. A.: On evaluating decision procedures for modal logics, in M. Pollack (ed.), Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97), Morgan Kaufmann, 1997, pp. 202–207.

  6. Hustadt, U. and Schmidt, R. A.: An empirical analysis of modal theorem provers, J. Appl. Non-Classical Logics 9(4) (1999), 479–522.

    Google Scholar 

  7. Hustadt, U. and Schmidt, R. A.: Issues of decidability for description logics in the framework of resolution, in R. Caferra and G. Salzer (eds.), First-Order Theorem Proving: FTP'98, Lecture Notes in Artificial Intelligence 1761, Springer, 2000, pp. 192–206.

  8. Hustadt, U. and Schmidt, R. A.: Maslov's class K revisited, in H. Ganzinger (ed.), Automated Deduction — CADE-16, Lecture Notes in Artificial Intelligence 1632, Springer, 1999, pp. 172–186.

  9. Hustadt, U., Schmidt, R. A. and Weidenbach, C.: Optimised functional translation and resolution, in: H. de Swart (ed.), Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX'98, Lecture Notes in Comput. Sci. 1397, Springer, 1998, pp. 36–37.

  10. Jeroslow, R. and Wang, J.: Solving propositional satisfiability problems, Ann. of Math. and Artificial Intelligence 1 (1990), 167–187.

    Google Scholar 

  11. Joyner Jr., W. H.: Resolution strategies as decision procedures, J. ACM 23(3) (1976), 398–417.

    Google Scholar 

  12. Lutz, C., Sattler, U. and Tobies, S.: A suggestion of an n-ary description logic, in P. Lambrix, A. Borgida, M. Lenzerini, R. Möller, and P. Patel-Schneider (eds.), Proc. of Intern. Workshop on Description Logics'99. Linköping University, 1999, pp. 81–85.

  13. Massacci, F.: Strongly analytic tableaux for normal modal logics, in Automated Deduction: CADE-12, Lecture Notes in Artificial Intelligence 814, Springer, 1994, pp. 723–737.

  14. Massacci, F.: Simplification: A general constraint propagation technique for propositional and modal tableaux, in H. de Swart (ed.), Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX'98, Lecture Notes in Artificial Intelligence 1397, Springer, 1998, pp. 217–231.

  15. Mints, G.: A resolution method for non-classical logics, Semiotika and Informatika 25 (1986), 120–135.

    Google Scholar 

  16. Mints, G.: Resolution calculi for modal logics, Amer. Math. Soc. Transl. 143 (1989), 1–14.

    Google Scholar 

  17. Mortimer, M.: On languages with two variables, Z. Math. Logik Grundlag. Math. 21 (1975), 135–140.

    Google Scholar 

  18. Ohlbach, H. J. and Schmidt, R. A.: Functional translation and second-order frame properties of modal logics, J. Logic and Comput. 7(5) (1997), 581–603.

    Google Scholar 

  19. Paramasivam, M. and Plaisted, D. A.: Automated deduction techniques for classification in description logic systems, J. Automated Reasoning 20(3) (1998), 337–364.

    Google Scholar 

  20. Plaisted, D. A. and Greenbaum, S.: A structure-preserving clause form translation, J. Symbolic Comput. 2 (1986), 293–304.

    Google Scholar 

  21. Plaisted, D. A. and Zhu, Y.: The Efficiency of Theorem Proving Strategies, Vieweg, 1997.

  22. Schmidt, R. A.: Decidability by resolution for propositional modal logics, J. Automated Reasoning 22(4) (1999), 379–396.

    Google Scholar 

  23. Tseitin, G. S.: On the complexity of derivations in propositional calculus, in A. O. Slisenko (ed.), Studies in Constructive Mathematics and Mathematical Logic, Part II, Consultants Bureau, New York, 1970, pp. 115–125.

    Google Scholar 

  24. Urquhart, A.: The complexity of propositional proofs, Bull. Symbolic Logic 1(4) (1995), 425–467.

    Google Scholar 

  25. Weidenbach, C., Meyer, C., Cohrs, C., Engel, T. and Keen, E.: SPASS V0.77, J. Automated Reasoning 21(1) (1998), 113.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre for Agent Research and Development, Department of Computing and Mathematics, Manchester Metropolitan University, Chester Street, Manchester, M1 5GD, UK. e-mail

    Ullrich Hustadt & Renate A. Schmidt

Authors
  1. Ullrich Hustadt
    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

Rights and permissions

Reprints and permissions

About this article

Cite this article

Hustadt, U., Schmidt, R.A. Using Resolution for Testing Modal Satisfiability and Building Models. Journal of Automated Reasoning 28, 205–232 (2002). https://doi.org/10.1023/A:1015067300005

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1015067300005

Search

Navigation