Deduction Systems for BDI Logics Using Sequent Calculus

摘要

In this paper, we present sound and complete deduction systems for propositional BDI logics by using Gentzen's sequent calculus. In these systems, we can construct the proof of a formula by using an extension of Wang's algorithm. Therefore, these systems are suitable for applications such as automatic; proving and specification checking in BDI logics.