Pith. sign in

REVIEW 5 minor 1 cited by

Structure-Preserving Uncertainty Propagation in First-Order Proof Search

T0 review · 0 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A first-order prover now computes uncertainty reports from retained proof histories, counting shared premises once and resolving opposing support at the atom where it occurs, without grounding the knowledge base.

desk verdict A genuine, carefully scoped extension of GK; accept with close checking of the fragment conditions. read the letter →

arxiv 2608.09190 v1 pith:UD7ITEK4 submitted 2026-08-10 cs.AI cs.LO

Tanel Tammet This is my paper · ORCID
classification cs.AIcs.LO
keywords first-ordertheoremprovinguncertaintypropagationproofprovenancedefaultruleswithexceptionsshared-thresholdsemanticsprobabilisticlogicprogrammingnonmonotonicreasoningdependency-awareevaluation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that a query-directed first-order theorem prover can produce quantitative uncertainty reports without grounding the whole knowledge base, by keeping proof histories and re-analyzing them after proof search. One calculation reconstructs the uncertain ground premises each proof actually used and computes the probability that at least one retained proof is available, counting shared premises once instead of once per proof. A second, dependency-aware calculation resolves positive versus negative support at the atom where the opposition occurs before that atom is used by later rules, and reports four components: unopposed positive support, unopposed negative support, conflict, and ignorance. The same mechanism evaluates uncertain exception conditions of default rules. If the paper's formal correspondence holds, these reports are exact region probabilities of a defined shared-threshold semantics on a finite acyclic fragment, while bounded search flags incomplete calculations instead of hiding them.

What carries the argument

The carrying objects are retained proof-history DAGs with activation-event identifiers, each naming an identified input-clause occurrence together with the ground instance it was used at, and the report-time directed dependency graph built from the clausified knowledge base. The retained-proof calculation uses inclusion-exclusion over activation-event sets (Equation (11)) so that shared premises are counted once. The dependency-aware calculation pools same-polarity support by noisy-or, then applies one shared Uniform(0,1) threshold per ground atom to both polarities, producing the four-region partition of Equation (2): (max(a-b,0), max(b-a,0), min(a,b), 1-max(a,b)). Contrary-gated defaults add an independent auxiliary threshold, and priorities assign overlap regions by rank. This machinery carries the argument because it replaces both double-counted scalar proof values and deferred query-level opposition with atom-level region measures computed from reconstructed ground instances.

What would settle it

Run the contested-premise example 0.5::bird(a), 0.5::¬bird(a), 0.9::flies(a)←bird(a) through a Monte Carlo sampler that draws independent thresholds for the two polarities. The independent-coupling positive support is 0.5·0.5·0.9 = 0.225, whereas the paper's shared-threshold report is (0,0,0,1); if an implementation returns the independent value on this input while claiming a completed dependency-aware result, the claimed shared-threshold semantics is not what is computed.

Watch

Extended reading notes

Core claim

GK's central claim is that provenance-aware reporting can be layered onto bounded first-order proof search without changing the search's clauses or requiring a finite global grounding. Retained proof histories are replayed to recover the ground instances of uncertain input clauses used by each derivation; same-polarity proofs are combined by inclusion-exclusion over activation-event sets, so a premise shared by two proofs is counted once. When a ground atom is potentially two-sided, a separate report-time traversal builds a bounded directed dependency graph and applies shared-threshold semantics: same-polarity contributions are pooled by noisy-or and the two pools are compared against one shared Uniform(0,1) threshold per atom, partitioning the query atom's sample space into positive-only, negative-only, conflict, and ignorance regions; uncertain exception conditions are evaluated in the same framework as usable-region probabilities rather than subtracted from rule confidence. Proposition 6 states that within the correspondence fragment, which requires a finite acyclic relevant graph, supported inference forms, and complete enumeration, the evaluator returns exactly the measures induced by the shared-threshold world definition, and the reported evaluation shows all 54 scalar frequencies within Monte Carlo precision of their closed forms.

Load-bearing premise

The reported numbers depend on a stipulated coupling: positive and negative support at an atom are resolved with one shared random threshold, and contrary-gated defaults get an independent auxiliary threshold; choose a different coupling and the reported four components change.

