发表机构
Tallinn University of Technology（塔林理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究针对一阶证明器GK框架，提出结构保留型不确定性传播方法，通过重构基前提、解析正负支持等计算，实现带不确定性的证明报告，经实验验证其有效性并与相关逻辑系统对比。
AI 中文摘要
GK是一种查询导向的一阶证明器，它将普通的基于归结的证明搜索扩展为包含显式正负断言、数值置信值以及带例外的优先默认规则，可直接处理非基子句，包括等式和函数项。它通过有界一阶证明搜索寻找候选证明，默认规则的例外条件则通过进一步的有界搜索进行检查，当例外本身依赖于默认规则时会递归执行，这避免了对有限全局基例化的需求，同时允许将不完整搜索结果明确报告。本文在该框架中加入了结构保留型定量报告：保留的证明历史用于两项计算，第一项重构每个证明所用的不确定基前提，并计算至少存在一个保留证明的概率（不独立计数共享前提）；第二项在中间原子处解析正负支持，再将该支持传播至后续规则，相同计算还可评估单个规则应用的不确定例外条件。报告区分正支持、负支持、冲突与无知状态，并标识检测到的不完整计算或 fallback。实现过程在证明搜索后执行有界重构和依赖遍历，仍无需全局基例化。分析示例与独立模拟器在其声明的片段上复现了参考计算，与概率逻辑、概率ASP、默认逻辑及目标导向ASP的比较识别出一致情况、语义差异、不支持的翻译及不完整计算的案例。
英文摘要
GK is a query-directed first-order prover that extends ordinary resolution-based proof search with explicit positive and negative claims, numerical confidence values, and prioritized default rules with exceptions. It works directly with non-ground clauses, including equality and function terms. Candidate proofs are found by bounded first-order proof search; exception conditions of defaults are checked by further bounded searches, recursively when exceptions themselves depend on defaults. This avoids requiring a finite global grounding, while allowing incomplete searches to be reported as such. This paper adds structure-preserving quantitative reporting to that framework. Retained proof histories are used in two calculations. The first reconstructs the uncertain ground premises used by each proof and computes the probability that at least one retained proof is available, without counting shared premises independently. The second resolves positive and negative support at intermediate atoms before that support is propagated through later rules; the same calculation evaluates uncertain exception conditions for individual rule applications. Reports separate positive support, negative support, conflict, and ignorance and identify detected incomplete calculations or fallbacks. The implementation performs bounded reconstruction and dependency traversal after proof search and still requires no global grounding. Analytic examples and independent simulators reproduce the reference calculations on their stated fragments. Comparisons with probabilistic logic, probabilistic ASP, default logic, and goal-directed ASP identify cases of agreement, semantic difference, unsupported translation, and incomplete computation.
Comments79 pages, 6 figures. Executable binaries, documentation, examples, and public samplers: https://github.com/tammet/gkreasoner
