An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
From MaRDI portal
Publication:4272505
DOI10.1093/logcom/3.1.63zbMath0788.03010OpenAlexW2092765780MaRDI QIDQ4272505
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
sequent calculusintuitionistic logicintuitionistic propositional logicdecision proceduretableau systemdecision algorithm
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
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, 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
