Structure-Preserving Uncertainty Propagation in First-Order Proof Search

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.

The main contributions are:

1. a retained-proof calculation that reconstructs the uncertain ground premises used by each proof and avoids double-counting premises shared by several proofs;

2. a dependency-aware calculation that resolves positive and negative support before propagation and evaluates uncertain exceptions for individual rule applications;

3. a bounded implementation that reports which calculation was used and marks detected fallbacks and unsupported cases; and

4. analytic, simulation, and system-comparison results that identify the fragments on which the calculations agree with their reference semantics and with other implemented systems.

The paper defines two separate reference models. Ground-instance activation (Model 1) models the availability of uncertain clause instances. Shared-threshold semantics (Model 2) models the usable support at ground atoms. GK first constructs a retained-proof result and attempts the dependency-aware calculation when it detects a contested ground atom. A completed dependency-aware result replaces the retained-proof result; otherwise the retained-proof result is returned directly or as a flagged fallback. The selected calculation and its status are therefore part of the interpretation of each answer row. Different rows in one run may be produced by different calculations.

For Model 1, an uncertain input clause C and a ground substitution θ define an activation event eC,θ = the ground instance Cθ is active, with probability equal to the input confidence on C. Distinct input-clause occurrences and distinct resulting ground instances define independent events; instances with confidence one are always active. If two substitutions produce the same syntactic ground instance of the same identified clause occurrence, they name one activation event. A derivation is available exactly when every activation event of the ground clause instances it uses holds. A ground-instance activation world is constructed by grounding, deleting each uncertain ground instance with probability 1-p, and deciding derivability using a query-ancestry requirement that discards contradictions derived wholly from the knowledge base. The model’s primary quantities are the activation probabilities Pact(Q), Pact(¬Q), and their difference.

For Model 2, no clause is deleted. A support contribution is the value supplied to a conclusion literal by one directed application when its body has the required usable states and its exception condition does not disable the application. For a ground atom A, the positive support pool before opposition aggregates contributions concluding A, and the negative support pool before opposition aggregates contributions concluding ¬A. To pool same-polarity contributions ri, combine them as 1 - ∏i(1 - ri). The pooled values a and b are support before opposition resolution. The reported components s+ and s- contain only support surviving opposition; conflict is recorded in c. Once the two pooled values are a and b, A is positively usable when its positive support is active and its negative support is not; it is negatively usable when the converse holds. In the conflict and ignorance regions, neither polarity is usable as a premise of a downstream application. A shared-threshold world is defined by grounding and orienting, drawing a shared uniform threshold UA for every ground atom A, and evaluating every directed application in dependency order. The four reported components are the probabilities of the four regions at the query atom: s+ = max(0, a-b), s- = max(0, b-a), c = min(a,b), g = 1 - max(a,b). Signed confidence is C(L) = s+(L) - s-(L).

The paper proves several propositions. Proposition 1 shows the four quantities are non-negative, sum to one, and at most one of s+ and s- is non-zero. Proposition 2 shows the shared-threshold coupling attains the Fréchet lower bound on unopposed support, with the signed confidence a-b independent of the unknown coupling. Proposition 3 shows that for a single contested premise, R(H) = r max(a-b, 0), 0, 0, 1 - r max(a-b, 0), so equal opposing premise support yields pure ignorance at the conclusion. Proposition 4 shows conditional-support preservation for blocked and unblocked classes. Proposition 5 shows local partitions and deterministic limits for the family of local combination rules. Proposition 6 establishes dependency-evaluator correspondence for queries within the correspondence fragment. Corollary 7 shows polarity invariance of completed reports: R(¬A) = (s-(A), s+(A), c(A), g(A)).

For defaults, a default application has three components: the usable state of its ordinary body, the usable state of its exception condition, and the rule confidence applied when the exception does not block it. In a shared-threshold world, the body and exception are evaluated first. If the body is not usable, the application contributes nothing. If the body is usable and the exception is positively usable, the default is blocked. Otherwise the rule contributes its stated confidence to the head’s support pool. Evidence for the explicit negation of the exception condition does not support the head directly; it only reduces the region in which the exception blocks the rule. The paper distinguishes arbitrary exceptions (undercutting attacks) from contrary-gated defaults where the exception is the negation of the head (rebutting attacks). For contrary-gated defaults, an auxiliary gate threshold VA is drawn independently of UA. The paper defines local rules for ordinary support vs. ordinary support, contrary-gated default vs. ordinary support, two equally ranked contrary-gated defaults (mutual blocking), and strict-priority override for unequally ranked defaults. Priority-zero defaults are treated as unranked, and reciprocal priority-zero pairs have their internal exception edges removed.

The implementation computes GK reports after proof search. The retained-proof calculation uses activation-event identifiers reconstructed by replaying proof histories. The proof-availability event of a derivation D is the joint event that every event in its activation-event set SD holds, with probability ∏e∈SD pe. Combining retained proofs uses inclusion-exclusion: P(∪i ADi) = ∑∅≠I⊆ 1,...,m (-1)I+1 ∏e∈∪i∈I SDi pe. This is sensitive to overlap, so two proofs with the same event set contribute as one, proofs with disjoint event sets combine by noisy-or, and partially overlapping proofs fall between. The dependency-aware calculation uses a separate report-time traversal of the clausified knowledge base to collect all directed positive and negative derivations at each contested ground atom, including shared dependency sets. It then enumerates configurations, pools each polarity, preserves shared predecessors, and applies the shared-threshold opposition resolution.

