Efficient loop-check for backward proof search in some non-classical propositional logics

DOI10.1007/3-540-61208-4_14zbMath1415.03023OpenAlexW1497109150MaRDI QIDQ4645239

Alain Heuerding, Heinrich Zimmermann, Michael Seyfried

Publication date: 10 January 2019

Published in: Theorem Proving with Analytic Tableaux and Related Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61208-4_14

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

A unified procedure for provability and counter-model generation in minimal implicational logic ⋮ ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching ⋮ Unnamed Item ⋮ Proof theory for positive logic with weak negation ⋮ Cut elimination by unthreading ⋮ Free variable tableaux for propositional modal logics ⋮ Hintikka multiplicities in matrix decision methods for some propositional modal logics ⋮ Two loop detection mechanisms: A comparison ⋮ Unnamed Item ⋮ From QBFs to \textsf{MALL} and back via focussing ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic ⋮ Verified Decision Procedures for Modal Logics. ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ The Tableau Workbench ⋮ EXPtime tableaux for ALC ⋮ Loop-check specification for a sequent calculus of temporal logic ⋮ Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models

Uses Software

• LWB

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof methods for modal and intuitionistic logics
• Contraction-free sequent calculi for intuitionistic logic
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Relations between propositional normal modal logics: an overview