Editorial extensions

If this is right

  • On one-sided derivations where each uncertain instance is used at most once, both reference semantics and the exact-translation comparisons return the same query values, so the new calculations reduce to standard probabilistic proof combination on that fragment.
  • A premise with equal opposing support no longer yields a propagated value like 0.45; the rule does not fire and the conclusion is reported as pure ignorance with the contested atom identified.
  • Two proofs sharing uncertain premises are combined as one union event rather than as independent noisy-or sources, and a duplicated proof contributes nothing beyond the original.
  • Default exceptions act as undercutting conditions: support for an exception condition reduces the rule's usable region but does not directly support the opposite conclusion, which instead enters the opposing pool.
  • Because the calculations run after bounded proof search and traverse only query-relevant ground instances, inputs with function terms and large irrelevant constant sets still produce reports, with fallback flags when reconstruction or traversal cannot complete.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same dependency graph could also emit the full coupling interval [max(0,a-b), min(a,1-b)] instead of only the shared-threshold lower bound, giving users a built-in sensitivity report on the opposition assumption.
  • Because the four-component report is computed from reconstructed ground instances, it could be extended to report which shared predecessors contributed to conflict, turning contested-atom identification into a fuller explanation trace.
  • The usable-region treatment of exceptions suggests a quantitative bridge to structured argumentation: undercutting attacks become conditional probabilities of blocked applications, while rebutting attacks enter the opposite pool; one testable extension would learn exception strength rather than stipulate it.
  • If the correspondence proposition holds, then on every finite acyclic query with one-sided rules GK's report should coincide with distribution-semantics query probabilities, while on contested-premise queries it should deliberately differ; users comparing systems should align the coupling choice before treating numerical differences as disagreements.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 5 minor

Summary. The paper extends the GK first-order resolution prover with two post-search quantitative report calculations. The first recomputes the probability that at least one retained proof is available, reconstructing ground activation events so that premises shared by several proofs are counted once. The second defines a shared-threshold semantics over directed ground applications and computes four region probabilities — positive support, negative support, conflict, and ignorance — by a report-time dependency traversal. The paper proves local algebraic properties (Propositions 1–5), states a conditional correspondence between the dependency-aware evaluator and the shared-threshold semantics (Proposition 6), and evaluates the implementation with analytic examples, Monte Carlo samplers, and comparisons with ProbLog, PASTA, plingo, smProbLog, TweetyProject, clingo, DLV, I-DLV, and s(CASP). It also contains an extensive and unusually explicit limitation section.

Significance. If the conditional claims are taken at face value, the contribution is significant for query-directed first-order reasoning with uncertainty and defaults: the system avoids global grounding, keeps conflict distinct from ignorance, and preserves shared dependencies in proof combination. The manuscript is also unusually careful in several respects: the shared-threshold semantics is presented as an authored postulate rather than an empirical finding; the shared-threshold sampler is a separate code base that does not call the reasoner; the clause-activation sampler's missing completion counts are disclosed and its values are not treated as semantic estimates; the status taxonomy distinguishes completed shared-threshold results from proof-pool decompositions; and Section 11 lists silent failure modes such as unflagged factoring and coarse dependency-index merging. The main caveat is that the reported agreement between GK and the samplers is internal consistency: the samplers implement the same defined semantics, so the evaluation validates implementation consistency and analytic arithmetic rather than providing independent confirmation of the semantics against an external model.

minor comments (5)
  1. [Section 5.4.3] The general statement in Section 5.4.1 that conflicted and ignorant exception states do not block a default is not applied in the contrary-gated case: there the default is blocked whenever the ordinary opposing pool is active, including the region UA ≤ min(a,b) that would otherwise be classified as conflict. Please add an explicit sentence stating that the contrary-gated local rule overrides the general exception-blocking rule, since a reader applying the general sentence would obtain different tuples.
  2. [Section 5.2.2, Proposition 2] The sensitivity interval [max(0,a−b), min(a,1−b)] is an interval for P(E+ \ E-), not for the reported s+ component; the shared-threshold report itself is a point value under the maximal-overlap coupling. Consider stating this explicitly near the interval, because the current wording could be read as making the report interval-valued.
  3. [Section 6.6 and Table 8] The paper-level codes such as RP/out and DA/in are not all emitted by the implementation; Example 12 is a row with no emitted flag and a paper-level outside-fragment classification. Please state near the example-suite table that these codes are the paper's classification, not necessarily the implementation's output fields, so that readers do not expect a flag where none exists.
  4. [Section 7.2.1 and Section 8.1] The clause-activation sampler uses the same GK prover for derivability checks; the paper says this, but it is worth repeating when the CA column is discussed in Section 8 that agreement with CA is not an independent test of proof search, and that only the shared-threshold sampler is independent of the reasoner's uncertainty code.
  5. [Throughout] Several inline mathematical examples have spacing artifacts from PDF rendering, such as 'Consider0.5 ::bird(a)' in Section 2 and 'Example 18, f lies(a)' in Table 7. These should be cleaned in the final version.

