MSPASS: Modal Reasoning by Translation and First-Order Resolution | SpringerLink
Skip to main content
Springer Nature Link
Log in

MSPASS: Modal Reasoning by Translation and First-Order Resolution

  • Conference paper
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000)

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

Abstract

mspass is an extension of the first-order theorem prover spass, which can be used as a modal logic theorem prover, a theorem prover for description logics and a theorem prover for the relational calculus.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

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

    Article  MATH  MathSciNet  Google Scholar 

  2. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Computat. 4(3), 217–247 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  3. De Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-based methods for modal logics. Logic J. IGPL (2000) (to appear)

    Google Scholar 

  4. Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proc. LICS 1999, pp. 295–303. IEEE Computer Soc, Los Alamitos (1999)

    Google Scholar 

  5. Herzig, A.: Raisonnement automatique en logique modale et algorithmes d’unification. PhD thesis, Univ. Paul-Sabatier, Toulouse (1989)

    Google Scholar 

  6. Hustadt, U.: Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Univ. d. Saarlandes, Saarbrücken, Germany (1999)

    Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

  8. Hustadt, U., Schmidt, R.A.: Maslov’s class K revisited. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 172–186. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  9. Hustadt, U., Schmidt, R.A.: Issues of decidability for description logics in the framework of resolution. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 191–205. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Hustadt, U., Schmidt, R.A.: Using resolution for testing modal satisfiability and building models. To appear in J. Automated Reasoning (2000)

    Google Scholar 

  11. Hustadt, U., Schmidt, R.A., Weidenbach, C.: Optimised functional translation and resolution. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 36–37. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  12. Nonnengart, A.: First-order modal logic theorem proving and functional simulation. In: Proc. IJCAI 1993, pp. 80–85. Morgan Kaufmann, San Francisco (1993)

    Google Scholar 

  13. Nonnengart, A., Rock, G., Weidenbach, C.: On generating small clause normal forms. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 397–411. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  14. Ohlbach, H.J.: Semantics based translation methods for modal logics. J. Logic Computat. 1(5), 691–746 (1991)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  Google Scholar 

  17. Schmidt, R.A.: MSPASS (1999), http://www.cs.man.ac.uk/~schmidt/mspass/

  18. Sutcliffe, G., Suttner, C.B.: The CADE-14 ATP system competition. J. Automated Reasoning 21(1), 99–134 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  19. Weidenbach, C.: SPASS (1999), http://spass.mpi-sb.mpg.de

  20. Weidenbach, C.: SPASS: Combining superposition, sorts and splitting. In: Handbook of Automated Reasoning. Elsevier, Amsterdam (2000) (to appear)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre for Agent Research and Development, Manchester Metropolitan University, Manchester, M1 5GD, United Kingdom

    Ullrich Hustadt

  2. Department of Computer Science, University of Manchester, Manchester, M13 9PL, United Kingdom

    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

Editor information

Editors and Affiliations

  1. School of Computer Science, University of St Andrews, Scotland

    Roy Dyckhoff

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hustadt, U., Schmidt, R.A. (2000). MSPASS: Modal Reasoning by Translation and First-Order Resolution. In: Dyckhoff, R. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2000. Lecture Notes in Computer Science(), vol 1847. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722086_7

Download citation

  • DOI: https://doi.org/10.1007/10722086_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67697-3

  • Online ISBN: 978-3-540-45008-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation