Efficient decision procedure for Belief modality

This paper defines decision algorithm for subclass of BKD45DKDIKD logic which is based on known algorithm for temporal BKD45DKDIKD logic [2]. BDI logics are widely used in agent based systems. Such usage of BDI logic can be found in [1]. The original decision algorithm uses loop-check technique for...

Full description

Saved in:
Bibliographic Details
Main Author: Adomas Birštunas
Format: Article
Language:English
Published: Vilnius University Press 2005-12-01
Series:Lietuvos Matematikos Rinkinys
Subjects:
Online Access:https://www.journals.vu.lt/LMR/article/view/26673
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1832593212282241024
author Adomas Birštunas
author_facet Adomas Birštunas
author_sort Adomas Birštunas
collection DOAJ
description This paper defines decision algorithm for subclass of BKD45DKDIKD logic which is based on known algorithm for temporal BKD45DKDIKD logic [2]. BDI logics are widely used in agent based systems. Such usage of BDI logic can be found in [1]. The original decision algorithm uses loop-check technique for BEL and temporal operators. Applied loop-check technique is not optimized and therefore loop-check takes most of the time used in decision algorithm. Some examples of efficient loop-check applications for logic KT, S4 and some subclasses of intuitionistic logic can be found in [4]. Another efficient loop-check can be found in work [3]. We concentrate on our attitude on loop-check optimization for BEL operator. This paper defines decision algorithm modification, which uses efficient loop-check for BEL operator, but do not effect performance of other parts of algorithm. We define optimization only for BEL operator and therefore we omit temporal operators in this paper.
format Article
id doaj-art-a121399d78764d989af8ee6bd9bcfc15
institution Kabale University
issn 0132-2818
2335-898X
language English
publishDate 2005-12-01
publisher Vilnius University Press
record_format Article
series Lietuvos Matematikos Rinkinys
spelling doaj-art-a121399d78764d989af8ee6bd9bcfc152025-01-20T18:15:51ZengVilnius University PressLietuvos Matematikos Rinkinys0132-28182335-898X2005-12-0145spec.10.15388/LMR.2005.26673Efficient decision procedure for Belief modalityAdomas Birštunas0Vilniaus University This paper defines decision algorithm for subclass of BKD45DKDIKD logic which is based on known algorithm for temporal BKD45DKDIKD logic [2]. BDI logics are widely used in agent based systems. Such usage of BDI logic can be found in [1]. The original decision algorithm uses loop-check technique for BEL and temporal operators. Applied loop-check technique is not optimized and therefore loop-check takes most of the time used in decision algorithm. Some examples of efficient loop-check applications for logic KT, S4 and some subclasses of intuitionistic logic can be found in [4]. Another efficient loop-check can be found in work [3]. We concentrate on our attitude on loop-check optimization for BEL operator. This paper defines decision algorithm modification, which uses efficient loop-check for BEL operator, but do not effect performance of other parts of algorithm. We define optimization only for BEL operator and therefore we omit temporal operators in this paper. https://www.journals.vu.lt/LMR/article/view/26673BDI logicloop-checksequent calculus
spellingShingle Adomas Birštunas
Efficient decision procedure for Belief modality
Lietuvos Matematikos Rinkinys
BDI logic
loop-check
sequent calculus
title Efficient decision procedure for Belief modality
title_full Efficient decision procedure for Belief modality
title_fullStr Efficient decision procedure for Belief modality
title_full_unstemmed Efficient decision procedure for Belief modality
title_short Efficient decision procedure for Belief modality
title_sort efficient decision procedure for belief modality
topic BDI logic
loop-check
sequent calculus
url https://www.journals.vu.lt/LMR/article/view/26673
work_keys_str_mv AT adomasbirstunas efficientdecisionprocedureforbeliefmodality