Structure-Preserving Uncertainty Propagation in First-Order Proof Search
2026-08-10 • Artificial Intelligence
Artificial IntelligenceLogic in Computer Science
AI summaryⓘ
The authors present GK, a first-order logic prover that uses both positive and negative claims, confidence levels, and prioritized default rules with exceptions to find proofs without fully grounding all variables. Their approach allows incomplete searches to be clearly reported and uses proof histories to calculate the overall probability that a proof exists while accounting for shared premises. They also analyze how positive and negative evidence supports intermediate conclusions and detect conflicts or uncertainty in the reasoning process. The paper compares GK to other logical frameworks and demonstrates its calculations through examples and simulations.
first-order logicresolution proof searchdefault logicnon-ground clausesproof confidencebounded searchuncertainty quantificationexception handlingprobabilistic logicproof dependencies
Authors
Tanel Tammet
Abstract
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.