Structure-Preserving Uncertainty Propagation in First-Order Proof Search

• URL: http://arxiv.org/abs/2608.09190v1
• Date: Mon, 10 Aug 2026 07:00:55 GMT
• Title: Structure-Preserving Uncertainty Propagation in First-Order Proof Search
• Abstract summary: GK is a query-directed first-order prover that extends ordinary resolution-based proof search.<n>It works directly with non-ground clauses, including equality and function terms.<n>This paper adds structure-preserving quantitative reporting to that framework.
• Score: 0.2538209532048867
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Autoformalizing Argumentative Material Inferences [26.35292656634472]
  We develop an autoformalization for argumentative material inference as guard completion.<n>GUARD yields significant improvements in verified-faithful.<n>We show that the symbolic soft critique and the explicit assumption layer account for most of these gains.
  arXiv  Detail & Related papers  (2026-09-15T11:05:26Z)
• Compute-Bounded Security Assurance - Coverage, Verification, and Response under Resource Constraints [0.0]
  Additional inference compute can increase the number of correctly resolved security-assurance tasks.<n>We develop a resource-constrained framework that separates success, unique coverage, accepted evidence, and operational protection.<n>A conceptual defensive architecture separates evidence analysis, adjudication, and operational authority.
  arXiv  Detail & Related papers  (2026-09-07T13:07:55Z)
• When benchmark inferences do not compose: Projectibility in AI evaluation [0.0]
  An AI benchmark result rarely reaches a consequential claim in one step.<n>Evaluators generalize it to further cases, interpret it as evidence of capability, extrapolate it to new tasks, transport it to another system or site.<n>This paper identifies a further problem: warranted links don't automatically make a warranted chain.
  arXiv  Detail & Related papers  (2026-07-28T18:07:04Z)
• Before the Action: Benchmarking LLMs on Prospective Hypothesis Discovery [95.44432473367836]
  Large language models (LLMs) excel at answering pre-specified questions, yet their ability to navigate the open-ended, pre-conclusion stage of discovery remains largely unmeasured.<n>We introduce Prospective Hypothesis Discovery (PHD), which asks models to autonomously construct grounded, discnative, and testable hypothesis spaces from inconclusive evidence.<n>We introduce HypoArena, comprising HypoData, a benchmark of 988 cases across six scientific and analytical domains, and HypoEval, an evaluation framework for open-ended hypothesis sets.
  arXiv  Detail & Related papers  (2026-07-17T08:56:43Z)
• Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification [0.0]
  Self-composition reduces information-flow verification to safety checking over two circuit copies.<n>Recent PDR-based techniques exploit this duplicated structure through copy symmetry and global cross-copy equivalence predicates.<n>We introduce guarded equivalence predicates to expose these relations to PDR.
  arXiv  Detail & Related papers  (2026-06-20T14:25:13Z)
• Finite Resources False Discovery Rate Control in Structured Hypothesis Spaces [47.16593717985932]
  We present a framework for controlling the false discovery rate when each hypothesis is evidenced only by a finite count of null draws.<n>We present two decision rules that are both robust to structural mis-specification, yet offer a distinct trade-off between exact FDR control and statistical power.
  arXiv  Detail & Related papers  (2026-06-13T16:56:52Z)
• Finite Certificates for In-Context Determinacy and a Threshold Theory of Emergence in Language Models [0.2864713389096699]
  This paper develops a model-theoretic framework for verifying context-conditioned language-model behavior.<n>It provides finite context certificates, pair-separator hitting sets, query teaching dimension, prompt-preservation criteria, and scale-limit witnesses.
  arXiv  Detail & Related papers  (2026-05-30T14:07:58Z)
• Exact Structural Abstraction and Tractability Limits [0.0]
  Exact correctness depends only on the induced classes $s sim_R simation' iff mathrmAdm_R(s)$.<n>Decision, search, approximation, statistical, randomized horizon, and distributional guarantees all reduce to this same quotient-recovery problem.
  arXiv  Detail & Related papers  (2026-04-08T17:59:47Z)
• Mitigating LLM Hallucinations via Conformal Abstention [70.83870602967625]
  We develop a principled procedure for determining when a large language model should abstain from responding in a general domain. We leverage conformal prediction techniques to develop an abstention procedure that benefits from rigorous theoretical guarantees on the hallucination rate (error rate) Experimentally, our resulting conformal abstention method reliably bounds the hallucination rate on various closed-book, open-domain generative question answering datasets.
  arXiv  Detail & Related papers  (2024-04-04T11:32:03Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  Cross-modal Retrieval methods build similarity relations between vision and language modalities by jointly learning a common representation space. However, the predictions are often unreliable due to the Aleatoric uncertainty, which is induced by low-quality data, e.g., corrupt images, fast-paced videos, and non-detailed texts. We propose a novel Prototype-based Aleatoric Uncertainty Quantification (PAU) framework to provide trustworthy predictions by quantifying the uncertainty arisen from the inherent data ambiguity.
  arXiv  Detail & Related papers  (2023-09-29T09:41:19Z)
• Sequential Predictive Two-Sample and Independence Testing [114.4130718687858]
  We study the problems of sequential nonparametric two-sample and independence testing. We build upon the principle of (nonparametric) testing by betting.
  arXiv  Detail & Related papers  (2023-04-29T01:30:33Z)
• Nested Counterfactual Identification from Arbitrary Surrogate Experiments [95.48089725859298]
  We study the identification of nested counterfactuals from an arbitrary combination of observations and experiments. Specifically, we prove the counterfactual unnesting theorem (CUT), which allows one to map arbitrary nested counterfactuals to unnested ones.
  arXiv  Detail & Related papers  (2021-07-07T12:51:04Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.