Sequent calculi with an efficient loop-check for BDI logics

Sequent calculi for BDI logics is a research object of the thesis. BDI logics are widely used for agent system description and implementation. Agents are autonomous systems, those acts in some environment and aspire to achieve preassigned goals. Implementation of the decision making is the main and the most complicated part in agent systems implementation. Logic calculi may be used for the decision making implementation. In this thesis, there are researched sequent calculi for BDI logics. Sequent calculi for BDI logics, like sequent calculi for other modal logics, use loop-check technique to get decidability. Inefficient loop-check takes a major part of the resources used for the derivation. For some modal logics, there are known loop-check free sequent calculi or calculi with an efficient loop-check. In this thesis, there is presented loop-check free sequent calculus for KD45 logic, which is the main fragment of the BDI logics. Introduced calculus not only eliminates loop-check, but also simplifies sequent derivation. For the branching time logic (another BDI logic fragment) there is presented sequent calculus with an efficient loop-check. Obtained results are adapted for creation sequent calculi for monoagent and multiagent BDI logics. Introduced calculi use only restricted loop-check. Moreover, loop-check is totally eliminated for some types of the loops. These results enables to create more efficient agent systems, those are based on the BDI logics