A simple tableau system for the logic of elsewhere

DOI10.1007/3-540-61208-4_12MaRDI QIDQ4645235zbMATH OpenOpenAlexFDO

Authors Stéphane Demri

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_12

zbMATH Keywords

induction hypothesismodal logicproof systempropositional variablesatisfiability problem

Mathematics Subject Classification ID

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

Recommendations

• A simple propositional \(\text{S}5\) tableau system
• TABLEAUX: A general theorem prover for modal logics
• Clausal Tableaux for Multimodal Logics of Belief
• Proof-theoretic functional completeness for the hybrid logics of everywhere and elsewhere
• On modal products with the logic of `elsewhere'

Cites work

• A cut-free Gentzen-type system for the modal logic S5
• A guide to completeness and complexity for modal logics of knowledge and belief
• A tableau system for propositional S5
• A tableau-like proof procedure for normal modal logics
• An essay in combinatory dynamic logic
• First-order modal tableaux
• scientific article; zbMATH DE number 4148058 (Why is no real title available?)
• scientific article; zbMATH DE number 3902618 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3325547 (Why is no real title available?)
• scientific article; zbMATH DE number 970635 (Why is no real title available?)
• Logical consequence in modal logic: Natural deduction in S5
• Modal definability in enriched languages
• Modal logic with names
• Modal trees for T and S5
• Proof methods for modal and intuitionistic logics
• Strongly analytic tableaux for normal modal logics
• TABLEAUX: A general theorem prover for modal logics
• The complexity of theorem-proving procedures
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic
• The modal logic of inequality
• Uniform and non uniform strategies for tableaux calculi for modal logics
• Using the Universal Modality: Gains and Questions
• What is an inference rule?

Cited in

(2)

• A simple propositional \(\text{S}5\) tableau system
• Hybrid tableaux for the difference modality

Describes a project that uses

Uses Software

• TABLEAUX

This page was built for publication: A simple tableau system for the logic of elsewhere

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