A simple tableau system for the logic of elsewhere

DOI10.1007/3-540-61208-4_12zbMath1415.03021OpenAlexW1582676071MaRDI QIDQ4645235

Stéphane P. 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

modal logicsatisfiability problemproof systempropositional variableinduction hypothesis

Mathematics Subject Classification ID

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

Related Items (1)

Hybrid Tableaux for the Difference Modality

Uses Software

• TABLEAUX

Cites Work

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

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