A Resolution Prover for Coalition Logic
A Resolution Prover for Coalition Logic
复制标题
DOI：
10.4204/eptcs.146.9
复制
发表时间：
2014-04
期刊：
影响因子：
2.9
通讯作者：
C. Nalon;Lan Zhang;C. Dixon;U. Hustadt
中科院分区：
文献类型：
--
作者：
C. Nalon;Lan Zhang;C. Dixon;U. Hustadt
我们提出了一个用于联合逻辑自动推理的原型工具，联合逻辑是一种非正态模态逻辑，可用于合作代理的推理。定理证明器CLProver基于最近对联盟逻辑的基于分辨率的演算的研究，该演算处理联盟问题，这是联盟逻辑的一种标准形式。我们提供了联盟问题和基于决议的联盟逻辑演算的概述。然后，我们给出CLProver实现的细节，并将结果与现有的基于表的求解器进行比较。
We present a prototype tool for automated reasoning for Coalition Logic, a non-normal modal logic that can be used for reasoning about cooperative agency. The theorem prover CLProver is based on recent work on a resolution-based calculus for Coalition Logic that operates on coalition problems, a normal form for Coalition Logic. We provide an overview of coalition problems and of the resolution-based calculus for Coalition Logic. We then give details of the implementation of CLProver and present the results for a comparison with an existing tableau-based solver.