用计算语义建模认知态度，支持心理概念精准表达与动态推理。
A Computationally Grounded Framework for Cognitive Attitudes (extended version)
- 基于信念库构建五类模态算子，刻画认知与动机状态。
- 证明算子间不可互表，可组合表示矛盾、偏好等复杂心理状态。
- 提供可判定的模型检测算法，适用于心理推理系统验证。
我们提出一种新型语言，用于形式化推理智能体的认知态度，涵盖认识论与动机性两类。通过基于信念库的计算语义进行解释，语言包含五类模态算子：隐含信念、完全吸引、完全排斥、现实吸引与现实排斥。我们给出了公理化体系，证明这些算子彼此不可互表，并可组合表示多种心理概念，如矛盾、漠然、动机存在与缺失、偏好等。进一步扩展语言以支持信念变化操作的动态推理。最后，给出语言的简洁模型检测表述，并基于TQBF归约实现一个PSPACE复杂度的模型检测算法。在具体实例上展示了算法的计算时间实验结果。
原文摘要 · Abstract (English)
We introduce a novel language for reasoning about agents' cognitive attitudes of both epistemic and motivational type. We interpret it by means of a computationally grounded semantics using belief bases. Our language includes five types of modal operators for implicit belief, complete attraction, complete repulsion, realistic attraction and realistic repulsion. We give an axiomatization and show that our operators are not mutually expressible and that they can be combined to represent a large variety of psychological concepts including ambivalence, indifference, being motivated, being demotivated and preference. We present a dynamic extension of the language that supports reasoning about the effects of belief change operations. Finally, we provide a succinct formulation of model checking for our languages and a PSPACE model checking algorithm relying on a reduction into TQBF. We present some experimental results for the implemented algorithm on computation time in a concrete example.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。