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.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
S.A. Cook,The complexity of theorem proving procedures, Proceedings of Third Annual ACM Symposium on Theory of Computing (1971) 151–158.
R.E. Ladner,The computational complexity of provability in systems of modal prepositional logic, SIAM J. on Computing, 6 (1977) 467–480.
R.P. McArthur,Tense logic D. Reidel, 1976.
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).
H. Rasiowa andR. Sikorski,The mathematics of metamathematics,Monografie Matematyczne 41, PWN, 1963.
K. Segerberg,An essay in classical modal logic,Filosofiska Studier 13, Uppsala Univ. (1971).
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). https://doi.org/10.1007/BF00713542
- Mathematical Logic
- Modal Operator
- Computational Linguistic
- Model Property
- Kripke Model