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...
Saved in:
Main Author: | |
---|---|
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 |