Circularity Check

1 steps flagged · score 2.0 of 10

No load-bearing circularity: central claims are conditional on explicitly stated semantic postulates; the main self-validation loop is disclosed and external benchmarks anchor the one-sided fragment.

  1. other [Section 7.2.2 (Shared-threshold sampler), applied in Section 8.2.2]
    "On its stated fragment, the sampler directly samples the defined shared-threshold semantics; its only numerical approximation is Monte Carlo sampling error. Agreement with GK is expected up to sampling precision, and a persistent disagreement indicates an implementation or semantic discrepancy."

    The ST sampler is a direct implementation of the same paper-defined Model 2 that the dependency-aware evaluator is claimed to compute. The GK/ST agreement is therefore an internal consistency check between two implementations of one specification, not an independent confirmation of the semantic postulates. The paper's own wording says the sampler 'directly samples the defined shared-threshold semantics' and that agreement is 'expected up to sampling precision.' This does not undermine the conditional correspondence theorem, which is stated relative to explicit postulates, and the external system comparisons supply independent evidence on the one-sided fragment, so the circularity is non-load-bearing.

full rationale

The derivation chain is largely non-circular. Proposition 6 is a conditional theorem about the dependency-aware evaluator agreeing with the shared-threshold world definition on the stated correspondence fragment; the fragment conditions and the shared-threshold, noisy-or, directed-reading, and contrary-gated postulates are explicitly presented as semantic choices rather than derived empirical facts. The retained-proof and dependency-aware calculations are evaluated against analytic closed forms that are algebraic consequences of the same definitions, and the CA sampler's reuse of the GK prover for derivability checks is disclosed in Section 7.2.1 as testing activation sampling but not proof search. The one genuine self-validation loop is the ST sampler, which implements the very semantics the evaluator is supposed to realize, so GK/ST agreement is implementation consistency rather than external confirmation; this is noted in the single step above and does not affect the conditional correctness claim. Independent grounding exists: exact agreements with ProbLog, PASTA, plingo, and smProbLog on the one-sided probabilistic fragment (C1, C2, N1, N2, F1) and with published default benchmarks in Table 9. The paper also explicitly lists the main limitations, including factoring-derived answers outside the fragment, the coarse dependency index, proof replay gaps, and the absence of a joint probability measure over the two models, all of which are stated rather than concealed. No fitted parameter is renamed as a prediction, and no load-bearing result is justified solely by a self-citation chain.

Assumptions & free parameters 2 free parameters · 6 assumptions · 2 invented entities

No parameters are fitted to data; input confidences are user-supplied. The central claim rests on two paper-specific semantic postulates (shared thresholds and auxiliary gates), on a directed reading of clauses, and on standard first-order logic. The exception limit and implementation caps are hand-chosen operational values, not part of the reference semantics.

free parameters (2)
  • Exception limit lambda = 0.5 default
    Section 3.3: operational threshold deciding which exception proofs enter recursive checking; not part of either reference semantics, but affects compatibility-mode outputs.
  • Report-time implementation caps = depth 16, 24 derivations per polarity, 20 reduced event sets, 6 shared predecessors, 400/1600 ms deadlines
    Section 6.6: hand-chosen implementation safeguards that determine when dependency-aware evaluation falls back; not derived from the semantics.
