Space-efficient Decision Procedures for Three Interpolable Propositional Intermediate Logics (Q4796459)

Intermediate logics are used in computer science in the frameworks of concurrency, program synthesis, abstract data type specification and formal verification. In this paper, the author considers three interpolable propositional intermediate logics and gives duplication-free tableau calculi in which the depth of proofs is linearly bounded by the length of the formula to be proved, every rule has a constant number of conclusions and the number of formulas in every conclusion is linearly bounded by the length of the formula to be proved. These properties allow space-efficient decision procedures. Using such calculi, the authors present an \(O(n)\)-SPACE decision procedure for one of the considered logics and an \(O(n\log n)\)-SPACE decision procedure for the other two logics. For every calculus the authors give a semantical proof of the soundness and completeness theorems.