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)

• Intuitionistic Decision Procedures Since Gentzen
• Normative reasoning and consequence
• The Tableau Workbench
• From QBFs to \textsf{MALL} and back via focussing
• Loop-check elimination for non-transitive distributed knowledge logic
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
• Two loop detection mechanisms: a comparison
• EXPtime tableaux for ALC
• A unified procedure for provability and counter-model generation in minimal implicational logic
• Loop-check specification for a sequent calculus of temporal logic
• Proof theory for positive logic with weak negation
• Detecting Loops During Proof Search in Propositional Affine Logic
• Hintikka multiplicities in matrix decision methods for some propositional modal logics
• Cut elimination by unthreading
• A new rule for LTL tableaux
• Free variable tableaux for propositional modal logics
• 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.
• 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)