用于混合PDL的带全局缓存的ExpTime表
计算机科学中的逻辑
2017-05-03 v1
摘要
我们提出了首个具有ExpTime复杂度的直接表决策过程，用于HPDL（混合命题动态逻辑）。它检查HPDL中给定的ABox（有限断言集）是否可满足。在技术层面，它将全局缓存与事件性条件的满足检查以及标称的处理相结合。我们的过程包含足够细节以直接实现，并已在TGC2（带全局缓存的表）系统中实现。由于HPDL可用作表示和推理术语知识的描述逻辑，我们的过程对实际应用很有用。
引用
@article{arxiv.1705.00848,
title = {ExpTime Tableaux with Global Caching for Hybrid PDL},
author = {Linh Anh Nguyen},
journal= {arXiv preprint arXiv:1705.00848},
year = {2017}
}