Using temporal logics of knowledge for specification and verification -- a case study

DOI10.1016/j.jal.2005.08.003zbMath1095.68050OpenAlexW2046865417MaRDI QIDQ2494726

Clare Dixon

Publication date: 30 June 2006

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2005.08.003

zbMATH Keywords

resolutionautomated deductionspecification and verificationtemporal and epistemic logics

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Rationality and learning in game theory (91A26) Temporal logic (03B44)

Related Items (3)

Parameterized verification of leader/follower systems via first-order temporal logic ⋮ Three Steps ⋮ Taming the Complexity of Temporal Epistemic Reasoning

Uses Software

• KARO
• TeMP
• TRP++

Cites Work

• Knowledge, action, and the frame problem
• First-order temporal verification in practice
• A structure-preserving clause form translation
• The complexity of reasoning about knowledge and time. I: Lower bounds
• Mechanising first-order temporal resolution
• Tableaux for logics of time and knowledge with interactions relating to synchrony
• Decision procedures for BDI logics
• Resolution for temporal logics of knowledge
• A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief
• Complete Axiomatizations for Reasoning about Knowledge and Time
• Automated Reasoning
• Clausal temporal resolution
• Automated Deduction – CADE-19
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Using temporal logics of knowledge for specification and verification -- a case study