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

DOI10.1007/3-540-61208-4_14zbMATH Open1415.03023OpenAlexW1497109150MaRDI QIDQ4645239FDOQ4645239

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

Recommendations

• Termination of derivations for minimal tense logic
• A New Method to Obtain Termination in Backward Proof Search For Modal Logic S4
• Detecting Loops During Proof Search in Propositional Affine Logic
• Efficient loop-check for KD45 logic
• Loop-free calculus for modal logic S4. II

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (17)

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

Uses Software

• LWB

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

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