Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

On the size of refutation Kripke models for some linear modal and tense logics


LetL be any modal or tense logic with the finite model property. For eachm, definer L (m) to be the smallest numberr such that for any formulaA withm modal operators,A is provable inL if and only ifA is valid in everyL-model with at mostr worlds. Thus, the functionr L determines the size of refutation Kripke models forL. In this paper, we will give an estimation ofr L (m) for some linear modal and tense logicsL.

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


  1. [1]

    S.A. Cook,The complexity of theorem proving procedures, Proceedings of Third Annual ACM Symposium on Theory of Computing (1971) 151–158.

  2. [2]

    R.E. Ladner,The computational complexity of provability in systems of modal prepositional logic, SIAM J. on Computing, 6 (1977) 467–480.

  3. [3]

    R.P. McArthur,Tense logic D. Reidel, 1976.

  4. [4]

    H. Ono andA. Nakamura,The computational complexity of satisfiability of modal propositional logic S4.3. Tech. Rep. No.C-5, Dept. of Applied Math., Hiroshima Univ. (1979).

  5. [5]

    H. Rasiowa andR. Sikorski,The mathematics of metamathematics,Monografie Matematyczne 41, PWN, 1963.

  6. [6]

    K. Segerberg,An essay in classical modal logic,Filosofiska Studier 13, Uppsala Univ. (1971).

Download references

Author information

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Ono, H., Nakamura, A. On the size of refutation Kripke models for some linear modal and tense logics. Stud Logica 39, 325–333 (1980).

Download citation


  • Mathematical Logic
  • Modal Operator
  • Computational Linguistic
  • Model Property
  • Kripke Model