Complexity of admissible rules. (English) Zbl 1115.03010

An inference rule is admissible in a logic \(L\) if the set of theorems of \(L\) is closed under the rule. V. Rybakov proved decidability of the problem od admissibility for many modal and superintuitionistic logics. The author provides complexity estimates for this problem which are optimal or close to optimal. Admissibility in “typical” extensions of K4 and superintuitionistic logics is co-NEXP-complete while derivability is P-SPACE-complete or even NP-complete. A co-NEXP decision procedure is given for admissibility in a class of logics including K4, GL, S4, S4Grz and Int. Admissibility is proved to be co-NEXP-hard in all superintuitionistic logics \(L\) such that every depth-3 tree is an \(L\)-frame and in similar normal modal extensions of K4.


03B45 Modal logic (including the logic of norms)
03B55 Intermediate logics
03D15 Complexity of computation (including implicit computational complexity)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Full Text: DOI Link


[1] Blackburn P., Venema Y. and Rijke M. (2001). Modal logic, Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge · Zbl 0988.03006
[2] Bull R.A. (1966). That all normal extensions of S4.3 have the finite model property. Zeitschrift mathematische Logik Grundlagen Mathematik 12: 341–344 · Zbl 0154.00407
[3] Chagrov, A.V.: On the complexity of propositional logics. In: Complexity problems in Mathematical Logic, pp. 80–90. Kalinin State University (1985) (in Russian) · Zbl 0615.03023
[4] Chagrov A.V. (1992). A decidable modal logic with the undecidable admissibility problem for inference rules. Algebra Logic 31: 53–55 · Zbl 0782.03005
[5] Chagrov A.V. and Zakharyaschev M. (1997). Modal Logic. Oxford Logic Guides, vol. 35. Oxford University Press, Oxford · Zbl 0871.03007
[6] Fagin, R.: Generalized first-order spectra and polynomial-time recognizable sets. In: Karp, R.M. (ed.) Complexity of Computation SIAM-AMS Proceedings, vol. 7, pp. 43–73 (1974) · Zbl 0303.68035
[7] Friedman H.M. (1975). One hundred and two problems in mathematical logic. J. Symbolic Logic 40(2): 113–129 · Zbl 0318.02002
[8] Ghilardi S. (1999). Unification in intuitionistic logic. J. Symbolic Logic 64(2): 859–880 · Zbl 0930.03009
[9] Ghilardi S. (2000). Best solving modal equations. Ann. Pure Appl. Logic 102(3): 183–198 · Zbl 0949.03010
[10] Ghilardi S. (2002). A resolution/tableaux algorithm for projective approximations in IPC. Logic J. IGPL 10(3): 229–243 · Zbl 1005.03504
[11] Iemhoff R. (2001). On the admissible rules of intuitionistic propositional logic. J. Symbolic Logic 66(1): 281–294 · Zbl 0986.03013
[12] Iemhoff R. (2005). Intermediate logics and Visser’s rules. Notre Dame J. Formal Logic 46(1): 65–81 · Zbl 1102.03032
[13] Iemhoff R. (2006). On the rules of intermediate logics. Arch. Math. Logic 45(5): 581–599 · Zbl 1096.03025
[14] Jeřábek E. (2005). Admissible rules of modal logics. J. Logic Comput. 15(4): 411–431 · Zbl 1077.03011
[15] Kuznetsov, A.V.: On superintuitionistic logics. In: Proceedings of the International Congress of Mathematicians (Vancouver), pp. 243–249 (1975) · Zbl 0342.02015
[16] Ladner R.E. (1977). The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6(3): 467–480 · Zbl 0373.02025
[17] Papadimitriou C.H. (1994). Computational complexity. Addison-Wesley, Reading · Zbl 0833.68049
[18] Rybakov V.V. (1997). Admissibility of logical inference rules. Studies in Logic and the Foundations of Mathematics, vol 136. Elsevier, Amsterdam · Zbl 0872.03002
[19] Spaan, E.: Complexity of modal logics. Ph.D. thesis, University of Amsterdam (1993) · Zbl 0831.03005
[20] Statman R. (1979). Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci. 9(1): 67–72 · Zbl 0411.03049
[21] Zakharyaschev M. (1996). Canonical formulas for K4. Part II: Cofinal subframe logics. J. Symbolic Logic 61(2): 421–449 · Zbl 0884.03014
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.