An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic

DOI10.1093/LOGCOM/3.1.63zbMath0788.03010OpenAlexW2092765780MaRDI QIDQ4272505

Jörg Hudelmaier

Publication date: 6 December 1993

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/3.1.63

zbMATH Keywords

sequent calculusintuitionistic logicintuitionistic propositional logicdecision proceduretableau systemdecision algorithm

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (29)

KALC: a constructive semantics for ALC ⋮ Proof compression and NP versus PSPACE ⋮ A unified procedure for provability and counter-model generation in minimal implicational logic ⋮ An Evaluation-Driven Decision Procedure for G3i ⋮ Proof Compression and NP Versus PSPACE II: Addendum ⋮ Linear depth deduction with subformula property for intuitionistic epistemic logic ⋮ Generalized tableau systems for intermediate propositional logics ⋮ Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem ⋮ Admissibility of structural rules for contraction-free systems of intuitionistic logic ⋮ Proof Compression and NP Versus PSPACE II ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Sequent calculi for intuitionistic Gödel-Löb logic ⋮ Inconsistency-tolerant description logic. II: A tableau algorithm for \(\mathcal{CALC}^{\mathsf C}\) ⋮ A Conditional Constructive Logic for Access Control and Its Sequent Calculus ⋮ Efficient loop-check for backward proof search in some non-classical propositional logics ⋮ Proof-search in intuitionistic logic based on constraint satisfaction ⋮ Optimization techniques for propositional intuitionistic logic and their implementation ⋮ Decision methods for linearly ordered Heyting algebras ⋮ Improved decision procedures for the modal logics K, T and S4 ⋮ Proof theory for Lax Logic ⋮ On Dummett's pragmatist justification procedure ⋮ A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications ⋮ Deciding intuitionistic propositional logic via translation into classical logic ⋮ Eight inference rules for implication ⋮ Uniform interpolation and the existence of sequent calculi ⋮ Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics ⋮ The G4i analogue of a G3i sequent calculus ⋮ Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models ⋮ Synthesis of modality definitions and a theorem prover for epistemic intuitionistic logic

This page was built for publication: An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic