基于有限词汇的义务行动逻辑自动推理
计算机科学中的逻辑
2014-01-07 v1
摘要
本文进一步研究了我们在先前工作中提出的义务行动逻辑的表列系统。该表列系统使用原子（来自给定的行动项布尔代数）作为公式的标签，这使得我们能够处理并行执行行动和行动补集这两个在其处理上可能存在困难的行动算子。该逻辑的限制之一是它使用具有有限数量行动的词汇。在本文中，我们证明了这一限制不影响演绎系统的协调性；换言之，我们证明了该系统相对于语言扩展是完备的。我们还研究了这一扩展演绎框架的计算复杂性，并证明了该系统的复杂性属于 PSPACE，相较于相关系统有所改进。
引用
@article{arxiv.1401.0969,
title = {Automated Reasoning over Deontic Action Logics with Finite Vocabularies},
author = {Pablo F. Castro and Thomas S. E. Maibaum},
journal= {arXiv preprint arXiv:1401.0969},
year = {2014}
}
备注
In Proceedings LAFM 2013, arXiv:1401.0564