An analytic tableau calculus for a temporalised belief logic

Ji Ma, Mehmet A. Orgun*, Kamel Adi

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)


A tableau is a refutation-based decision procedure for a related logic, and is among the most popular proof procedures for modal logics. In this paper, we present a labelled tableau calculus for a temporalised belief logic called TML+, which is obtained by adding a linear-time temporal logic onto a belief logic by the temporalisation method of Finger and Gabbay. We first establish the soundness and the completeness of the labelled tableau calculus based on the soundness and completeness results of its constituent logics. We then sketch a resolution-type proof procedure that complements the tableau calculus and also propose a model checking algorithm for TML+ based on the recent results for model checking procedures for temporalised logics. TML+ is suitable for formalising trust and agent beliefs and reasoning about their evolution for agent-based systems. Based on the logic TML+, the proposed labelled tableau calculus could be used for analysis, design and verification of agent-based systems operating in dynamic environments.

Original languageEnglish
Pages (from-to)289-304
Number of pages16
JournalJournal of Applied Logic
Issue number4
Publication statusPublished - Dec 2011


Dive into the research topics of 'An analytic tableau calculus for a temporalised belief logic'. Together they form a unique fingerprint.

Cite this