A bi-intuitionistic modal logic: foundations and automation

DOI10.1016/J.JLAMP.2015.11.003MaRDI QIDQ299186zbMATHOpenAlexWikidataFDO

Authors John G. Stell, Renate A. Schmidt, David Rydeheard

Publication date 22 June 2016

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2015.11.003

zbMATH Keywords

decidabilitytemporal logicbi-intuitionistic logiccorrespondence theoremtableau system

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) Temporal logic (03B44)

Recommendations

• Tableau Development for a Bi-intuitionistic Tense Logic
• BDD-based automated reasoning for propositional bi-intuitionistic tense logics
• Cut-elimination and proof search for bi-intuitionistic tense logic
• A Cut-Free Sequent Calculus for Bi-intuitionistic Logic
• Bi-simulating in bi-intuitionistic logic

Cites work

• scientific article; zbMATH DE number 3902440 (Why is no real title available?)
• scientific article; zbMATH DE number 46487 (Why is no real title available?)
• scientific article; zbMATH DE number 3501559 (Why is no real title available?)
• scientific article; zbMATH DE number 1852920 (Why is no real title available?)
• scientific article; zbMATH DE number 5791678 (Why is no real title available?)
• A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
• A description logic with transitive and inverse roles and role hierarchies
• A formalization of the propositional calculus of H-B logic
• A modal walk through space
• Automated synthesis of tableau calculi
• Axiomatic and tableau-based reasoning for \(Kt (H, R)\)
• Bi-Heyting algebras, toposes and modalities
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods
• Constructive negation, implication, and co-implication
• Handbook of Spatial Logics
• Modal logic
• Modal logics based on mathematical morphology for qualitative spatial reasoning
• Relations on hypergraphs
• Self-dual morphological operators and filters.
• Symmetric Heyting relation algebras with applications to hypergraphs
• Using tableau to decide description logics with full role negation and identity

Cited in

(9)

• Analytic cut and Mints' symmetric interpolation method for bi-intuitionistic tense logic
• Expressing discrete spatial relations under granularity
• On displaying negative modalities
• Hennessy-Milner properties via topological compactness
• Blocking and other enhancements for bottom-up model generation methods
• The logic of discrete qualitative relations
• Intuitionistic public announcement logic with distributed knowledge
• BDD-based automated reasoning for propositional bi-intuitionistic tense logics
• \(L\)-fuzzy relational mathematical morphology based on adjoint triples

Describes a project that uses

Uses Software

• MetTeL

This page was built for publication: A bi-intuitionistic modal logic: foundations and automation

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