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

DOI10.1007/3-540-61208-4_14MaRDI QIDQ4645239zbMATH OpenOpenAlexFDO

Authors Alain Heuerding, Michael Seyfried, Heinrich Zimmermann

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) Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)

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

Cites work

• scientific article; zbMATH DE number 3670430 (Why is no real title available?)
• scientific article; zbMATH DE number 512976 (Why is no real title available?)
• scientific article; zbMATH DE number 3363520 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Contraction-free sequent calculi for intuitionistic logic
• Proof methods for modal and intuitionistic logics
• Relations between propositional normal modal logics: an overview
• The Computational Complexity of Provability in Systems of Modal Propositional Logic

Cited in

(20)

• Verified Decision Procedures for Modal Logics.
• From QBFs to \textsf{MALL} and back via focussing
• Detecting Loops During Proof Search in Propositional Affine Logic
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• Cut elimination by unthreading
• Proof theory for positive logic with weak negation
• A new rule for LTL tableaux
• EXPtime tableaux for ALC
• Loop-check specification for a sequent calculus of temporal logic
• Intuitionistic Decision Procedures Since Gentzen
• Two loop detection mechanisms: a comparison
• Free variable tableaux for propositional modal logics
• The Tableau Workbench
• Loop-check elimination for non-transitive distributed knowledge logic
• Normative reasoning and consequence
• 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
• Efficient loop-check for KD45 logic

Describes a project that uses

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)