文章背景与核心概要
在人工智能和形式化逻辑领域，如何在存在不确定性和默认规则的情况下进行高效、严谨的推理长期以来是一个核心挑战。传统的概率逻辑和答案集编程（ASP）往往需要全局基础化（grounding），这在处理包含函数项的一阶逻辑时极其低效甚至不可行。本文介绍了一种针对查询导向一阶定理证明器 GK 的结构保持定量报告框架，它能够在无需有限全局基础化的前提下，显式处理正负声明、数值置信度以及带例外优先级的默认规则。
该研究的核心技术在于利用保留的证明历史记录执行两项关键计算：一是重建不确定的基础前提，精确计算至少存在一个可用证明的概率，同时避免对共享前提进行独立的重复计算；二是进行支持消解，在传播前对中间原子上的正负支持进行消解，并评估单个规则应用的未决例外条件。最终生成的报告能够清晰地将正支持、负支持、冲突和未知区分开来，并对任何检测到的不完整计算或降级回退进行标记，为复杂逻辑系统中的不确定性管理提供了突破性的解决方案。
Structure-Preserving Uncertainty Propagation in First-Order Proof Search
一阶证明搜索中保持结构的的不确定性传播
Abstract Summary
摘要概要
This paper introduces a structure-preserving quantitative reporting framework for GK, a query-directed first-order prover. Unlike traditional provers, GK integrates explicit positive/negative claims, numerical confidence values, and prioritized default rules with exceptions, handling non-ground clauses (including equality and function terms) without requiring a finite global grounding.
本文引入了一个针对 GK（一种查询导向的一阶定理证明器）的保持结构的的定量报告框架。与传统证明器不同，GK 集成了显式的正/负断言、数值置信度以及带有例外的优先级默认规则，能够在不需要有限全局基础化的前提下处理非基础子句（包括等式和函数项）。
By leveraging retained proof histories, the newly added framework performs two core calculations: 1. Uncertain Ground Premises Reconstruction: Computes the probability that at least one retained proof is available, carefully preventing the independent double-counting of shared premises. 2. Support Resolution: Resolves positive and negative support at intermediate atoms prior to propagation, and evaluates uncertain exception conditions for individual rule applications.
通过利用保留的证明历史，新加入的框架执行两项核心计算： 1. 不确定基础前提重建： 计算至少有一个保留证明可用的概率，同时严谨地防止对共享前提进行独立的重复计算。 2. 支持消解： 在传播之前消解中间原子上的正支持和负支持，并评估单个规则应用的不确定例外条件。
The resulting reports distinctly categorize positive support, negative support, conflict, and ignorance, while flagging any detected incomplete calculations or fallbacks.
由此产生的报告清晰地将正支持、负支持、冲突和未知进行分类，同时标记任何检测到的不完整计算或降级回退。
Paper Metadata
论文元数据
- arXiv ID: arXiv:2608.09190
- Primary Subject: Artificial Intelligence (
cs.AI) - Secondary Subject: Logic in Computer Science (
cs.LO) - Author: Tanel Tammet
- Submitted: August 10, 2026
- Length: 79 pages, 6 figures
- arXiv ID: arXiv:2608.09190
- 主要学科: 人工智能 (
cs.AI)- 次要学科: 计算机科学逻辑 (
cs.LO)- 作者: Tanel Tammet
- 提交时间: 2026年8月10日
- 篇幅: 79 页，6 个图表
Key Features & Implementation
核心功能与实现
- No Global Grounding: Operates via bounded first-order proof searches, handling recursive exception checks dynamically and reporting incomplete searches transparently.
- Granular Reporting: Separates support metrics into positive support, negative support, conflict, and ignorance.
- Comparative Analysis: Compares performance and semantics against probabilistic logic, probabilistic answer set programming (ASP), default logic, and goal-directed ASP (highlighting agreements, semantic variations, and translation gaps).
- Open Source: Executable binaries, comprehensive documentation, examples, and public samplers are available on the GitHub Repository.
- 无全局基础化： 通过有界的一阶证明搜索运行，动态处理递归例外检查，并透明地报告不完整的搜索。
- 细粒度报告： 将支持度量细分为正支持、负支持、冲突和未知。
- 对比分析： 将性能和语义与概率逻辑、概率答案集编程（ASP）、默认逻辑以及目标导向 ASP 进行对比（强调一致性、语义变体和转换差距）。
- 开源： 可执行二进制文件、全面的文档、示例和公共采样器可在 GitHub 仓库 获取。