Decision Procedure for Temporal Logic of Belief and Actions

Article type: Research Article

Authors: Pliuškevičius, Regimantas | Pliuškevičienė, Aida

Affiliations: Institute of Mathematics and Informatics, Akademijos 4, 08663 Vilnius, Lithuania, e‐mail: {regis,aida}@ktl.mii.lt

Abstract: A temporal logic of belief and actions (TLBA) is considered. The TLBA allows us to express informational and dynamic properties of computational agents. The considered fragment of TLBA allows one: (1) to present a deduction‐based structured decision procedure; (2) to separate a decision procedure for so‐called induction‐free formulas and (3) to use only logical axioms for such formulas. The main new technical tool of the presented decision procedure is separation rules which incorporate traditional rules for the temporal operator “next”, belief modalities and action constants.

Keywords: rational agent, temporal, modal, and dynamic logics, agent‐based logic, deduction‐based decision procedure, sequent calculus

Journal: Informatica, vol. 15, no. 3, pp. 379-398, 2004