Abstract
We investigate the complexity of the decision problem for subclasses of the intuitionistic propositional calculus and present upper bounds for decision procedures locating these subclasses into lower complexity classes like co-NP or polynomial time.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Kleene S. C.,Introduction to Metamathematics. van Nostrand (1952).
Marin-Löf P., Mints G. (eds),COLOG-88.Lecture Notes in Computer Science, Springer-Verlag v. 417, (1990).
Mints G.,Resolution calculi for the non-classical logics. (Russian). 9 Soviet Symp. in Cybernetics. Moscow, VINITI, (1981).
Mints G.,Gentzen-type systems and resolution rule. Part I. In [2], pp. 198–231.
Mints G., Tyugu E.,Justification of the structural synthesis of programs. Sci. of Comput. Program., (1982), N2, 215–240.
B. Nordström, K. Peterson, J. Smith,Programming in Martin-Löf's Type Theory. An Introduction. Oxford University Press, (1990).
Orevkov V.,On Glivenko classes of sequents. Proc. Steklov Inst. of Math., (1968), AMS Translations-Series 2, v. 98.
Wajsberg M.,Untersuchungen über den Aussagenkalkül von A. Heyting, Wiadomosci Matematyczne, 46, (1938), 45–101.