首个完备的直觉逻辑推理系统，支持不确定信息处理。
Implementing the First-Order Logic of Here and There
- 基于自然演绎与嵌入法构建高效证明器
- 在大规模测试集上验证了可靠性和效率
- 适合逻辑研究者和形式化验证工程师
本文提出针对一阶此处与彼处逻辑（HT）的自动化定理证明系统。其核心方法包括：基于原生序言演算的分析性证明搜索，通过自由变量和斯科伦化优化；以及将HT逻辑嵌入直觉逻辑，并结合直觉逻辑的序言、表格和连接演算。所有证明器均在一个大规模一阶公式基准集上进行评估，为后续更高效的HT证明器开发奠定基础。
原文摘要 · Abstract (English)
We present automated theorem provers for the first-order logic of here and there (HT). They are based on a native sequent calculus for the logic of HT and an axiomatic embedding of the logic of HT into intuitionistic logic. The analytic proof search in the sequent calculus is optimized by using free variables and skolemization. The embedding is used in combination with sequent, tableau and connection calculi for intuitionistic first-order logic. All provers are evaluated on a large benchmark set of first-order formulas, providing a foundation for the development of more efficient HT provers.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。