The evaluation uses two sampler families: the clause-activation sampler (CA) implementing Model 1 and the shared-threshold sampler (ST) implementing Model 2. The shared-threshold suite contains examples Y1–Y18, two variants, and two trace checks, comparing 54 scalar frequencies with analytic values at 400,000 worlds per case. The example suite produced 43 answer rows. GK and shared-threshold results agree on all supported cases within Monte Carlo tolerance. The paper identifies model differences (contested premises), coverage limits (open premises, recursive rules), and directed-reading limitations (no contraposition). The system comparison includes ProbLog, PASTA, plingo, smProbLog, TweetyProject, clingo, DLV, I-DLV, and s(CASP). The comparison distinguishes exact translations, approximate analogues, unsupported translations, and incomplete runs. Reports retain each system’s native output type; the comparison does not convert them to one score.

The paper concludes that GK now retains the identities of uncertain premises while combining proofs and resolves opposing support before it is propagated. Uncertain exceptions are evaluated for the rule applications they can block. Reports separate positive support, negative support, conflict, and ignorance and identify detected incomplete calculations. The retained-proof calculation reproduces proof-union probabilities on the tested complete proof sets. The dependency-aware calculation agrees with the shared-threshold reference model on its stated finite fragment. Comparisons with other reasoners show agreement on the one-sided and deterministic fragments with the same independent-choice and proof-union semantics, and different outputs when the systems use different semantics for opposition, defaults, or multiple models. The implementation remains bounded, and remaining work includes broader replay coverage, proof-guided completion of open premises, provenance-aware aggregation in the threshold-world sampler, a stated criterion for choosing between credulous and skeptical cycle policies, and empirical calibration of input confidences.

Improvements to AI Systems:

1. Uncertainty-Aware Reasoning with Conflict Resolution

• Implement a reasoning module that tracks both positive and negative support for claims, explicitly separating conflict (both supports active) and ignorance (neither active) from clear conclusions.

• The system can output quadruples (s+, s-, c, g) instead of single confidence scores, enabling downstream decision-making to distinguish evidence for, evidence against, contradictory evidence, and no evidence.

2. Proof-Overlap-Aware Confidence Aggregation

• Replace naive probabilistic combination (e.g., noisy-OR) with inclusion-exclusion over shared activation events from proof histories.

• The system avoids double-counting shared premises across multiple proofs, producing more accurate confidence estimates for conclusions supported by overlapping or partially redundant derivations.

3. Dependency-Aware Propagation with Exception Handling

• Before propagating support through rules, resolve opposition at intermediate atoms using a shared-threshold coupling (Fréchet bounds).

• The system can evaluate uncertain exception conditions per rule application, blocking defaults only when the exception is positively usable, and distinguishing undercutting (arbitrary exceptions) from rebutting (contrary-gated) attacks.

4. Bounded, Incomplete-Search Transparency

• Integrate a report-time reconstruction of proof histories and dependency traversals that flags incomplete calculations or fallbacks (e.g., when dependency-aware resolution is not feasible).

• The system explicitly marks each answer row with the calculation method used (retained-proof vs. dependency-aware) and its status (complete, fallback, unsupported), enabling users to trust or re-query based on computational limits.

5. Polarity-Invariant Reasoning

• Enforce that the report for a negated query is the polarity-swapped report of the original query (Corollary 7).

• The system can maintain consistency when answering both positive and negative queries, avoiding asymmetric biases in question-answering or contradiction detection.

6. Default Logic with Priority and Mutual Blocking

• Implement prioritized defaults with strict-priority override and mutual blocking for equally ranked defaults, using independent gate thresholds for contrary-gated rules.

• The system can handle non-monotonic reasoning where new evidence can retract conclusions, and can model defeasible knowledge with explicit exception conditions.

7. Reference-Semantics Validation

• Use the two sampler families (clause-activation and shared-threshold) as internal consistency checks for the reasoning engine.

• The system can self-validate its outputs against Monte Carlo simulations on finite fragments, detecting semantic drift or implementation bugs in real time.

8. Cross-System Semantic Comparison

• Adopt the paper’s taxonomy (exact translation, approximate analogue, unsupported, incomplete) when integrating outputs from other probabilistic/logic systems (e.g., ProbLog, ASP solvers).

• The system can transparently report when its semantics differ from other tools, preventing silent misinterpretation of results in multi-system pipelines.

What the Improved AI System Can Do:

• Answer queries with nuanced uncertainty reports that separate evidence polarity, conflict, and ignorance, rather than a single probability.

• Combine multiple proofs without overcounting shared evidence, improving calibration in domains like medical diagnosis or legal reasoning.

• Reason with defaults and exceptions, handling contradictory rules gracefully and explaining whether a conclusion is blocked, supported, or unknown.

• Operate under bounded resources, explicitly stating when its reasoning is incomplete or relies on a fallback, enabling safe deployment in time-critical applications.

• Maintain logical consistency across negated queries and support non-monotonic inference with priorities.

• Validate its own outputs against reference models and compare semantics with other AI reasoners, facilitating integration in heterogeneous AI systems.