Qiana让逻辑推理能跨上下文和公式，支持含矛盾的推理。
Qiana: A First-Order Formalism to Quantify over Contexts and Formulas with Temporality
- 基于一阶逻辑，可对公式和上下文同时量化
- 支持含矛盾的上下文，能表达如'人人知道阿尔斯所说'的语义
- 兼容现有定理证明器，适合形式化验证与知识建模
我们提出Qiana，一种用于在特定上下文中为真公式的逻辑框架。在Qiana中，可对公式和上下文进行量化，以表达‘每个人都知道爱丽丝所说的一切’等语义。该框架允许上下文内存在不一致，即容许矛盾共存。此外，Qiana建立在一阶逻辑基础上，具有有限公理化性质，因此其理论可与现有的一阶逻辑定理证明器兼容。我们展示了Qiana如何表示时间性、事件演算和模态逻辑，并讨论了其不同设计选择。
原文摘要 · Abstract (English)
We introduce Qiana, a logic framework for reasoning on formulas that are true only in specific contexts. In Qiana, it is possible to quantify over both formulas and contexts to express, e.g., that ``everyone knows everything Alice says''. Qiana also permits paraconsistent logics within contexts, so that contexts can contain contradictions. Furthermore, Qiana is based on first-order logic, and is finitely axiomatizable, so that Qiana theories are compatible with pre-existing first-order logic theorem provers. We show how Qiana can be used to represent temporality, event calculus, and modal logic. We also discuss different design alternatives of Qiana.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。