将认知ATL的有效性归约到认知CTL的有效性
计算机科学中的逻辑
2013-03-05 v1 人工智能
多智能体系统
摘要
我们提出从认知交替时态逻辑(ATL)的一个子集到认知计算树逻辑(CTL)的保有效性翻译。所考虑的认知ATL子集已知具有有限模型性质和可判定的模型检测。这意味着有效性的可判定性，但隐含的算法不可行。将有效性问题归约到相应CTL系统中的有效性问题，使得该逻辑的自动推理技术可用于处理表面上更复杂的ATL系统。
引用
@article{arxiv.1303.0794,
title = {Reducing Validity in Epistemic ATL to Validity in Epistemic CTL},
author = {Dimitar P. Guelev},
journal= {arXiv preprint arXiv:1303.0794},
year = {2013}
}
备注
In Proceedings SR 2013, arXiv:1303.0071