Did you know ... Search Documentation:
Pack sphere -- TODO

sPHeRE TODO — alignment with the JAIR paper "sPHeRE: a Reasoner for Hybrid Knowledge Bases"

(Last reviewed: 2026-07-22, against README/pack.pl and a live run of the test suite with SWI-Prolog 9.3.22, bddem@4.3.1, cplint@4.5.0, trill@8.0.0 installed as packs.)

Overall: the architecture described in the paper IS present in the code:

So most of the "todo" is bug-fixing and closing verification/documentation gaps, not building new subsystems from scratch.

=== PA - Expl ===

[ ] 1. Found and_f_ax and and_f in trillo and check the shape of explanations

[ ] 2. Explanations must only contain prob axioms and lpassertions

=== P0 — Critical / reproducible bugs (block the paper's core claim of computing P(q)) ===

[ ] 1. Fix prob/2 — currently fails for every example tried (Example_1, Example_2, Example_7) with: ret_prob/3: Domain error: `foreign_return_value' expected, found `<int>' Repro: cd prolog/sphere_test swipl -g "use_module(library(sphere_test/test_ex1)), test_ex1, halt." -t "halt(1)" All prob/2-based tests fail this way; query/1 (Boolean) tests mostly still pass. Likely root cause: prolog/utility/trillo.pl states "This module is based on TRILL version 6.0.2", but the pack directory has trill@8.0.0 and bddem@4.3.1 installed side by side — the vendored copy has drifted from the bddem C ABI it was written against (Env/BDD handle representation, or argument order in some ret_probc/or_listc call chain). Trace Env vs BDD handles through get_node/3 -> get_p/3 -> ret_probc/3, and through oracle_call/4-6 -> solve_all/4-5 -> instanceOf_meta/6 -> get_bdd/4, since BDD handles and Env handles are both encoded as small/large Prolog integers and are easy to swap silently. This is almost certainly the same issue the existing TODO items below are meant to fix by depending on the real trill/cplint packs instead.

[ ] 2. Fix well-founded-model correctness bug in examples/Example_7.pl: subClassOf(c,complementOf(h)). h(a). c(a):- \+ h(a). query(c(a)) currently succeeds; per WFS/Theorem 7 it must fail (h(a) is true, so \+ h(a) fails, so c(a) must be false — test_ex7.pl:persjbq already encodes the expected is_false). Investigate the doubling/oracle interaction for complementOf classes and negative literals over DL-atoms (sphere_not_dl/5, sphere_neg_H/6, oracle_call/4-6).

[ ] 3. andc_inc/4, called from sphere_check_inconsistency/4 (sphere.pl), is not defined anywhere in this repo nor exported by the installed bddem pack (verified: current_predicate/2 finds nothing). Any HKB that triggers an actual inconsistency while check_incons is enabled will crash with "unknown procedure". Either implement andc_inc/4 (e.g. andc/4 + zeroc/2 check) or replace its use with an existing bddem predicate.

[ ] 4. examples/Example_4.pl is missing (referenced by prolog/sphere_test/test_ex4.pl, which expects commander(john)/person(john) probabilistic facts). Loading it fails with "source_sink ... does not exist". Recreate this example (it is meant to also stand in for the paper's technical Example 4 — p(X)/d(X)/g(X)/o(a)/o(b) scenario already partially covered by examples/Example_1.pl, so reconcile naming/content).

[ ] 5. Re-enable test_ex4 and test_ex7 in prolog/sphere_test/test.pl's test/0 (currently commented out) once items 1-4 are fixed, so ?- test. actually exercises the full suite again.

=== P1 — Fidelity to the theoretical guarantees (Sections 4-5 of the paper) ===

[ ] 6. No code enforces or checks DL-safety (Definition 2: every LP-rule variable must occur in a positive non-DL-atom in the body), yet Theorems 6 and 7 (termination, correctness) explicitly require the HKB to be DL-safe. Add a load-time check that warns (or errors) when a loaded rule is not DL-safe.

[ ] 7. Resolve the two `% TODO: check whether H is a Dl-atom` markers left in sphere.pl (sphere_check_inconsistency/4, sphere_neg_H/6). Right now every arity-1/2 head is treated identically regardless of whether its predicate actually occurs in the DL ontology O, but the PITA^d transformation (Section 4.2.1, rules 2b.i vs 2b.ii) and Definition 1 (DL-atom vs non-DL-atom) explicitly branch on this distinction.

[ ] 8. Several TRILL^O tableau rules inherited in trillo.pl are marked as incomplete: ch_rule/max_rule ("TODO da sistemare" / "TO IMPROVE!"), and disjointClasses / disjointUnion clash checks ("TODO use hierarchy" — ignores the class hierarchy). These affect completeness/correctness (Lemma 1) for HKBs using cardinality restrictions or disjointness axioms. Audit and fix, or clearly document the restriction in README (e.g. "cardinality restrictions are not fully supported yet").

[ ] 9. Theorem 6 (termination) only holds when the HKB has no function symbols; today the only mitigation for the function-symbol case is the optional depth_bound setting (default false, i.e. off). Consider: (a) documenting this limitation prominently, (b) emitting a warning when function symbols are detected and depth_bound is off.

=== P2 — Example/test coverage matching the paper ===

[ ] 10. Add an example/test for paper's Example 5 queries (safe(t), spillover_count(t,s(0))), which exercise negation over a recursively defined predicate. examples/Example_spillover.pl currently only has spillover_count/2 without at_least_two_spillovers/1 / safe/1.

[ ] 11. Add an example/test for paper's Examples 8-9 (TRILL^O assuming non-ground LP-assertions true: a(X):-o(X). o(i1). a⊑b. i2:a. vs i1:a.) to directly validate the "heads" unification feature of Section 4.2.2. examples/Example_3.pl is close to this but has no corresponding test_ex3.pl wired into the suite.

[ ] 12. Add a short header comment to each examples/*.pl file noting which paper example/section it corresponds to, to keep the mapping maintainable (current numbering does not match the paper's, e.g. Example_1.pl ≅ paper's Example 4, Example_spillover.pl ≅ paper's Examples 1/3).

=== P3 — Documentation & packaging ===

[ ] 13. Update README.md to document the PHKB^FS-specific features that are actually implemented but currently undocumented: DISPONTE probabilistic DL axioms (annotationAssertion('.../disponte#probability', Axiom, literal(P))), function symbols, and the set_sphere/2 settings (depth_bound, depth, check_incons, single_var, tabling, epsilon_parsing).

[ ] 14. pack.pl declares requires(bddem). with no version constraint. Once the root cause of bug #1 is confirmed, pin a known-good version range to prevent silent breakage against future bddem releases.

[ ] 15. (Pre-existing TODO items, likely the real fix for bug #1 above)

[ ] 16. prolog/sphere_test_article/ only contains scripts for the Social-Networks-style benchmark (gen_graph.py, run, test.sh, init_test.sh, collect_time.py). The paper's Section 7 (Q2) also reports Lipid and University-Benchmark comparisons against NoHR/HexLite — add/link the corresponding scripts and data if they belong in this repo, or note in README where they actually live.

=== Note on the source PDF === The supplied PDF still contains several unresolved author review comments/annotations (in Italian, e.g. around the sPHeRE-complete-oracle definition, the Theorem 7 proof sketch, figure/table captions in Section 7, and the acknowledgments). These indicate the paper itself is a working draft in a few spots (informal definitions flagged by the authors, incomplete bidirectional-network results wording, unclear figure legend). Treat those specific spots as lower-confidence ground truth when implementing items 6/7 above.