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 (17)

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

This page was built for publication: Efficient loop-check for backward proof search in some non-classical propositional logics