assumptions (6)
  • ad hoc to paper Noisy-or is the same-polarity pooling operator for support contributions (Equation 1).
    Section 5.2.1 states noisy-or is the defined aggregation rule and that other pooling rules express different dependence assumptions.
  • ad hoc to paper Each ground atom has one shared threshold UA ~ Uniform(0,1), giving maximal-overlap coupling of positive and negative support pools.
    Section 5.2.2 defines this as the opposition rule; Proposition 2 shows it attains the Frechet lower bound, a choice not implied by inputs.
  • ad hoc to paper Contrary-gated defaults use an auxiliary independent threshold VA.
    Section 5.4.3 explicitly calls the independent pair a semantic postulate for this local default case.
  • domain assumption Ground-instance activation independence: each uncertain ground clause instance is active independently with probability equal to its input confidence.
    Section 5.1 adopts the ground-choice convention of distribution semantics, matching ProbLog; it is an interpretation of input confidences, not an empirical fact.
  • domain assumption Directed reading of clauses: only authored or selected conclusion literals are used; contraposition and classical equivalence are not preserved.
    Section 6.4 states classically equivalent source formulas can yield different reports, and direction is treated as part of the input.
  • standard math Standard first-order resolution, paramodulation, factoring, and equality reasoning are sound.
    Background logic inherited from gkc; the paper does not reprove it.
invented entities (2)
  • Shared threshold UA per ground atom
    purpose: Determines whether pooled positive or negative support is active, defining positive, negative, conflict, and ignorance regions.
    Introduced in Section 5.2.2 as a semantic postulate; no observable counterpart.
  • Auxiliary contrary-gated threshold VA
    purpose: Independent gate for defaults whose exception condition is the negation of the rule head.
    Section 5.4.3 calls the independent pair a semantic postulate.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Structure-Preserving Uncertainty Propagation in First-Order Proof Search." pith.science (2026). https://pith.science/paper/UD7ITEK4

@misc{pith2026260809190,
  author       = {Pith},
  title        = {Pith review of: Structure-Preserving Uncertainty Propagation in First-Order Proof Search},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UD7ITEK4}},
  note         = {Machine review of arXiv:2608.09190}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2608.09190 by the authors.

