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. / Darbe nagrinėjami sekvenciniai skaičiavimai BDI logikoms. BDI logikos yra plačiai naudojamos agentinių sistemų aprašymui ir realizavimui. Agentai yra autonomiškos sistemos, kurios veikia kažkurioje aplinkoje ir siekia įvykdyti iš anksto apibrėžtus tikslus. Sprendimų priėmimo realizavimas yra svarbiausia ir sudėtingiausia dalis realizuojant agentines sistemas. Sprendimo priėmimo realizavimui gali būti naudojami logikos skaičiavimai. Šiame darbe ir yra nagrinėjami sekvenciniai skaičiavimai BDI logikoms. BDI logikose, kaip ir kitose modalumo logikose, yra naudojama ciklų paieška išsprendžiamumui gauti. Neefektyvi ciklų paieška užima didesnę išvedimų paieškos resursų dalį. Kai kurioms modalumo logikoms yra žinomi becikliai skaičiavimai ar skaičiavimai naudojantys efektyvią ciklų paiešką. Šiame darbe yra pateikiamas beciklis sekvencinis skaičiavimas KD45 logikai, kuri yra esminis BDI logikų fragmentas. Pateiktas skaičiavimas ne tik eliminuoja ciklų paiešką, bet ir supaprastina patį sekvencijos išvedimą. Skaidaus laiko logikai (kitam BDI logikų fragmentui) yra pateikiamas sekvencinis skaičiavimas naudojantis efektyvią ciklų paiešką. Gauti rezultatai yra pritaikyti sukuriant sekvencinius skaičiavimus vianaagentinei ir daugiaagentinei BDI logikoms. Pristatyti skaičiavimai naudoja tik apribotą ciklų paiešką. Be to, kai kurių tipų ciklus eliminuoja visiškai. Šie rezultatai įgalina kurti efektyvesnes agentines sistemas, paremtas BDI logikomis.

Darbe nagrinėjami sekvenciniai skaičiavimai BDI logikoms. BDI logikos yra plačiai naudojamos agentinių sistemų aprašymui ir realizavimui. Agentai yra autonomiškos sistemos, kurios veikia kažkurioje aplinkoje ir siekia įvykdyti iš anksto apibrėžtus tikslus. Sprendimų priėmimo realizavimas yra svarbiausia ir sudėtingiausia dalis realizuojant agentines sistemas. Sprendimo priėmimo realizavimui gali būti naudojami logikos skaičiavimai. Šiame darbe ir yra nagrinėjami sekvenciniai skaičiavimai BDI logikoms. BDI logikose, kaip ir kitose modalumo logikose, yra naudojama ciklų paieška išsprendžiamumui gauti. Neefektyvi ciklų paieška užima didesnę išvedimų paieškos resursų dalį. Kai kurioms modalumo logikoms yra žinomi becikliai skaičiavimai ar skaičiavimai naudojantys efektyvią ciklų paiešką. Šiame darbe yra pateikiamas beciklis sekvencinis skaičiavimas KD45 logikai, kuri yra esminis BDI logikų fragmentas. Pateiktas skaičiavimas ne tik eliminuoja ciklų paiešką, bet ir supaprastina patį sekvencijos išvedimą. Skaidaus laiko logikai (kitam BDI logikų fragmentui) yra pateikiamas sekvencinis skaičiavimas naudojantis efektyvią ciklų paiešką. Gauti rezultatai yra pritaikyti sukuriant sekvencinius skaičiavimus vianaagentinei ir daugiaagentinei BDI logikoms. Pristatyti skaičiavimai naudoja tik apribotą ciklų paiešką. Be to, kai kurių tipų ciklus eliminuoja visiškai. Šie rezultatai įgalina kurti efektyvesnes agentines sistemas, paremtas BDI logikomis. / 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.

Automated proof system for logic of correlated knowledge is presented in the dissertation. The system consists of the sequent calculus GS-LCK and the proof search procedure GS-LCK-PROC. Sequent calculus is sound, complete and satisfy the properties of invertibility of rules, admissibility of weakening, contraction and cut. The procedure GS-LCK-PROC is terminating and allows to check if the sequent is provable. Also decidability of logic of correlated knowledge has been proved. Using the terminating procedure GS-LCK-PROC the validity of all formulas of logic of correlated knowledge can be checked. / Automatinė įrodymų sistema koreliatyvių žinių logikai yra pristatoma disertacijoje. Sistemą sudaro sekvencinis skaičiavimas GS-LCK ir įrodymo paieškos procedūra GS-LCK-PROC. Sekvencinis skaičiavimas yra pagrįstas, pilnas ir tenkina taisyklių apverčiamumo, silpninimo, prastinimo ir pjūvio leistinumo savybes. Procedūra GS-LCK-PROC yra baigtinė ir leidžia patikrinti, ar sekvencija yra išvedama. Taip pat buvo įrodytas koreliatyvių žinių logikos išsprendžiamumas. Naudojant baigtinę procedūra GS-LCK-PROC, visų koreliatyvių žinių logikos formulių tapatus teisingumas gali būti patikrintas.

Automatinė įrodymų sistema koreliatyvių žinių logikai yra pristatoma disertacijoje. Sistemą sudaro sekvencinis skaičiavimas GS-LCK ir įrodymo paieškos procedūra GS-LCK-PROC. Sekvencinis skaičiavimas yra pagrįstas, pilnas ir tenkina taisyklių apverčiamumo, silpninimo, prastinimo ir pjūvio leistinumo savybes. Procedūra GS-LCK-PROC yra baigtinė ir leidžia patikrinti, ar sekvencija yra išvedama. Taip pat buvo įrodytas koreliatyvių žinių logikos išsprendžiamumas. Naudojant baigtinę procedūra GS-LCK-PROC, visų koreliatyvių žinių logikos formulių tapatus teisingumas gali būti patikrintas. / Automated proof system for logic of correlated knowledge is presented in the dissertation. The system consists of the sequent calculus GS-LCK and the proof search procedure GS-LCK-PROC. Sequent calculus is sound, complete and satisfy the properties of invertibility of rules, admissibility of weakening, contraction and cut. The procedure GS-LCK-PROC is terminating and allows to check if the sequent is provable. Also decidability of logic of correlated knowledge has been proved. Using the terminating procedure GS-LCK-PROC the validity of all formulas of logic of correlated knowledge can be checked.