Space-efficient Decision Procedures for Three Interpolable Propositional Intermediate Logics

DOI10.1093/LOGCOM/12.6.955MaRDI QIDQ4796459zbMATH OpenOpenAlexFDO

Authors Guido Fiorino

Publication date 6 October 2003

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/55cae736e9609f190c42d38b9a3ad2c2037f7200

zbMATH Keywords

duplication-free tableau calculipropositional intermediate logicsspace-efficient decision procedures

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Intermediate logics (03B55) Complexity of proofs (03F20)

Review text

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.

Recommendations

• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• An O(n n)-SPACE decision procedure for the propositional Dummett logic
• Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics
• On sequent calculi for intuitionistic propositional logic.
• A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications

Cited in

(7)

• Decision methods for linearly ordered Heyting algebras
• Intuitionistic Decision Procedures Since Gentzen
• A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics
• An O(n n)-SPACE decision procedure for the propositional Dummett logic
• Optimization techniques for propositional intuitionistic logic and their implementation

This page was built for publication: Space-efficient Decision Procedures for Three Interpolable Propositional Intermediate Logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4796459)