Figure 1
Figure 1. Calculation sequence used to assemble a GK report. [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Proof search structure. Solid branches collect proofs of [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Same-polarity pooling followed by shared-threshold opposition resolution. Here [PITH_FULL_IMAGE:figures/full_fig_p017_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Post-search report construction. Retained proof histories produce the retained-proof [PITH_FULL_IMAGE:figures/full_fig_p028_4.png]
Figure 5
Figure 5. Figure 5: Provenance-aware same-polarity pooling. The two proofs are neither independent nor [PITH_FULL_IMAGE:figures/full_fig_p030_5.png]
Figure 6
Figure 6. Figure 6: Same-polarity agreement and opposite-polarity divergence. Left: two independent pos [PITH_FULL_IMAGE:figures/full_fig_p056_6.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Every pooling rule has its world: matching probability combination rules to situations and stakes

    stat.ME 2026-08 accept novelty 6.0 of 10

    A pooling rule is only correct when the numbers it combines are generated in a matching way, and every rule's mismatch has a measurable probability and decision cost.

Reference graph

Works this paper leans on

54 extracted references · 42 canonical work pages · cited by 1 Pith paper

  1. [1]

    Alviano, F

    M. Alviano, F. Calimeri, C. Dodaro, D. Fuscà, N. Leone, S. Perri, F. Ricca, P. Veltri, and J. Zangari. The ASP system DLV2. InLogic Programming and Nonmonotonic Reasoning, LNCS 10377, pp. 215–221, 2017

    work page 2017

  2. [2]

    Alsinet, C

    T. Alsinet, C. I. Chesñevar, L. Godo, and G. R. Simari. A logic programming framework for possibilistic argumentation: formalization and logical properties.Fuzzy Sets and Systems, 159(10):1208–1228, 2008. doi:10.1016/j.fss.2007.12.013

    work page doi:10.1016/j.fss.2007.12.013 2008

  3. [3]

    Arias, M

    J. Arias, M. Carro, E. Salazar, K. Marple, and G. Gupta. Constraint answer set program- ming without grounding.Theory and Practice of Logic Programming, 18(3–4):337–354, 2018. doi:10.1017/S1471068418000285

    doi:10.1017/s1471068418000285 2018

  4. [4]

    Azzolini

    D. Azzolini. On the development of PASTA: inference in probabilistic answer set program- ming under the credal semantics. InProceedings of the 39th International Conference on Logic Programming, EPTCS 385, pp. 314–316, 2023. doi:10.4204/EPTCS.385.34

    work page doi:10.4204/eptcs.385.34 2023

  5. [5]

    S. H. Bach, M. Broecheler, B. Huang, and L. Getoor. Hinge-loss Markov random fields and probabilistic soft logic.Journal of Machine Learning Research, 18(109):1–67, 2017

    work page 2017

  6. [6]

    Baral, M

    C. Baral, M. Gelfond, and N. Rushton. Probabilistic reasoning with answer sets.Theory and Practice of Logic Programming, 9(1):57–144, 2009. doi:10.1017/S1471068408003645

    doi:10.1017/s1471068408003645 2009

  7. [7]

    N. D. Belnap. A useful four-valued logic. In J. M. Dunn and G. Epstein, editors,Modern Uses of Multiple-Valued Logic, pp. 8–37. Reidel, 1977

    work page 1977

  8. [8]

    Bílková, S

    M. Bílková, S. Frittella, D. Kozhemiachenko, O. Majer, and K. Manoorkar. Describing and quantifying contradiction between pieces of evidence via Belnap–Dunn logic and Dempster– Shafer theory.Proceedings of Machine Learning Research, 215:37–47, 2023

    work page 2023

Show all 54 references
  1. [9]

    Bochman and V

    A. Bochman and V. Lifschitz. Pearl’s causality in a logical setting. InAAAI 2015, pp. 1446– 1452, 2015. doi:10.1609/aaai.v29i1.9411. 76

    2015 doi

  2. [10]

    G.Brewka.Addingprioritiesandspecificitytodefaultlogic.InJELIA,LNCS838, pp.247–260, 1994

    1994

  3. [11]

    B. G. Buchanan and E. H. Shortliffe, editors.Rule-Based Expert Systems: The MYCIN Exper- iments of the Stanford Heuristic Programming Project. Addison–Wesley, Reading, MA, 1984

    1984

  4. [12]

    Calimeri, D

    F. Calimeri, D. Fuscà, S. Perri, and J. Zangari. I-DLV: the new intelligent grounder of DLV. Intelligenza Artificiale, 11(1):5–20, 2017. doi:10.3233/IA-170104

    2017 doi

  5. [13]

    F. G. Cozman and D. D. Mauá. The joy of probabilistic answer set programming: semantics, complexity, expressivity, inference.International Journal of Approximate Reasoning, 125:218– 239, 2020. doi:10.1016/j.ijar.2020.07.004

    2020 doi

  6. [14]

    Confalonieri, J

    R. Confalonieri, J. C. Nieves, M. Osorio, and J. Vázquez-Salceda. Dealing with explicit pref- erences and uncertainty in answer set programming.Annals of Mathematics and Artificial Intelligence, 65(2–3):159–198, 2012. doi:10.1007/s10472-012-9311-0

    2012 doi

  7. [15]

    A. P. Dempster. Upper and lower probabilities induced by a multivalued mapping.Annals of Mathematical Statistics, 38(2):325–339, 1967. doi:10.1214/aoms/1177698950

    1967

  8. [16]

    T. Denœux. Conjunctive and disjunctive combination of belief functions induced by nondistinct bodies of evidence.Artificial Intelligence, 172(2–3):234–264, 2008. doi:10.1016/j.artint.2007.05.008

    2008 doi

  9. [17]

    De Raedt, A

    L. De Raedt, A. Kimmig, and H. Toivonen. ProbLog: a probabilistic Prolog and its application in link discovery. InIJCAI, pp. 2468–2473, 2007

    2007

  10. [18]

    Dietrich and C

    F. Dietrich and C. List. Probabilistic opinion pooling. In A. Hájek and C. Hitchcock, editors, The Oxford Handbook of Probability and Philosophy, pp. 519–540. Oxford University Press, 2016

    2016

  11. [19]

    Dubois and H

    D. Dubois and H. Prade.Possibility Theory: An Approach to Computerized Processing of Uncertainty. Plenum Press, New York, 1988

    1988

  12. [20]

    Dupin de Saint-Cyr and H

    F. Dupin de Saint-Cyr and H. Prade. Handling uncertainty and defeasibility in a possi- bilistic logic setting.International Journal of Approximate Reasoning, 49(1):67–82, 2008. doi:10.1016/j.ijar.2007.08.001

    2008 doi

  13. [21]

    Fierens, G

    D. Fierens, G. Van den Broeck, J. Renkens, D. Shterionov, B. Gutmann, I. Thon, G. Janssens, and L. De Raedt. Inference and learning in probabilistic logic programs using weighted Boolean formulas.Theory and Practice of Logic Programming, 15(3):358–401, 2015. doi:10.1017/S14710...

    2015 doi

  14. [22]

    M. Fitting. Bilattices and the semantics of logic programming.Journal of Logic Programming, 11(2):91–116, 1991

    1991

  15. [23]

    Gebser, R

    M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub. Multi-shot ASP solv- ing with clingo.Theory and Practice of Logic Programming, 19(1):27–82, 2019. doi:10.1017/S1471068418000054

    2019 doi

  16. [24]

    Gogate and P

    V. Gogate and P. M. Domingos. Probabilistic theorem proving. InUAI 2011, pp. 256–265, 2011. 77

    2011

  17. [25]

    Genest and J

    C. Genest and J. V. Zidek. Combining probability distributions: a critique and an annotated bibliography.Statistical Science, 1(1):114–135, 1986

    1986

  18. [26]

    Governatori, M

    G. Governatori, M. J. Maher, G. Antoniou, and D. Billington. Argumentation se- mantics for defeasible logic.Journal of Logic and Computation, 14(5):675–702, 2004. doi:10.1093/logcom/14.5.675

    2004 doi

  19. [27]

    M. J. Gómez Lucero, C. I. Chesñevar, and G. R. Simari. Modelling argument accrual with possibilistic uncertainty in a logic programming setting.Information Sciences, 228:1–25, 2013. doi:10.1016/j.ins.2012.11.025

    2013 doi

  20. [28]

    C. Guo, G. Pleiss, Y. Sun, and K. Q. Weinberger. On calibration of modern neural networks. InProceedings of the 34th International Conference on Machine Learning, PMLR 70, pp. 1321–1330, 2017

    2017

  21. [29]

    S. Hahn, T. Janhunen, R. Kaminski, J. Romero, N. Rühling, and T. Schaub. Plingo: a system for probabilistic reasoning in answer set programming.Theory and Practice of Logic Program- ming, 25(2):134–167, 2025. doi:10.1017/S1471068424000449

    2025 doi

  22. [30]

    Heckerman

    D. Heckerman. Probabilistic interpretations for MYCIN’s certainty factors. In L. N. Kanal and J. F. Lemmer, editors,Uncertainty in Artificial Intelligence, pp. 167–196. North-Holland, 1986

    1986

  23. [31]

    A. Hunter. Argument strength in probabilistic argumentation based on defeasible rules.Inter- national Journal of Approximate Reasoning, 146:79–105, 2022. doi:10.1016/j.ijar.2022.04.003

    2022 doi

  24. [32]

    Jøsang.Subjective Logic: A Formalism for Reasoning Under Uncertainty

    A. Jøsang.Subjective Logic: A Formalism for Reasoning Under Uncertainty. Springer, 2016

    2016

  25. [33]

    Kimmig, G

    A. Kimmig, G. Van den Broeck, and L. De Raedt. Algebraic model counting.Journal of Applied Logic, 22:46–62, 2017. doi:10.1016/j.jal.2016.11.031

    2017 doi

  26. [34]

    E. P. Klement, R. Mesiar, and E. Pap.Triangular Norms. Kluwer, 2000

    2000

  27. [35]

    S. Min, K. Krishna, X. Lyu, M. Lewis, W.-t. Yih, P. Koh, M. Iyyer, L. Zettlemoyer, and H. Ha- jishirzi. FActScore: Fine-grained atomic evaluation of factual precision in long form text gen- eration. InProceedings of EMNLP 2023, pp. 12076–12100, 2023. doi:10.18653/v1/2023.emnlp...

    2023 doi

  28. [36]

    N. Potyka. Bipolar abstract argumentation with dual attacks and supports. InKR 2020, pp. 677–686, 2020. doi:10.24963/kr.2020/69

    2020 doi

  29. [37]

    J. L. Pollock. Defeasible reasoning.Cognitive Science, 11(4):481–518, 1987. doi:10.1207/s15516709cog1104_4

    1987 doi

  30. [38]

    H. Prakken. Probabilistic strength of arguments with structure. InKR 2018, pp. 158–167, 2018

    2018

  31. [39]

    R. Reiter. A logic for default reasoning.Artificial Intelligence, 13(1–2):81–132, 1980. doi:10.1016/0004-3702(80)90014-4

    1980 doi

  32. [40]

    A. Rago, F. Toni, M. Aurisicchio, and P. Baroni. Discontinuity-free decision support with quantitative argumentation debates. InKR 2016, pp. 63–73, 2016. 78

    2016

  33. [41]

    Richardson and P

    M. Richardson and P. Domingos. Markov logic networks.Machine Learning, 62:107–136, 2006. doi:10.1007/s10994-006-5833-1

    2006 doi

  34. [42]

    Shafer.A Mathematical Theory of Evidence

    G. Shafer.A Mathematical Theory of Evidence. Princeton University Press, 1976

    1976

  35. [43]

    T. Sato. A statistical learning method for logic programs with distribution semantics. InICLP 1995, pp. 715–729. MIT Press, 1995

    1995

  36. [44]

    E. H. Shortliffe and B. G. Buchanan. A model of inexact reasoning in medicine.Mathematical Biosciences, 23:351–379, 1975. doi:10.1016/0025-5564(75)90047-4

    1975 doi

  37. [45]

    Sneyers, D

    J. Sneyers, D. De Schreye, and T. Frühwirth. Probabilistic legal reasoning in CHRiSM.Theory and Practice of Logic Programming, 13(4–5):769–781, 2013. doi:10.1017/S1471068413000483

    2013 doi

  38. [46]

    Sutcliffe

    G. Sutcliffe. The TPTP problem library and associated infrastructure: from CNF to TH0, TPTP v6.4.0.Journal of Automated Reasoning, 59:483–502, 2017

    2017

  39. [47]

    T. Tammet. GKC: a reasoning system for large knowledge bases. InCADE 27, LNAI 11716, pp. 538–549, 2019. doi:10.1007/978-3-030-29436-6_32

    2019 doi

  40. [48]

    Tammet, D

    T. Tammet, D. Draheim, and P. Järv. Confidences for commonsense reasoning. InCADE 28, LNAI 12699, pp. 507–524, 2021. doi:10.1007/978-3-030-79876-5_29

    2021 doi

  41. [49]

    Tammet, D

    T. Tammet, D. Draheim, and P. Järv. GK: implementing full first order default logic for commonsense reasoning (system description). InIJCAR 2022, LNAI 13385, pp. 300–309, 2022. doi:10.1007/978-3-031-10769-6_18

    2022 doi

  42. [50]

    Tammet, D

    T. Tammet, D. Draheim, P. Järv, and M. Verrev. First order logic and commonsense reasoning: a path less travelled. In2nd Workshop on Goal-directed Execution of Answer Set Programs, CEUR-WS 3193, 2022

    2022

  43. [51]

    M. Thimm. The Tweety Library Collection for logical aspects of artificial intelligence and knowledge representation.Künstliche Intelligenz, 31(1):93–97, 2017. doi:10.1007/s13218-016- 0458-4

    2017 doi

  44. [52]

    Totis, L

    P. Totis, L. De Raedt, and A. Kimmig. smProbLog: stable model semantics in ProbLog for probabilistic argumentation.Theory and Practice of Logic Programming, 23(6):1198–1247,

  45. [53]

    Wang and Y

    Z. Wang and Y. Shen. Convergent semantics for weighted bipolar argumentation. InAAAI 2026, pp. 19415–19423, 2026. doi:10.1609/aaai.v40i23.39019. 79

    2026 doi

  46. [2023]

    doi:10.1017/S147106842300008X

    doi

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.