Intuitionistic propositional logic is polynomial-space complete

DOI10.1016/0304-3975(79)90006-9zbMath0411.03049DBLPjournals/tcs/Statman79OpenAlexW1991670662WikidataQ56224787 ScholiaQ56224787MaRDI QIDQ1259589

Richard Statman

Publication date: 1979

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2027.42/23534

zbMATH Keywords

proof theorycomplexity of proofstyped lambda calculusNp-completenesslength of derivationsvalidity in intuitionistic propositional logic

Mathematics Subject Classification ID

Complexity of computation (including implicit computational complexity) (03D15) Intuitionistic mathematics (03F55) Combinatory logic and lambda calculus (03B40) Complexity of proofs (03F20)

Related Items (67)

Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer) ⋮ Sequent Calculus for Intuitionistic Epistemic Logic IEL ⋮ The complexity of Horn fragments of linear logic ⋮ Complexity of interpolation and related problems in positive calculi ⋮ Proof compression and NP versus PSPACE ⋮ Stable Philosophical Systems and Radical Anti-realism ⋮ Satisfiability in many-valued sentential logic is NP-complete ⋮ IMPLICATIONAL RELEVANCE LOGIC IS 2-EXPTIME-COMPLETE ⋮ Partial up an down logic ⋮ Undecidability of Propositional Separation Logic and Its Neighbours ⋮ Graph decompositions and tree automata in reasoning with uncertainty ⋮ Complexity of admissible rules ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ A lower bound for intuitionistic logic ⋮ Partial algebras and complexity of satisfiability and universal theory for distributive lattices, Boolean algebras and Heyting algebras ⋮ Unnamed Item ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Computational complexity of the word problem in modal and Heyting algebras with a small number of generators ⋮ Proof Compression and NP Versus PSPACE II: Addendum ⋮ Proof theory for positive logic with weak negation ⋮ An informational view of classical logic ⋮ Complexity of some problems in positive and related calculi ⋮ Complexity of some language fragments of fuzzy logics ⋮ On the polynomial-space completeness of intuitionistic propositional logic ⋮ Admissible rules in the implication-negation fragment of intuitionistic logic ⋮ Tarski's theorem on intuitionistic logic, for polyhedra ⋮ Unnamed Item ⋮ From QBFs to \textsf{MALL} and back via focussing ⋮ Hypothetical datalog: Complexity and expressibility ⋮ Unnamed Item ⋮ On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems ⋮ Unnamed Item ⋮ An \(\mathsf{AC}^{1}\)-complete model checking problem for intuitionistic logic ⋮ Proof Compression and NP Versus PSPACE II ⋮ Sufficient conditions for cut elimination with complexity analysis ⋮ Plug and Play Negations ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Proof-search in intuitionistic logic based on constraint satisfaction ⋮ Unification under a mixed prefix ⋮ Studying provability in implicational intuitionistic logic ⋮ Optimization techniques for propositional intuitionistic logic and their implementation ⋮ Rules with parameters in modal logic. II. ⋮ Linearizing intuitionistic implication ⋮ Disjunction property and complexity of substructural logics ⋮ The emptiness problem for intersection types ⋮ Typing in reflective combinatory logic ⋮ Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic ⋮ Computational complexity for bounded distributive lattices with negation ⋮ The consequence relation in the logic of commutative GBL-algebras is PSPACE-complete ⋮ Unnamed Item ⋮ How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning ⋮ The typed lambda-calculus is not elementary recursive ⋮ Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding ⋮ Infiniteness of \(\text{proof}(\alpha)\) is polynomial-space complete ⋮ Complexity of intuitionistic propositional logic and its fragments ⋮ A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications ⋮ Mereotopology in 2nd-Order and Modal Extensions of Intuitionistic Propositional Logic ⋮ Some pitfalls of LK-to-LJ translations and how to avoid them ⋮ Deriving Efficient Sequential and Parallel Generators for Closed Simply-Typed Lambda Terms and Normal Forms ⋮ Proof finding algorithms for implicational logics ⋮ Pre-grammars and inhabitation for a subset of rank 2 intersection types ⋮ The complexity of the disjunction and existential properties in intuitionistic logic ⋮ DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV ⋮ \(\lambda\)-definability of free algebras ⋮ Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction ⋮ Synthesis of modality definitions and a theorem prover for epistemic intuitionistic logic

Cites Work

• The polynomial-time hierarchy
• The typed lambda-calculus is not elementary recursive
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Intuitionistic propositional logic is polynomial-space complete