A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief
From MaRDI portal
A tableaux-based proof method is presented for two multi-agent temporal logics: a temporal logic of knowledge \(KLn\) in which \(n\) unary modal connectives \(K_iA\) (meaning ``agent \(i\) knows \(A\)) satisfy axioms similar to the modal logic S5 (which describes \textit{idealized} knowledge), and a temporal logic of belief \(BLn\) in which \(n\) unary modal connectives \(B_iA\) (meaning ``agent \(i\) believes in \(A\)) satisfy axioms similar to the modal logic KD45 (which describes \textit{idealized} beliefs).
Recommendations
- A resolution-based proof method for temporal logics of knowledge and belief
- An analytic tableau calculus for a temporalised belief logic
- Tableau methods for modal and temporal logics
- A general tableau method for propositional interval temporal logics
- scientific article; zbMATH DE number 3937153
- A general tableau method for propositional interval temporal logics: theory and implementation
- A framework for using knowledge in tableau proofs
- A tableau method for interval temporal logic with projection
- Sequent calculi for temporal logics of common knowledge and belief
- A tableau calculus for a temporal logic with temporal connectives
Cites work
- A guide to completeness and complexity for modal logics of knowledge and belief
- scientific article; zbMATH DE number 3670430 (Why is no real title available?)
- scientific article; zbMATH DE number 795590 (Why is no real title available?)
- scientific article; zbMATH DE number 3274715 (Why is no real title available?)
- Knowledge, belief and time
- Proof methods for modal and intuitionistic logics
- The complexity of reasoning about knowledge and time. I: Lower bounds
- What can machines know?
Cited in
(22)- Clausal resolution in a logic of rational agency
- Sequent calculi for branching time temporal logics of knowledge and beliefwith awareness: completeness and decidability
- A sequent calculus for logic of knowledge and past time: completeness and decidability
- Using temporal logics of knowledge for specification and verification -- a case study
- A general tableau method for propositional interval temporal logics: theory and implementation
- Knowledge and approximations: a formal study under the perspective of information systems and rough set theory
- Tableau methods for modal and temporal logics
- Temporal logics of knowledge and their applications in security
- Tableaux-based decision method for single-agent linear time synchronous temporal epistemic logics with interacting time and knowledge
- Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic
- Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs
- Tableaux for logics of time and knowledge with interactions relating to synchrony
- Taming the Complexity of Temporal Epistemic Reasoning
- A tableau method for interval temporal logic with projection
- scientific article; zbMATH DE number 1107650 (Why is no real title available?)
- Analytic tableau systems for propositional bimodal logics of knowledge and belief
- A decision procedure for a temporal belief logic
- An analytic tableau calculus for a temporalised belief logic
- A framework for using knowledge in tableau proofs
- A resolution-based proof method for temporal logics of knowledge and belief
- Logics for Temporal Information Systems in Rough Set Theory
- Tableau Systems for Epistemic Positional Logics
This page was built for publication: A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4236067)
