nsaspy/prolog-rlm
1
0
Fork 0
Code Issues 83 Pull requests 10 Projects Releases Packages Wiki Activity Actions

[MACHINE-SPIRIT 3/8] Epistemics and truth maintenance: belief revision, ATMS/TMS, paraconsistency, defaults, provenance, temporal truth #398

New issue
Closed
opened 2026-09-08 01:29:19 +00:00 by nsaspy · 4 comments
nsaspy commented 2026-09-08 01:29:19 +00:00
Owner
Copy link

Parent: #397
Related: #394
Downstream: lost-rob0t/symbolic-memory#4 #6 #7

Distinct research mandate

Treat truth maintenance and epistemic state as the primary problem: belief revision, TMS/ATMS, non-monotonic/default reasoning, paraconsistency, provenance, temporal truth, source dependence, defeat, and cross-theory epistemic composition.

Depth 3 status — DESIGN-COMPLETE, IMPLEMENTATION-UNPROVEN

All four required subpasses are durably preserved in this issue's comments.

A — foundations: COMPLETE

Epistemic Support Graph (ESG) + explicit versioned Epistemic Profiles.

Canonical evidence independently preserves positive/negative support, justifications, assumptions/environments, validity, lifecycle and provenance. Warrant is computed under an explicit profile rather than stored as one mutable truth value.

Hard distinctions:

withdraw(P) != assert(not(P))
temporal change != belief revision
default defeat != explicit false
trust != probability
supersession != destruction

Candidate profiles include support-paraconsistent, WFS/default, stable-model, argumentation and revision-projection views.

B — semantic/adversarial deepening: COMPLETE

ESG is augmented by a Typed Defeat / Dependence Graph.

Preserve rebut / undermine / undercut / deterministic invalidate separately; preferences are typed/partial/scoped; source dependence prevents echo corroboration; circular support cannot self-bootstrap; iterated revision retains lineage; bitemporal valid_at vs known_at preserves historical epistemic state; semantic acceptance remains separate from evaluation completeness.

C — composition / heterogeneity: COMPLETE

Adopt an Epistemic Federation Fabric (EFF). Local theories retain local WFS/ASP/paraconsistent/argumentation/revision semantics and exchange status-bearing epistemic exports through typed/versioned bridges.

Hard federation invariants:

local NAF/absence != cross-theory explicit negation
credulous != skeptical warrant
undefined != conflicted != no-model != resource-limited
local priorities/defaults stay namespaced unless explicitly lifted
identity reconciliation is an explicit provenance-bearing assumption
semantic/epistemic bridges never grant host authority

Classic global MCS equilibrium remains an optional bounded federation profile, not ambient memory truth.

D — computational realization / scaling / conformance: COMPLETE

Adopt the Demand-Driven Interface-Factored Epistemic Executor.

ESG + defeat/dependence + immutable ledger
              ↓
       Epistemic Query Plan (EQP)
 relevance slice + bridge SCC condensation
              ↓
 local profile-specific projected interface summaries
              ↓
 acyclic delta flow / profile-specific SCC evaluator
              ↓
 factorized interface alternatives + constraints
              ↓
 warrant + completeness + compressed replay receipt

Key D decisions:

  1. Demand slice first. Select only theories/bridges reachable from the query/context/profile.
  2. Project local states to bridge-visible epistemic interfaces. Local models that differ internally but export the same interface may be quotiented for federation; full local model Cartesian products are not the default.
  3. SCC-specific evaluation. Acyclic/monotone regions use topological or semi-naive fixed-point propagation; WFS uses tabled/alternating fixed-point semantics; ASP/equilibrium SCCs use bounded projected-interface solver search; argumentation uses its named semantics; noncomposable SCCs return explicit diagnostics.
  4. Factor alternatives. Use an engine-neutral AND/OR + guard/nogood/link choice DAG; BDD/ZDD/d-DNNF/tree-decomposition or solver-native representations are optional optimizations, never canonical semantics.
  5. Incremental invalidation is dependency-directed. Evidence/lifecycle -> local summary -> bridge -> SCC -> downstream cache. If local recomputation yields the same projected interface digest, invalidation stops there.
  6. Caches are derived state. Keys include theory/profile/evidence frontier, valid_at/known_at, interface signature, identity/dependence, bridge/mapping/closure generation and relevant translator/backend contract versions.
  7. Explicit structural budgets. Bound selected theories, bridge edges, SCC size, interface dimensions, projected states, solver calls, factorized-choice nodes, proof bytes, CPU/wall/memory. Resource exhaustion never becomes semantic false/top-1 truth and never triggers implicit LLM fallback.
  8. Compressed explanations. Shared receipt DAG: query plan -> interface summaries -> bridge/SCC receipts -> local justifications -> source assertions.
  9. Deterministic concurrency. EQP reuses the one canonical runtime/scheduler; scheduling interleavings may not change semantic outcomes.
  10. Replay/differential oracle. For identical canonical evidence/context/profile/bridge versions and budgets:
cold == warm-cache == cache-rebuilt
incremental == full from-scratch

under semantic/receipt-normalized comparison.

All compiled-semantic epistemic conformance fixtures must execute with zero provider/LLM calls.

Required conformance direction

Depth 3 records adversarial fixtures covering contradiction without explosion, withdrawal vs negation, default/defeat cycles, source dependence, bitemporal corrections, multiple/no stable models, profile plurality, noncomposable bridges, irrelevant-theory pruning, projected-interface quotienting, scoped invalidation, same-interface propagation stop, resource ceilings, concurrency determinism, cache/incremental differential equivalence, historical replay, explanation compression and stale-cache rejection for action/VERIFY.

Canonical handoffs

Strong conclusions are cross-linked to:

  • #394 — safe reasoning/lowering + Epistemic Query Plan execution contract;
  • #376 — EQP must reuse the one canonical runtime/scheduler and zero-model local expert execution;
  • symbolic-memory #6 — immutable epistemic ledger/frontiers + dependency-directed rebuildable cache state;
  • symbolic-memory #7 — demand-driven federated query surface and replay/explanation contract.

Unresolved implementation questions

  • exact first supported profile/federation matrix;
  • SWI incremental tabling vs optional XSB-compatible backend for WFS-heavy workloads;
  • ASP backend/process/FFI isolation and multi-shot lifecycle;
  • empirical SCC/interface-width cutoffs and optional factorization representation;
  • efficient incremental argumentation beyond bounded rebuild;
  • distributed multi-process/node execution belongs primarily to Depth 5 world-model scaling.

Completion statement

Depth 3 A/B/C/D is design-complete only. No Machine Spirit milestone is claimed from this research. Executable acceptance remains gated by later implementation/conformance evidence.

Next: #401A — procedural intelligence / expert systems.

Refs #392 #394 #397 #376 and downstream symbolic-memory#4/#6/#7.

Parent: #397 Related: #394 Downstream: lost-rob0t/symbolic-memory#4 #6 #7 ## Distinct research mandate Treat truth maintenance and epistemic state as the primary problem: belief revision, TMS/ATMS, non-monotonic/default reasoning, paraconsistency, provenance, temporal truth, source dependence, defeat, and cross-theory epistemic composition. ## Depth 3 status — DESIGN-COMPLETE, IMPLEMENTATION-UNPROVEN All four required subpasses are durably preserved in this issue's comments. ### A — foundations: COMPLETE **Epistemic Support Graph (ESG) + explicit versioned Epistemic Profiles.** Canonical evidence independently preserves positive/negative support, justifications, assumptions/environments, validity, lifecycle and provenance. Warrant is computed under an explicit profile rather than stored as one mutable truth value. Hard distinctions: ```text withdraw(P) != assert(not(P)) temporal change != belief revision default defeat != explicit false trust != probability supersession != destruction ``` Candidate profiles include support-paraconsistent, WFS/default, stable-model, argumentation and revision-projection views. ### B — semantic/adversarial deepening: COMPLETE ESG is augmented by a **Typed Defeat / Dependence Graph**. Preserve rebut / undermine / undercut / deterministic invalidate separately; preferences are typed/partial/scoped; source dependence prevents echo corroboration; circular support cannot self-bootstrap; iterated revision retains lineage; bitemporal `valid_at` vs `known_at` preserves historical epistemic state; semantic acceptance remains separate from evaluation completeness. ### C — composition / heterogeneity: COMPLETE Adopt an **Epistemic Federation Fabric (EFF)**. Local theories retain local WFS/ASP/paraconsistent/argumentation/revision semantics and exchange status-bearing epistemic exports through typed/versioned bridges. Hard federation invariants: ```text local NAF/absence != cross-theory explicit negation credulous != skeptical warrant undefined != conflicted != no-model != resource-limited local priorities/defaults stay namespaced unless explicitly lifted identity reconciliation is an explicit provenance-bearing assumption semantic/epistemic bridges never grant host authority ``` Classic global MCS equilibrium remains an optional bounded federation profile, not ambient memory truth. ### D — computational realization / scaling / conformance: COMPLETE Adopt the **Demand-Driven Interface-Factored Epistemic Executor**. ```text ESG + defeat/dependence + immutable ledger ↓ Epistemic Query Plan (EQP) relevance slice + bridge SCC condensation ↓ local profile-specific projected interface summaries ↓ acyclic delta flow / profile-specific SCC evaluator ↓ factorized interface alternatives + constraints ↓ warrant + completeness + compressed replay receipt ``` Key D decisions: 1. **Demand slice first.** Select only theories/bridges reachable from the query/context/profile. 2. **Project local states to bridge-visible epistemic interfaces.** Local models that differ internally but export the same interface may be quotiented for federation; full local model Cartesian products are not the default. 3. **SCC-specific evaluation.** Acyclic/monotone regions use topological or semi-naive fixed-point propagation; WFS uses tabled/alternating fixed-point semantics; ASP/equilibrium SCCs use bounded projected-interface solver search; argumentation uses its named semantics; noncomposable SCCs return explicit diagnostics. 4. **Factor alternatives.** Use an engine-neutral AND/OR + guard/nogood/link choice DAG; BDD/ZDD/d-DNNF/tree-decomposition or solver-native representations are optional optimizations, never canonical semantics. 5. **Incremental invalidation is dependency-directed.** Evidence/lifecycle -> local summary -> bridge -> SCC -> downstream cache. If local recomputation yields the same projected interface digest, invalidation stops there. 6. **Caches are derived state.** Keys include theory/profile/evidence frontier, `valid_at`/`known_at`, interface signature, identity/dependence, bridge/mapping/closure generation and relevant translator/backend contract versions. 7. **Explicit structural budgets.** Bound selected theories, bridge edges, SCC size, interface dimensions, projected states, solver calls, factorized-choice nodes, proof bytes, CPU/wall/memory. Resource exhaustion never becomes semantic false/top-1 truth and never triggers implicit LLM fallback. 8. **Compressed explanations.** Shared receipt DAG: query plan -> interface summaries -> bridge/SCC receipts -> local justifications -> source assertions. 9. **Deterministic concurrency.** EQP reuses the one canonical runtime/scheduler; scheduling interleavings may not change semantic outcomes. 10. **Replay/differential oracle.** For identical canonical evidence/context/profile/bridge versions and budgets: ```text cold == warm-cache == cache-rebuilt incremental == full from-scratch ``` under semantic/receipt-normalized comparison. All compiled-semantic epistemic conformance fixtures must execute with **zero provider/LLM calls**. ## Required conformance direction Depth 3 records adversarial fixtures covering contradiction without explosion, withdrawal vs negation, default/defeat cycles, source dependence, bitemporal corrections, multiple/no stable models, profile plurality, noncomposable bridges, irrelevant-theory pruning, projected-interface quotienting, scoped invalidation, same-interface propagation stop, resource ceilings, concurrency determinism, cache/incremental differential equivalence, historical replay, explanation compression and stale-cache rejection for action/VERIFY. ## Canonical handoffs Strong conclusions are cross-linked to: - #394 — safe reasoning/lowering + Epistemic Query Plan execution contract; - #376 — EQP must reuse the one canonical runtime/scheduler and zero-model local expert execution; - symbolic-memory #6 — immutable epistemic ledger/frontiers + dependency-directed rebuildable cache state; - symbolic-memory #7 — demand-driven federated query surface and replay/explanation contract. ## Unresolved implementation questions - exact first supported profile/federation matrix; - SWI incremental tabling vs optional XSB-compatible backend for WFS-heavy workloads; - ASP backend/process/FFI isolation and multi-shot lifecycle; - empirical SCC/interface-width cutoffs and optional factorization representation; - efficient incremental argumentation beyond bounded rebuild; - distributed multi-process/node execution belongs primarily to Depth 5 world-model scaling. ## Completion statement Depth 3 A/B/C/D is **design-complete only**. No Machine Spirit milestone is claimed from this research. Executable acceptance remains gated by later implementation/conformance evidence. Next: #401A — procedural intelligence / expert systems. Refs #392 #394 #397 #376 and downstream symbolic-memory#4/#6/#7.
nsaspy commented 2026-09-08 01:47:43 +00:00
Author
Owner
Copy link

Depth 3 / #400A — epistemic foundations: support graphs, truth maintenance, revision, defaults, paraconsistency

This is subpass A only. It establishes representative epistemic formalisms and candidate architectures. #400 remains open for B/C/D. Do not advance to #401.

Research question

Given the source/semantic architecture produced by #398/#399, how should Machine Spirit represent and compute epistemic state when all of the following can coexist?

  • source A asserts P;
  • source B explicitly denies P;
  • an old source asserted P but later withdrew/corrected it;
  • P was true at t1 but not at t2;
  • rule R strictly derives P;
  • default D normally derives P unless exception E;
  • P holds only under hypothesis/context H;
  • multiple independent derivations support P;
  • a derivation loses a premise;
  • a trusted policy chooses a winner for one operational query without rewriting history.

The core requirement is truth/support/acceptance separation. A proposition's stored evidence state is not the same thing as what a particular non-monotonic semantics warrants, and neither is the same thing as a destructive belief-set rewrite.

Primary / authoritative sources inspected

  1. Jon Doyle, A Truth Maintenance System, Artificial Intelligence 12 (1979), 231–272. Foundational justification-based TMS: beliefs record justifications/dependencies so changes can propagate through the dependency network. The key architectural lesson is to make reasons for belief explicit rather than storing only conclusions. Bibliographic/technical context confirmed through Stanford's logic-AI reference discussion of Doyle 1979.
  2. Johan de Kleer, An Assumption-based TMS, Artificial Intelligence 28(2) (1986), 127–162, DOI 10.1016/0004-3702(86)90080-9. ATMS labels propositions with assumption environments; inconsistent assumption sets become nogoods. Crucially, multiple contexts/solutions can coexist without destructive global retraction.
  3. C. E. Alchourrón, P. Gärdenfors, D. Makinson, On the Logic of Theory Change: Partial Meet Contraction and Revision Functions, JSL 50(2) (1985), 510–530, DOI 10.2307/2274239. AGM gives rationality postulates and representation results for contraction/revision by minimal change over belief sets.
  4. Raymond Reiter, A Logic for Default Reasoning, Artificial Intelligence 13 (1980). Default theories define extensions: conclusions can depend on consistency/absence conditions, and a theory can have multiple extensions or problematic extension structure. This is useful semantics, but dangerous as a hidden global truth policy.
  5. Michael Gelfond & Vladimir Lifschitz, The Stable Model Semantics for Logic Programming (ICLP/SLP 1988), 1070–1080; and Classical Negation in Logic Programs and Disjunctive Databases, New Generation Computing 9 (1991), 365–385. Stable-model semantics gives a declarative account of negation-as-failure; the 1991 extension adds explicit/classical negation and directly addresses incomplete information.
  6. Allen Van Gelder, Kenneth Ross, John Schlipf, The Well-Founded Semantics for General Logic Programs, JACM 38(3) (1991), 620–650. WFS gives a unique partial/three-valued model for general logic programs. Operationally important here: unresolved negative recursion becomes undefined rather than forcing an arbitrary model. SWI-Prolog supports WFS using tabled predicates + tnot/1, including residual conditions for undefined answers.
  7. Nuel Belnap, How a Computer Should Think (1977) / the Belnap-Dunn FOUR tradition. The key information model independently tracks positive and negative information, yielding states equivalent to neither / true-only / false-only / both. This is highly suitable as a support-state summary for inconsistent/incomplete memory, but it does not itself decide source priority or defaults.
  8. Phan Minh Dung, On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games, Artificial Intelligence 77(2) (1995), 321–357, DOI 10.1016/0004-3702(94)00041-X. Abstract argumentation separates arguments from attack/acceptance semantics and supplies skeptical/credulous ways of computing warranted arguments.
  9. Todd Green, Grigoris Karvounarakis, Val Tannen, Provenance Semirings, PODS 2007, DOI 10.1145/1265530.1265535. Provenance annotations can algebraically preserve alternative/conjunctive derivations through positive relational computation. Important boundary: provenance algebra is not automatically probability, trust, or truth.
  10. Current execution evidence: SWI-Prolog's WFS implementation supports tabled negation and residual programs; goal-directed ASP/s(CASP) literature demonstrates query-directed stable-model reasoning with justification trees and constraints. These are viable execution mechanisms, not a reason to collapse the canonical epistemic representation into one engine's semantics.

What current architecture already gets right

#392/#394 and symbolic-memory already preserve several essential distinctions:

  • proposition != assertion;
  • positive support != explicit negative support;
  • source claim != world assertion;
  • provenance and justification are first-class;
  • append-only history rather than last-write-wins;
  • temporal validity, scenario and attribution are explicit;
  • unknown is not Prolog failure;
  • conflict is preservable instead of auto-resolved;
  • derived/materialized state is rebuildable.

Those decisions survive.

The missing layer is a precise separation between evidence state, assumption environment, non-monotonic consequence, and revision policy.

Candidate architecture A — global JTMS / retract-and-propagate belief state

Maintain one current belief state. Each accepted node has justifications; when premises disappear, recursively retract dependent conclusions. Defaults can use absence conditions.

Conceptually:

ep_node(N, Proposition).
ep_justification(J, N, InPremises, OutPremises).
ep_status(N, in_or_out).

Strengths

  • simple current-state query surface;
  • explanations/dependency invalidation are natural;
  • maps well to table invalidation and classic TMS machinery;
  • useful inside a single bounded reasoning context.

Failure

It is the wrong canonical model for Machine Spirit. One global IN/OUT status loses plurality:

  • source-specific contradictory worlds;
  • alternate hypotheses;
  • multiple default extensions;
  • historical states;
  • source correction vs world falsity;
  • later queries using different trust/resolution policies.

A JTMS-style view remains useful as a derived context-local materialization, not the durable epistemic substrate.

Candidate architecture B — AGM belief-set revision as canonical truth state

Represent Machine Spirit's current beliefs as a logically closed theory K. New evidence P triggers expansion/revision; correction/retraction triggers contraction; use entrenchment/preference to minimize change.

Strengths

  • principled rationality postulates;
  • explicit notion of minimal change;
  • strong fit for a single agent maintaining a coherent commitment set;
  • useful for trusted policy layers that need one operational belief set.

Failure

Canonical Machine Spirit memory is intentionally multi-source, append-only, inconsistent and contextual. Classical AGM assumes a much cleaner target object than the evidence ledger we need. Destructively revising K when a news source changes would erase exactly the historical disagreement/provenance we want to preserve.

AGM should therefore be available as a revision projection/profile over a selected theory/context/trust policy, not as the storage semantics.

Example:

ledger: preserve A:P, B:not(P), correction(A,P), timestamps, derivations
                   ↓
AGM-like operational projection under policy X
                   ↓
selected coherent commitment set Kx

Changing policy X produces another projection, never mutated history.

Candidate architecture C — ATMS environments + paraconsistent evidence support (preferred foundation)

Use immutable assertion/derivation records to build an Epistemic Support Graph (ESG). Every proposition has independent positive and negative support sets. Justifications are hyperedges. Assumptions/context choices form explicit environments. Incompatible environments/nogoods are recorded rather than globally deleting one side.

Conceptual data model:

ep_support(SupportId,
           PropositionRef,
           Polarity,            % positive | negative
           AssertionOrDerivationRef,
           ContextRef,
           ValidityRef,
           ProvenanceRef).

ep_justification(JustId,
                 ConclusionSupport,
                 RuleRef,
                 PremiseSupportRefs,
                 AssumptionRefs,
                 ProfileRef,
                 ContextRef).

ep_environment(EnvId,
               AssumptionRefs,
               ContextRefs,
               PolicyRef,
               Meta).

ep_nogood(NogoodId, AssumptionRefs, ReasonRef, ProvenanceRef).

ep_lifecycle(EventId,
             Kind,              % withdraw | supersede | retract_claim | invalidate_derivation | corroborate ...
             TargetRef,
             CauseRef,
             Time,
             ProvenanceRef).

The base evidence state for a proposition at context/time can be summarized as:

positive support?   negative support?    support_state
no                  no                   neither
yes                 no                   supported_only
no                  yes                  refuted_only
yes                 yes                  both/conflicted

This is deliberately Belnap-like information state, not the final consequence relation.

ATMS-style environments preserve which assumption combinations support which conclusions. A contradiction marks an incompatible environment/nogood; it does not require deleting source evidence. de Kleer's ATMS is especially relevant because multiple contexts can coexist while avoiding repeated destructive retraction.

Why this fits Machine Spirit

  • append-only storage maps naturally to evidence/support events;
  • multiple sources and hypotheses coexist;
  • every conclusion can retain exact derivation paths;
  • temporal and contextual filters happen before/while building an environment;
  • conflict becomes queryable information;
  • alternative resolution policies can share one canonical evidence substrate;
  • removing a premise invalidates derived support without deleting historical records;
  • provenance can be shared structurally across derivation DAGs.

Candidate architecture D — argumentation graph as canonical state

Translate every supporting/refuting chain into an argument; contradictions/defaults/priorities become attack/defeat relations; use Dung-style grounded/preferred/stable semantics to calculate acceptance.

Strengths

  • excellent explanation model for contested claims;
  • skeptical vs credulous conclusions are explicit;
  • default/prioritized reasoning and source conflicts can be presented as attack/defeat structures;
  • good fit for research/news disputes.

Failure

Making argumentation the primitive store adds unnecessary expansion for ordinary facts, temporal state and deterministic Horn consequences. Arguments should be a derived epistemic view over ESG justifications, especially for contested/default queries.

Preferred architecture: ESG + explicit Epistemic Profiles

The architecture should therefore be:

immutable semantic assertions / source history
                    ↓
         EPISTEMIC SUPPORT GRAPH
 positive support | negative support
 justifications | assumptions | environments
 lifecycle | validity | provenance
                    ↓
      explicit epistemic profile
  ┌─────────┬─────────┬─────────┬─────────┐
  │         │         │         │         │
paracons.  WFS    stable/ASP   argument   AGM-like
support    default  models      view       revision
summary    view      view       view       view
  │         │         │         │         │
  └─────────┴─────────┴─────────┴─────────┘
                    ↓
        warranted query outcome
                    ↓
       explanation / counterevidence

The profile is part of query semantics. It must never be inferred from whichever Prolog predicate happened to be called.

Conceptual API:

epistemic_query(+TheoryRef,
                +Query,
                +Context,
                +EpistemicProfile,
                +Options,
                -Outcome).

epistemic_support(+Proposition,
                  +Context,
                  +Options,
                  -SupportState).

epistemic_explain(+OutcomeRef, -Explanation).

epistemic_counterevidence(+OutcomeRef, -CounterEvidence).

Outcome should distinguish at least:

support_state: neither | supported_only | refuted_only | both
acceptance: warranted | unwarranted | undecided | credulous_only | profile_inconsistent
profile: explicit profile/version
assumptions: exact environment
validity: query-time/context
support: justification refs
counterevidence: refuting justification refs

Do not compress this into one confidence float.

Baseline epistemic profile direction

A should establish the profile family but not prematurely freeze every B/C/D semantic detail.

support_paraconsistent

  • always available for validated evidence;
  • reports independent support/refutation;
  • contradiction is non-explosive;
  • no automatic winner;
  • minimal assumptions.

This should be the safest base query mode for heterogeneous memory.

well_founded_default

  • candidate default/non-monotonic workhorse for compatible bounded logic-program fragments;
  • unique partial model;
  • negative cycles can remain undefined;
  • SWI already has practical WFS/tabling machinery and residual explanations;
  • not permitted to reinterpret explicit negative evidence as simple negation-as-failure.

stable_models

  • optional profile for problems whose semantics genuinely require stable/default models;
  • multiple models are preserved;
  • expose skeptical (true in all admitted models) vs credulous (true in at least one) results;
  • zero models is an explicit epistemic failure state, not false;
  • solver/model enumeration limits must be surfaced.

argumentation

  • derive arguments/attacks/defeats from ESG support/justifications;
  • especially appropriate for contested research, defaults and source-priority explanations;
  • semantics (grounded/preferred/etc.) must be named/versioned.

revision_projection

  • AGM-inspired coherent operational commitment view;
  • runs only over selected admitted evidence/context with explicit preference/entrenchment policy;
  • output is a projection, never canonical deletion.

Five distinctions that MUST become hard invariants

1. Retraction/withdrawal != explicit negation

If a source says P, then later withdraws that statement:

withdraw(source_assertion(P)) != assert(not(P))

The lifecycle event deactivates that source support in ordinary current views; it does not create negative world evidence unless the correction explicitly asserts ¬P.

2. Temporal change != belief revision

CEO(A) valid Jan-May
CEO(B) valid Jun-current

is not a contradiction requiring AGM contraction. Both can be true at different valid times. Epistemic conflict detection must occur after temporal/context qualification.

3. Defeated default != false proposition

If birds normally fly is defeated for a penguin, that means the default justification does not warrant flies(penguin) in that environment. It is not by itself explicit support for not(flies(penguin)).

4. Source trust != proposition probability

A trust policy may control admission/preference, but:

trust(source)=0.8

is not automatically:

P(P)=0.8

Trust, compiler confidence, provenance multiplicity, probability and default priority remain separate dimensions.

5. Supersession != destruction

Newer semantic projections or source revisions can supersede old active support, but historical support/derivation remains replayable.

Defaults and rule priority: A-level decision

Do not encode priority by Prolog clause order.

Represent defaults explicitly:

ep_default(DefaultId,
           Preconditions,
           Conclusion,
           ExceptionConditions,
           PriorityInfo,
           Scope,
           Provenance).

Priority information is symbolic data and should support at least explicit declared priority and specificity evidence. The resolution semantics belongs to an epistemic profile.

Reiter default logic demonstrates why this matters: default theories can have multiple extensions. Stable-model semantics similarly admits multiple models. Machine Spirit must expose this plurality where it exists rather than selecting the first solver result.

Depth 3B should attack exact default priority/specificity behavior and competing non-monotonic semantics.

Incremental invalidation model

Canonical ESG records are immutable. Current support indexes/materialized warranted views are derived.

When a premise becomes inactive for a query context because of correction, expiry, identity revision, context change or explicit lifecycle event:

premise support changes active-status
        ↓
justification dependency graph
        ↓
invalidate affected derived supports
        ↓
recompute affected profile views only

This composes directly with #398D's canonical-vs-derived split and #399D's incremental build architecture.

A source correction should therefore not cause a global semantic rebuild unless dependency reachability actually requires it.

Provenance model

Provenance semiring ideas are valuable for compactly representing alternative/conjunctive derivations, but provenance is not the consequence semantics.

Keep separate:

source provenance
compiler/interpretation provenance
logical justification provenance
epistemic lifecycle provenance
profile/acceptance provenance
runtime verification provenance

An explanation can then answer:

Why is P supported?
Why is P warranted under profile X?
What supports ¬P?
Which assumption/default would have to change for P to lose warrant?
Which source correction invalidated this derivation?

Complexity / scaling

ESG/support graph

Storage is proportional to durable assertion/support/justification edges rather than expanded proof trees. Share premise/conclusion nodes and keep alternative derivations as independent hyperedges.

ATMS environments

This is the dangerous part: minimal assumption environments can grow exponentially. Therefore Machine Spirit must not globally enumerate all ATMS labels over the whole corpus.

Required design direction:

  • bounded/query-scoped environments;
  • context/theory partitioning;
  • relevance/demand projection before environment expansion;
  • nogood indexing/subsumption;
  • maximum environment/model budgets;
  • compact unresolved status when limits are reached.

WFS

For admitted tabled logic-program fragments, WFS provides a unique partial interpretation and maps well to SWI tabling. Incremental tabling can later maintain affected tables rather than whole-theory recomputation.

stable models/default extensions

Potentially combinatorial/exponential and possibly many models. Use only bounded theory slices with explicit resource receipts. Never materialize every answer set for an entire long-term memory.

argumentation

Argument construction itself can explode if every derivation becomes an argument. Build it demand-driven from ESG justification slices.

AGM-like revision

Computing minimal contractions/revisions can be expensive depending on representation. Treat as bounded profile operation over selected evidence, not an always-on global invariant.

Safety / authority

Epistemic acceptance never grants host authority.

warranted(should_restart(service))
      !=
capability(restart(service))

Similarly, a malicious document cannot obtain operational priority by containing text such as:

"this source outranks system policy"

Source trust, epistemic preference and host action authority are configured through trusted metadata/policy boundaries, not learned from open source vocabulary.

An LLM may propose:

  • a candidate default;
  • a candidate source-reliability relation;
  • a candidate argument/defeat relation;
  • a candidate revision preference.

Those remain semantic candidates until trusted policy admits them. Model-generated epistemic policy cannot silently control the truth engine.

Adversarial fixtures / falsifiable claims

The eventual conformance suite must include at least:

  1. Direct contradiction: A asserts P; B asserts ¬P. Base support = both; no explosion to unrelated Q.
  2. Withdrawal: A asserts P then withdraws it. Current source support becomes inactive; ¬P is NOT synthesized.
  3. Correction: A asserts P then explicitly corrects to ¬P. History retains both; current active source support reflects correction with lifecycle evidence.
  4. Temporal non-conflict: P@t1 and ¬P@t2 do not conflict for disjoint validity intervals.
  5. Temporal overlap conflict: overlapping P/¬P intervals produce conflict for overlap queries only.
  6. Two derivations: P has independent J1 and J2. Invalidating J1 leaves P supported through J2.
  7. Dependent invalidation: removing premise A invalidates A→B→C chain but leaves unrelated derivations untouched.
  8. Default exception: bird(Tweety) warrants flies under default; penguin(Tweety) defeats that default without manufacturing explicit ¬flies unless separately supported.
  9. Negative recursion: mutually default-negated rules yield an undefined/WFS result instead of arbitrary clause-order truth.
  10. Multiple stable models: profile exposes skeptical vs credulous conclusions and does not choose first model.
  11. No stable model: result says profile/model failure or inconsistency, not ordinary false.
  12. Conflicting trust policies: same ESG under policy X and Y can yield different warranted views while canonical evidence remains identical.
  13. Attributed claim: source_claims(S,P) does not satisfy unqualified-world P unless an explicit bridge/admission policy permits it.
  14. Scenario isolation: P in hypothetical H never supports ordinary world P.
  15. Retraction of derivation rule: rule lifecycle invalidation removes derived support but not source assertions.
  16. Nogood environment: assumptions {A,B} marked incompatible; supports requiring both cannot become warranted in that environment.
  17. Resource ceiling: environment/model explosion returns bounded undecided/resource_limited with receipt, never arbitrary top-1 truth.
  18. Authority injection: remembered text declaring itself authoritative cannot alter epistemic/host policy.
  19. Explanation duality: every warranted P can return support; every conflicted P can return both support and counterevidence.
  20. Replay: same canonical ESG + profile version + context produces semantically equivalent warranted results after derived cache rebuild.

Canonical design recommendations

prolog-rlm #394

Add an explicit Epistemic Support Graph + Epistemic Profile boundary. true/explicit_false/unknown/conflicted should not be a single opaque enum produced directly from facts. Results need independent support/refutation state plus profile acceptance.

Recommended result direction:

epistemic_outcome(
    Query,
    support_state(SupportState),
    acceptance(Acceptance),
    profile(ProfileRef),
    environment(EnvironmentRef),
    support(SupportRefs),
    counterevidence(CounterRefs),
    assumptions(AssumptionRefs),
    validity(Validity),
    unresolved(Unresolved),
    receipt(ReceiptRef)).

Do not finalize one universal default semantics in #394 before #400B/D.

symbolic-memory #6

Persist immutable epistemic support/lifecycle/justification inputs sufficient to rebuild current epistemic views. The ledger should not persist a single mutable truth column as authority.

Specifically preserve:

  • positive/negative support events;
  • assertion withdrawal/correction/supersession separately;
  • justification hyperedges;
  • assumptions/environment refs where durable;
  • temporal/context validity;
  • nogoods/incompatibility evidence where promoted;
  • epistemic profile/version on durable promoted conclusions/receipts;
  • rebuildable current support/acceptance indexes.

symbolic-memory #7

Query APIs should accept an explicit epistemic profile and return support state + acceptance + counterevidence, not just true/false/conflicted.

Cross-memory reasoning must make the evidence admission/trust/context policy explicit. all memories must not silently mean one global classical theory.

#397

Mark Depth 3A complete only. Queue #400B next.

Rejected simplifications

  • One float confidence per fact: loses contradiction, derivation plurality, default defeat, attribution and policy dependence.
  • Latest assertion wins: destroys provenance/history and misclassifies temporal change.
  • Global classical consistency: impossible/undesirable for heterogeneous web/news/log memory.
  • Belnap FOUR as complete reasoning system: excellent information-state basis, insufficient for defaults/priorities/revision.
  • AGM as storage semantics: useful coherent projection theory, wrong for append-only heterogeneous evidence.
  • ATMS labels globally materialized: semantically attractive but can explode combinatorially.
  • ASP/stable models everywhere: powerful profile, but multiple/no models and grounding/search cost make it unsuitable as universal base semantics.
  • WFS everywhere: excellent deterministic default profile for compatible programs, but does not by itself encode all source/trust/paraconsistent/revision semantics.
  • Argumentation as primitive storage: useful derived contested-belief view, unnecessarily expands ordinary deterministic knowledge.

A-level decision

GO: adopt a canonical Epistemic Support Graph over the existing proposition/assertion/context/justification substrate, with independent positive/negative support and explicit assumption environments. Treat all actual warrant/truth-maintenance behavior as versioned Epistemic Profiles over that substrate.

Preferred default safety posture for arbitrary heterogeneous memory is paraconsistent support reporting; a bounded well-founded default profile is the strongest current candidate for deterministic zero-LLM default reasoning over admitted logic-program fragments. Stable-model, argumentation and AGM-style revision remain explicit opt-in profiles/views.

This is a foundations decision, not final epistemics. #400B must now attack it, especially: default specificity/priorities, reinstatement, cycles of defeat, belief-vs-source trust, probabilistic/uncertain evidence, iterated revision, temporal correction, contradiction propagation, and whether ESG+profiles can avoid semantic mismatches between WFS/ASP/argumentation/paraconsistent views.

## Depth 3 / #400A — epistemic foundations: support graphs, truth maintenance, revision, defaults, paraconsistency This is **subpass A only**. It establishes representative epistemic formalisms and candidate architectures. #400 remains open for B/C/D. Do not advance to #401. ### Research question Given the source/semantic architecture produced by #398/#399, how should Machine Spirit represent and compute epistemic state when all of the following can coexist? - source A asserts P; - source B explicitly denies P; - an old source asserted P but later withdrew/corrected it; - P was true at t1 but not at t2; - rule R strictly derives P; - default D normally derives P unless exception E; - P holds only under hypothesis/context H; - multiple independent derivations support P; - a derivation loses a premise; - a trusted policy chooses a winner for one operational query without rewriting history. The core requirement is **truth/support/acceptance separation**. A proposition's stored evidence state is not the same thing as what a particular non-monotonic semantics warrants, and neither is the same thing as a destructive belief-set rewrite. ## Primary / authoritative sources inspected 1. Jon Doyle, **A Truth Maintenance System**, *Artificial Intelligence* 12 (1979), 231–272. Foundational justification-based TMS: beliefs record justifications/dependencies so changes can propagate through the dependency network. The key architectural lesson is to make reasons for belief explicit rather than storing only conclusions. Bibliographic/technical context confirmed through Stanford's logic-AI reference discussion of Doyle 1979. 2. Johan de Kleer, **An Assumption-based TMS**, *Artificial Intelligence* 28(2) (1986), 127–162, DOI 10.1016/0004-3702(86)90080-9. ATMS labels propositions with assumption environments; inconsistent assumption sets become nogoods. Crucially, multiple contexts/solutions can coexist without destructive global retraction. 3. C. E. Alchourrón, P. Gärdenfors, D. Makinson, **On the Logic of Theory Change: Partial Meet Contraction and Revision Functions**, *JSL* 50(2) (1985), 510–530, DOI 10.2307/2274239. AGM gives rationality postulates and representation results for contraction/revision by minimal change over belief sets. 4. Raymond Reiter, **A Logic for Default Reasoning**, *Artificial Intelligence* 13 (1980). Default theories define extensions: conclusions can depend on consistency/absence conditions, and a theory can have multiple extensions or problematic extension structure. This is useful semantics, but dangerous as a hidden global truth policy. 5. Michael Gelfond & Vladimir Lifschitz, **The Stable Model Semantics for Logic Programming** (ICLP/SLP 1988), 1070–1080; and **Classical Negation in Logic Programs and Disjunctive Databases**, *New Generation Computing* 9 (1991), 365–385. Stable-model semantics gives a declarative account of negation-as-failure; the 1991 extension adds explicit/classical negation and directly addresses incomplete information. 6. Allen Van Gelder, Kenneth Ross, John Schlipf, **The Well-Founded Semantics for General Logic Programs**, *JACM* 38(3) (1991), 620–650. WFS gives a unique partial/three-valued model for general logic programs. Operationally important here: unresolved negative recursion becomes undefined rather than forcing an arbitrary model. SWI-Prolog supports WFS using tabled predicates + `tnot/1`, including residual conditions for undefined answers. 7. Nuel Belnap, **How a Computer Should Think** (1977) / the Belnap-Dunn FOUR tradition. The key information model independently tracks positive and negative information, yielding states equivalent to neither / true-only / false-only / both. This is highly suitable as a *support-state summary* for inconsistent/incomplete memory, but it does not itself decide source priority or defaults. 8. Phan Minh Dung, **On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games**, *Artificial Intelligence* 77(2) (1995), 321–357, DOI 10.1016/0004-3702(94)00041-X. Abstract argumentation separates arguments from attack/acceptance semantics and supplies skeptical/credulous ways of computing warranted arguments. 9. Todd Green, Grigoris Karvounarakis, Val Tannen, **Provenance Semirings**, PODS 2007, DOI 10.1145/1265530.1265535. Provenance annotations can algebraically preserve alternative/conjunctive derivations through positive relational computation. Important boundary: provenance algebra is not automatically probability, trust, or truth. 10. Current execution evidence: SWI-Prolog's WFS implementation supports tabled negation and residual programs; goal-directed ASP/s(CASP) literature demonstrates query-directed stable-model reasoning with justification trees and constraints. These are viable execution mechanisms, not a reason to collapse the canonical epistemic representation into one engine's semantics. ## What current architecture already gets right #392/#394 and symbolic-memory already preserve several essential distinctions: - proposition != assertion; - positive support != explicit negative support; - source claim != world assertion; - provenance and justification are first-class; - append-only history rather than last-write-wins; - temporal validity, scenario and attribution are explicit; - `unknown` is not Prolog failure; - conflict is preservable instead of auto-resolved; - derived/materialized state is rebuildable. Those decisions survive. The missing layer is a precise separation between **evidence state**, **assumption environment**, **non-monotonic consequence**, and **revision policy**. --- # Candidate architecture A — global JTMS / retract-and-propagate belief state Maintain one current belief state. Each accepted node has justifications; when premises disappear, recursively retract dependent conclusions. Defaults can use absence conditions. Conceptually: ```prolog ep_node(N, Proposition). ep_justification(J, N, InPremises, OutPremises). ep_status(N, in_or_out). ``` ### Strengths - simple current-state query surface; - explanations/dependency invalidation are natural; - maps well to table invalidation and classic TMS machinery; - useful inside a single bounded reasoning context. ### Failure It is the wrong **canonical** model for Machine Spirit. One global IN/OUT status loses plurality: - source-specific contradictory worlds; - alternate hypotheses; - multiple default extensions; - historical states; - source correction vs world falsity; - later queries using different trust/resolution policies. A JTMS-style view remains useful as a **derived context-local materialization**, not the durable epistemic substrate. --- # Candidate architecture B — AGM belief-set revision as canonical truth state Represent Machine Spirit's current beliefs as a logically closed theory K. New evidence P triggers expansion/revision; correction/retraction triggers contraction; use entrenchment/preference to minimize change. ### Strengths - principled rationality postulates; - explicit notion of minimal change; - strong fit for a single agent maintaining a coherent commitment set; - useful for trusted policy layers that need one operational belief set. ### Failure Canonical Machine Spirit memory is intentionally **multi-source, append-only, inconsistent and contextual**. Classical AGM assumes a much cleaner target object than the evidence ledger we need. Destructively revising K when a news source changes would erase exactly the historical disagreement/provenance we want to preserve. AGM should therefore be available as a **revision projection/profile** over a selected theory/context/trust policy, not as the storage semantics. Example: ```text ledger: preserve A:P, B:not(P), correction(A,P), timestamps, derivations ↓ AGM-like operational projection under policy X ↓ selected coherent commitment set Kx ``` Changing policy X produces another projection, never mutated history. --- # Candidate architecture C — ATMS environments + paraconsistent evidence support **(preferred foundation)** Use immutable assertion/derivation records to build an **Epistemic Support Graph (ESG)**. Every proposition has independent positive and negative support sets. Justifications are hyperedges. Assumptions/context choices form explicit environments. Incompatible environments/nogoods are recorded rather than globally deleting one side. Conceptual data model: ```prolog ep_support(SupportId, PropositionRef, Polarity, % positive | negative AssertionOrDerivationRef, ContextRef, ValidityRef, ProvenanceRef). ep_justification(JustId, ConclusionSupport, RuleRef, PremiseSupportRefs, AssumptionRefs, ProfileRef, ContextRef). ep_environment(EnvId, AssumptionRefs, ContextRefs, PolicyRef, Meta). ep_nogood(NogoodId, AssumptionRefs, ReasonRef, ProvenanceRef). ep_lifecycle(EventId, Kind, % withdraw | supersede | retract_claim | invalidate_derivation | corroborate ... TargetRef, CauseRef, Time, ProvenanceRef). ``` The base evidence state for a proposition at context/time can be summarized as: ```text positive support? negative support? support_state no no neither yes no supported_only no yes refuted_only yes yes both/conflicted ``` This is deliberately Belnap-like **information state**, not the final consequence relation. ATMS-style environments preserve which assumption combinations support which conclusions. A contradiction marks an incompatible environment/nogood; it does not require deleting source evidence. de Kleer's ATMS is especially relevant because multiple contexts can coexist while avoiding repeated destructive retraction. ### Why this fits Machine Spirit - append-only storage maps naturally to evidence/support events; - multiple sources and hypotheses coexist; - every conclusion can retain exact derivation paths; - temporal and contextual filters happen before/while building an environment; - conflict becomes queryable information; - alternative resolution policies can share one canonical evidence substrate; - removing a premise invalidates derived support without deleting historical records; - provenance can be shared structurally across derivation DAGs. --- # Candidate architecture D — argumentation graph as canonical state Translate every supporting/refuting chain into an argument; contradictions/defaults/priorities become attack/defeat relations; use Dung-style grounded/preferred/stable semantics to calculate acceptance. ### Strengths - excellent explanation model for contested claims; - skeptical vs credulous conclusions are explicit; - default/prioritized reasoning and source conflicts can be presented as attack/defeat structures; - good fit for research/news disputes. ### Failure Making argumentation the primitive store adds unnecessary expansion for ordinary facts, temporal state and deterministic Horn consequences. Arguments should be a **derived epistemic view over ESG justifications**, especially for contested/default queries. --- # Preferred architecture: ESG + explicit Epistemic Profiles The architecture should therefore be: ```text immutable semantic assertions / source history ↓ EPISTEMIC SUPPORT GRAPH positive support | negative support justifications | assumptions | environments lifecycle | validity | provenance ↓ explicit epistemic profile ┌─────────┬─────────┬─────────┬─────────┐ │ │ │ │ │ paracons. WFS stable/ASP argument AGM-like support default models view revision summary view view view view │ │ │ │ │ └─────────┴─────────┴─────────┴─────────┘ ↓ warranted query outcome ↓ explanation / counterevidence ``` The **profile is part of query semantics**. It must never be inferred from whichever Prolog predicate happened to be called. Conceptual API: ```prolog epistemic_query(+TheoryRef, +Query, +Context, +EpistemicProfile, +Options, -Outcome). epistemic_support(+Proposition, +Context, +Options, -SupportState). epistemic_explain(+OutcomeRef, -Explanation). epistemic_counterevidence(+OutcomeRef, -CounterEvidence). ``` Outcome should distinguish at least: ```text support_state: neither | supported_only | refuted_only | both acceptance: warranted | unwarranted | undecided | credulous_only | profile_inconsistent profile: explicit profile/version assumptions: exact environment validity: query-time/context support: justification refs counterevidence: refuting justification refs ``` Do **not** compress this into one `confidence` float. --- ## Baseline epistemic profile direction A should establish the profile family but **not prematurely freeze every B/C/D semantic detail**. ### `support_paraconsistent` - always available for validated evidence; - reports independent support/refutation; - contradiction is non-explosive; - no automatic winner; - minimal assumptions. This should be the safest base query mode for heterogeneous memory. ### `well_founded_default` - candidate default/non-monotonic workhorse for compatible bounded logic-program fragments; - unique partial model; - negative cycles can remain undefined; - SWI already has practical WFS/tabling machinery and residual explanations; - **not** permitted to reinterpret explicit negative evidence as simple negation-as-failure. ### `stable_models` - optional profile for problems whose semantics genuinely require stable/default models; - multiple models are preserved; - expose skeptical (true in all admitted models) vs credulous (true in at least one) results; - zero models is an explicit epistemic failure state, not `false`; - solver/model enumeration limits must be surfaced. ### `argumentation` - derive arguments/attacks/defeats from ESG support/justifications; - especially appropriate for contested research, defaults and source-priority explanations; - semantics (grounded/preferred/etc.) must be named/versioned. ### `revision_projection` - AGM-inspired coherent operational commitment view; - runs only over selected admitted evidence/context with explicit preference/entrenchment policy; - output is a projection, never canonical deletion. --- ## Five distinctions that MUST become hard invariants ### 1. Retraction/withdrawal != explicit negation If a source says `P`, then later withdraws that statement: ```text withdraw(source_assertion(P)) != assert(not(P)) ``` The lifecycle event deactivates that source support in ordinary current views; it does not create negative world evidence unless the correction explicitly asserts ¬P. ### 2. Temporal change != belief revision ```text CEO(A) valid Jan-May CEO(B) valid Jun-current ``` is not a contradiction requiring AGM contraction. Both can be true at different valid times. Epistemic conflict detection must occur **after temporal/context qualification**. ### 3. Defeated default != false proposition If `birds normally fly` is defeated for a penguin, that means the default justification does not warrant `flies(penguin)` in that environment. It is not by itself explicit support for `not(flies(penguin))`. ### 4. Source trust != proposition probability A trust policy may control admission/preference, but: ```text trust(source)=0.8 ``` is not automatically: ```text P(P)=0.8 ``` Trust, compiler confidence, provenance multiplicity, probability and default priority remain separate dimensions. ### 5. Supersession != destruction Newer semantic projections or source revisions can supersede old active support, but historical support/derivation remains replayable. --- ## Defaults and rule priority: A-level decision Do not encode priority by Prolog clause order. Represent defaults explicitly: ```prolog ep_default(DefaultId, Preconditions, Conclusion, ExceptionConditions, PriorityInfo, Scope, Provenance). ``` Priority information is symbolic data and should support at least explicit declared priority and specificity evidence. The **resolution semantics belongs to an epistemic profile**. Reiter default logic demonstrates why this matters: default theories can have multiple extensions. Stable-model semantics similarly admits multiple models. Machine Spirit must expose this plurality where it exists rather than selecting the first solver result. Depth 3B should attack exact default priority/specificity behavior and competing non-monotonic semantics. --- ## Incremental invalidation model Canonical ESG records are immutable. Current support indexes/materialized warranted views are derived. When a premise becomes inactive for a query context because of correction, expiry, identity revision, context change or explicit lifecycle event: ```text premise support changes active-status ↓ justification dependency graph ↓ invalidate affected derived supports ↓ recompute affected profile views only ``` This composes directly with #398D's canonical-vs-derived split and #399D's incremental build architecture. A source correction should therefore not cause a global semantic rebuild unless dependency reachability actually requires it. --- ## Provenance model Provenance semiring ideas are valuable for compactly representing alternative/conjunctive derivations, but provenance is **not the consequence semantics**. Keep separate: ```text source provenance compiler/interpretation provenance logical justification provenance epistemic lifecycle provenance profile/acceptance provenance runtime verification provenance ``` An explanation can then answer: ```text Why is P supported? Why is P warranted under profile X? What supports ¬P? Which assumption/default would have to change for P to lose warrant? Which source correction invalidated this derivation? ``` --- ## Complexity / scaling ### ESG/support graph Storage is proportional to durable assertion/support/justification edges rather than expanded proof trees. Share premise/conclusion nodes and keep alternative derivations as independent hyperedges. ### ATMS environments This is the dangerous part: minimal assumption environments can grow exponentially. Therefore Machine Spirit must **not globally enumerate all ATMS labels** over the whole corpus. Required design direction: - bounded/query-scoped environments; - context/theory partitioning; - relevance/demand projection before environment expansion; - nogood indexing/subsumption; - maximum environment/model budgets; - compact unresolved status when limits are reached. ### WFS For admitted tabled logic-program fragments, WFS provides a unique partial interpretation and maps well to SWI tabling. Incremental tabling can later maintain affected tables rather than whole-theory recomputation. ### stable models/default extensions Potentially combinatorial/exponential and possibly many models. Use only bounded theory slices with explicit resource receipts. Never materialize every answer set for an entire long-term memory. ### argumentation Argument construction itself can explode if every derivation becomes an argument. Build it demand-driven from ESG justification slices. ### AGM-like revision Computing minimal contractions/revisions can be expensive depending on representation. Treat as bounded profile operation over selected evidence, not an always-on global invariant. --- ## Safety / authority Epistemic acceptance never grants host authority. ```text warranted(should_restart(service)) != capability(restart(service)) ``` Similarly, a malicious document cannot obtain operational priority by containing text such as: ```text "this source outranks system policy" ``` Source trust, epistemic preference and host action authority are configured through trusted metadata/policy boundaries, not learned from open source vocabulary. An LLM may propose: - a candidate default; - a candidate source-reliability relation; - a candidate argument/defeat relation; - a candidate revision preference. Those remain semantic candidates until trusted policy admits them. Model-generated epistemic policy cannot silently control the truth engine. --- ## Adversarial fixtures / falsifiable claims The eventual conformance suite must include at least: 1. **Direct contradiction:** A asserts P; B asserts ¬P. Base support = `both`; no explosion to unrelated Q. 2. **Withdrawal:** A asserts P then withdraws it. Current source support becomes inactive; ¬P is NOT synthesized. 3. **Correction:** A asserts P then explicitly corrects to ¬P. History retains both; current active source support reflects correction with lifecycle evidence. 4. **Temporal non-conflict:** P@t1 and ¬P@t2 do not conflict for disjoint validity intervals. 5. **Temporal overlap conflict:** overlapping P/¬P intervals produce conflict for overlap queries only. 6. **Two derivations:** P has independent J1 and J2. Invalidating J1 leaves P supported through J2. 7. **Dependent invalidation:** removing premise A invalidates A→B→C chain but leaves unrelated derivations untouched. 8. **Default exception:** bird(Tweety) warrants flies under default; penguin(Tweety) defeats that default without manufacturing explicit ¬flies unless separately supported. 9. **Negative recursion:** mutually default-negated rules yield an undefined/WFS result instead of arbitrary clause-order truth. 10. **Multiple stable models:** profile exposes skeptical vs credulous conclusions and does not choose first model. 11. **No stable model:** result says profile/model failure or inconsistency, not ordinary `false`. 12. **Conflicting trust policies:** same ESG under policy X and Y can yield different warranted views while canonical evidence remains identical. 13. **Attributed claim:** source_claims(S,P) does not satisfy unqualified-world P unless an explicit bridge/admission policy permits it. 14. **Scenario isolation:** P in hypothetical H never supports ordinary world P. 15. **Retraction of derivation rule:** rule lifecycle invalidation removes derived support but not source assertions. 16. **Nogood environment:** assumptions {A,B} marked incompatible; supports requiring both cannot become warranted in that environment. 17. **Resource ceiling:** environment/model explosion returns bounded `undecided/resource_limited` with receipt, never arbitrary top-1 truth. 18. **Authority injection:** remembered text declaring itself authoritative cannot alter epistemic/host policy. 19. **Explanation duality:** every warranted P can return support; every conflicted P can return both support and counterevidence. 20. **Replay:** same canonical ESG + profile version + context produces semantically equivalent warranted results after derived cache rebuild. --- ## Canonical design recommendations ### prolog-rlm #394 Add an explicit **Epistemic Support Graph + Epistemic Profile** boundary. `true/explicit_false/unknown/conflicted` should not be a single opaque enum produced directly from facts. Results need independent support/refutation state plus profile acceptance. Recommended result direction: ```prolog epistemic_outcome( Query, support_state(SupportState), acceptance(Acceptance), profile(ProfileRef), environment(EnvironmentRef), support(SupportRefs), counterevidence(CounterRefs), assumptions(AssumptionRefs), validity(Validity), unresolved(Unresolved), receipt(ReceiptRef)). ``` Do not finalize one universal default semantics in #394 before #400B/D. ### symbolic-memory #6 Persist immutable epistemic support/lifecycle/justification inputs sufficient to rebuild current epistemic views. The ledger should not persist a single mutable `truth` column as authority. Specifically preserve: - positive/negative support events; - assertion withdrawal/correction/supersession separately; - justification hyperedges; - assumptions/environment refs where durable; - temporal/context validity; - nogoods/incompatibility evidence where promoted; - epistemic profile/version on durable promoted conclusions/receipts; - rebuildable current support/acceptance indexes. ### symbolic-memory #7 Query APIs should accept an explicit epistemic profile and return **support state + acceptance + counterevidence**, not just `true/false/conflicted`. Cross-memory reasoning must make the evidence admission/trust/context policy explicit. `all memories` must not silently mean one global classical theory. ### #397 Mark Depth 3A complete only. Queue #400B next. --- ## Rejected simplifications - **One float confidence per fact:** loses contradiction, derivation plurality, default defeat, attribution and policy dependence. - **Latest assertion wins:** destroys provenance/history and misclassifies temporal change. - **Global classical consistency:** impossible/undesirable for heterogeneous web/news/log memory. - **Belnap FOUR as complete reasoning system:** excellent information-state basis, insufficient for defaults/priorities/revision. - **AGM as storage semantics:** useful coherent projection theory, wrong for append-only heterogeneous evidence. - **ATMS labels globally materialized:** semantically attractive but can explode combinatorially. - **ASP/stable models everywhere:** powerful profile, but multiple/no models and grounding/search cost make it unsuitable as universal base semantics. - **WFS everywhere:** excellent deterministic default profile for compatible programs, but does not by itself encode all source/trust/paraconsistent/revision semantics. - **Argumentation as primitive storage:** useful derived contested-belief view, unnecessarily expands ordinary deterministic knowledge. ## A-level decision **GO:** adopt a canonical **Epistemic Support Graph** over the existing proposition/assertion/context/justification substrate, with independent positive/negative support and explicit assumption environments. Treat all actual warrant/truth-maintenance behavior as versioned **Epistemic Profiles** over that substrate. Preferred default safety posture for arbitrary heterogeneous memory is paraconsistent support reporting; a bounded well-founded default profile is the strongest current candidate for deterministic zero-LLM default reasoning over admitted logic-program fragments. Stable-model, argumentation and AGM-style revision remain explicit opt-in profiles/views. This is a foundations decision, not final epistemics. **#400B must now attack it**, especially: default specificity/priorities, reinstatement, cycles of defeat, belief-vs-source trust, probabilistic/uncertain evidence, iterated revision, temporal correction, contradiction propagation, and whether ESG+profiles can avoid semantic mismatches between WFS/ASP/argumentation/paraconsistent views.
nsaspy commented 2026-09-08 01:47:43 +00:00
Author
Owner
Copy link

Depth 3 / #400B — adversarial epistemics: typed defeat, source dependence, circular support, and iterated correction

This is subpass B only. It attacks #400A's Epistemic Support Graph (ESG) + explicit Epistemic Profiles rather than assuming that architecture is correct. #400 remains open for C/D; do not advance to #401.

Research questions

The A design preserves positive/negative support and profile-relative warrant. B asks whether that is enough when real non-monotonic systems contain attacks on reasons, not merely opposite conclusions, and when evidence histories are correlated, cyclic, ordered, and temporally backdated.

Specifically:

  1. Can one ESG faithfully support WFS, stable-model, argumentation, defeasible/default and revision views without silently identifying their semantics?
  2. How should rebuttal, undermining and undercutting defeat differ structurally?
  3. Can default specificity/priority be represented without turning priority into clause order or one global scalar?
  4. How should reinstatement, defeat cycles, skeptical/credulous plurality and self-supporting derivations behave?
  5. How do we stop ten copied news stories from looking like ten independent corroborations?
  6. How should iterated corrections and backdated evidence affect what is believed now versus what was known then?
  7. Which epistemic outcomes are semantic (undefined, credulous_only, profile_inconsistent) versus operational (resource_limited)?

Primary / authoritative sources inspected

  1. John Pollock, work on defeasible reasoning / Cognitive Carpentry tradition. Pollock's crucial distinction is between rebutting defeaters, which support a conflicting conclusion, and undercutting defeaters, which attack the inference connection itself without supporting the opposite conclusion. This directly exposes a weakness in a proposition-only positive/negative support model.
  2. Sanjay Modgil & Henry Prakken, “The ASPIC+ framework for structured argumentation: a tutorial” (2014), Argument & Computation. ASPIC+ constructs arguments using strict vs defeasible rules and distinguishes attacks on ordinary premises, defeasible conclusions and defeasible inference steps; preferences decide when many attacks succeed as defeats, while undercutting attacks target rule applicability itself. It explicitly separates attack from defeat and provides rationality conditions for instantiations.
  3. Phan Minh Dung, “On the Acceptability of Arguments...” (1995), Artificial Intelligence 77(2). Grounded/preferred/stable argumentation semantics demonstrate that cycles/reinstatement and skeptical/credulous acceptance are properties of an attack/defeat graph, not reducible to one support bit.
  4. Francesca Toni, Assumption-Based Argumentation tutorial (2014). ABA derives attacks from rules, assumptions and contraries and supplies multiple semantics/dispute procedures. It reinforces the value of retaining assumptions as explicit epistemic objects rather than hiding them in procedural negation.
  5. Gerhard Brewka, “Reasoning about Priorities in Default Logic” (AAAI 1994) and Brewka & Eiter, “Preferred Answer Sets for Extended Logic Programs” (1998/1999). Prioritized non-monotonic reasoning is not safely reducible to arbitrary numeric scores or rule order; different priority semantics can produce different preferred extensions, and priority handling itself needs an explicit semantic contract.
  6. Alferes, Damásio & Pereira, “A Logic Programming System for Nonmonotonic Reasoning” (1995). Extended WFS with explicit negation supplies a top-down sound/complete procedure and a paraconsistent WFSX_p variant that can represent contradiction without explosion and identify integrity violations. This is strong evidence that WFS-style and paraconsistent behavior can coexist in one implementation family, but only under a precisely defined semantics.
  7. Alcântara, Damásio & Pereira, “An encompassing framework for Paraconsistent Logic Programs” (2005). Bilattice-inspired semantics integrate explicit/default negation and define paraconsistent well-founded and coherent answer-set variants. Key lesson: one can combine contradiction and non-monotonicity, but the combination is itself a named semantics—not an automatic property of storing four support states.
  8. Darwiche & Pearl, “On the Logic of Iterated Belief Revision” (1997). AGM is too weak for sequences of observations because belief-set contents do not fully determine rational future revisions; revision must operate on richer epistemic states. This strongly supports preserving revision policy state/history separately from the evidence ledger.
  9. Cordier & Siegel, “A temporal revision model for reasoning about world change” (1994). Distinguishes belief change about a static world from updates tracking an actually changing world. This reinforces A's temporal change != belief revision and motivates bitemporal treatment of backdated corrections.
  10. Dong, Berti-Equille & Srivastava, “Integrating Conflicting Data: The Role of Source Dependence” (PVLDB 2009) plus related CIDR work on source dependence. Truth-discovery accuracy changes materially when sources copy/derive from one another; repeated claims are not independent corroboration. Machine Spirit must therefore preserve source-dependence lineage as epistemic evidence rather than counting source IDs.

Attack on #400A: what breaks

A's ESG can represent:

support(P)
support(not P)
justification(J -> P)

but this does not distinguish these materially different cases:

1. rebuttal:
   J1 concludes P
   J2 concludes not(P)

2. premise undermining:
   J1 depends on premise A
   J2 establishes that A is not admissible in this context

3. inference undercutting:
   J1: looks_red(X) => red(X)
   J2: red_light(X)
       attacks applicability/reliability of the inference
       WITHOUT concluding not(red(X))

4. source-dependence defeat of corroboration:
   source B copied source A
   B's assertion still exists
   but A+B must not count as two independent supports

If every attack is encoded as negative support for P, the system fabricates false propositions. If every attack merely toggles a justification inactive, history and profile semantics disappear.

Therefore ESG survives, but must be refined with a typed defeat/attack layer whose targets can be propositions, support episodes, premises, inference applications, assumptions, source-independence claims, or policy/admission decisions.

Candidate architecture A — global priority-ranked defaults

Give each default/source/rule a numeric weight or total order. Resolve every conflict by taking the stronger item.

priority(rule_penguin, 90).
priority(rule_bird, 50).
trust(reuters, 0.9).

Strengths

  • simple;
  • deterministic;
  • easy to implement and cache;
  • intuitive for narrow policy systems.

Fatal problems

  • source trust, rule specificity, evidence quality, temporal recency, statistical confidence and authority are different dimensions;
  • total orders fabricate comparability where none exists;
  • reinstatement/cycles can depend on structure, not just winner weight;
  • copied sources can inflate evidence despite identical weights;
  • numeric priority hides why an attack succeeded;
  • different default semantics interpret the same ordering differently.

Rejected as canonical semantics. Numeric/ordered preferences may exist inside explicit profiles, but cannot be the substrate.

Candidate architecture B — translate everything to ASP/stable models

Compile ESG/defaults/priorities into extended logic programs; use answer sets/preferred answer sets as the universal epistemic semantics.

Strengths

  • powerful non-monotonic expressiveness;
  • mature skeptical/credulous semantics;
  • explicit negation and multiple models;
  • priorities can be represented with established approaches.

Failure

  • ordinary evidence support/counterevidence should remain queryable even when a program has no answer set;
  • source withdrawals, provenance and bitemporal history are not naturally the canonical object;
  • undercutting/source-dependence attacks must be encoded into program-specific machinery;
  • multiple model semantics are correct for some domains and excessive for others;
  • a profile with zero stable models must not erase the underlying evidence state.

Keep as a profile/engine, not the canonical epistemic representation.

Candidate architecture C — structured argumentation as canonical epistemic store

Turn every assertion/rule/derivation into arguments and every conflict/exception into attacks/defeats. Use ASPIC+/ABA-style structures as canonical memory.

Strengths

  • naturally represents rebuttal, undercutting, undermining, preferences, reinstatement and cycles;
  • excellent explanation surface;
  • clean skeptical/credulous acceptance semantics through Dung-family semantics.

Failure

  • massive over-expansion for ordinary monotonic facts/Horn closure;
  • argument identity is derivative of semantic evidence/justifications and can change with profile/admission policy;
  • temporal/materialized current views should not require storing all argument trees;
  • WFS/ASP/revision profiles should be able to consume the same evidence without going through one argumentation translation.

Use as a derived profile/view.

Candidate architecture D — ESG + Typed Defeat Graph + profile-specific acceptance (preferred)

Refine A into two canonical but distinct graph layers:

immutable semantic evidence / lifecycle
                ↓
      EPISTEMIC SUPPORT GRAPH
 propositions | support episodes | justifications
 assumptions | validity | provenance | source lineage
                ↓
        TYPED DEFEAT GRAPH
 rebut | undermine | undercut | invalidate
 dependence | incompatibility | policy-prefer
                ↓
      named epistemic profile
 WFS / paraconsistent / argumentation /
 stable-model / revision / specialized defaults
                ↓
       profile-relative warrant

The defeat layer does not itself decide acceptance. It preserves the structure required for profiles to do so honestly.

Conceptual records:

ep_attack(AttackId,
          Kind,                % rebut | undermine | undercut | invalidate | dependence
          AttackerRef,
          TargetRef,
          ContextRef,
          ValidityRef,
          ProvenanceRef).

ep_preference(PreferenceId,
              Dimension,       % rule_priority | specificity | source_policy | recency ...
              PreferredRef,
              OtherRef,
              Scope,
              BasisRefs,
              PolicyRef,
              ProvenanceRef).

ep_dependence(DependenceId,
              SourceOrEvidenceA,
              SourceOrEvidenceB,
              Kind,            % copied_from | syndicates | derived_from | shared_origin | suspected_dependence
              StrengthClass,
              EvidenceRefs,
              Validity,
              ProvenanceRef).

ep_preference is deliberately partial and typed. The substrate does not collapse unrelated dimensions into one total ranking.

B decision 1 — rebuttal, undermining and undercutting are hard semantic distinctions

Adopt a target taxonomy equivalent to:

rebut      -> attacks a defeasible conclusion with contrary conclusion
undermine  -> attacks admissibility/credibility of an ordinary premise/support episode
undercut   -> attacks applicability/reliability of a defeasible inference application
invalidate -> deterministic lifecycle/schema/context reason makes a support unusable in the selected query

Example:

camera says object is red                    support(P)
second calibrated camera says not red        rebut(P)
record says first camera was disconnected    undermine(camera_observation)
red floodlight was active                    undercut(looks_red => red)
sensor payload failed signature validation   invalidate(assertion)

Only the first two need a contrary proposition. Undercutting must never manufacture not(P).

This is a canonical refinement required for #394 and symbolic-memory #6/#7.

B decision 2 — preference is a typed relation, not one magic score

Default/source resolution must keep at least these dimensions distinguishable:

explicit rule priority
logical/schematic specificity
source admission policy
source independence/dependence
recency / transaction order
valid-time applicability
evidence-quality class
compiler/extraction quality
operational policy preference

A profile may define a composition policy, e.g. lexicographic or partial-order lifting, but the composition policy itself is named/versioned and appears in the warrant receipt.

No implicit:

0.9 trust + 0.8 confidence + newer timestamp = 2.7 truth

And no raw Prolog clause order.

B does not freeze one universal specificity algorithm. Brewka/Brewka-Eiter demonstrate that priority semantics are substantive and can alter extensions. C/D should decide which bounded profile(s) actually ship.

B decision 3 — source correlation is first-class epistemic structure

This is a major addition from truth-discovery/source-dependence research.

Suppose ten news sites repeat the same wire story:

A -> original report P
B -> copied from A
C -> syndicates B
D -> copied from A
...

Canonical evidence still contains ten assertion episodes. But a corroboration query must not conclude 10 independent sources.

Introduce an evidence-origin/dependence graph and expose both:

raw_support_count
independent_support_components

or equivalent structured summaries.

Hard rules:

  • dependence never deletes the copied assertion;
  • suspected dependence is not certain dependence;
  • source identity != evidence-origin identity;
  • two articles from the same publisher may be independent investigations;
  • two nominally different publishers may share one wire/service/source;
  • LLM-generated summaries citing the same underlying page are not independent evidence;
  • compiler duplication must not create epistemic corroboration.

The dependence graph influences selected profiles/admission/corroboration policies but does not become proposition probability by fiat.

B decision 4 — circular support cannot bootstrap itself into warrant

A raw justification graph can contain:

P <- Q
Q <- P

or nastier cycles through defaults/attacks.

The system needs an external-grounding invariant:

A strongly connected component of support dependencies cannot create warranted support solely from itself unless the selected epistemic profile explicitly gives fixed-point/model semantics that license it.

For monotonic strict/Horn support, an SCC with no externally supported seed contributes no new support.

For default/negative cycles:

  • WFS profile may return undefined;
  • stable-model profile may expose multiple/no stable models;
  • argumentation profile may yield undecided/unaccepted arguments depending on semantics;
  • paraconsistent support profile simply exposes the cycle and its raw dependencies without converting it to warrant.

Therefore self_supporting and circular_dependency become explanation conditions, not hidden implementation quirks.

B decision 5 — reinstatement belongs to acceptance semantics, not ledger mutation

Classic pattern:

A supports P
B defeats A
C defeats B

Some semantics reinstate A/P; cycles and floating reinstatement can differ under grounded vs preferred semantics.

Machine Spirit therefore must never store:

P = permanently defeated

Canonical state stores attack/defeat candidates and their provenance. The selected profile computes acceptance. Changing from grounded to preferred semantics may change warrant while the ESG/typed defeat graph remains identical.

This is exactly why argumentation remains a profile/view rather than canonical truth storage.

B decision 6 — iterated revision requires revision-state lineage

Darwiche-Pearl shows that the current belief set alone is insufficient for rational iterated revision. Machine Spirit's revision_projection must therefore be defined over an explicit revision epistemic state and operation sequence, not simply rerun AGM contraction on a set of currently accepted propositions.

Conceptual receipt/state:

ep_revision_state(StateId,
                  ParentStateRef,
                  RevisionOperatorRef,
                  PreferenceStateRef,
                  AdmittedEvidenceRefs,
                  OperationRef,
                  ResultCommitmentRefs,
                  ReceiptRef).

Hard invariant:

canonical evidence ledger != revision state != revision-projected belief set

Revision projections are rebuildable if all operator/version/state inputs are retained. Different revision operators may legitimately produce different commitment states.

B decision 7 — backdated corrections require bitemporal epistemics

A correction may arrive today stating that a claim was wrong since last month.

We must distinguish:

valid time       when the world/source content is asserted to apply
transaction time when Machine Spirit learned/recorded the evidence

Example:

Jan 10: source says CEO(A), valid Jan 1 onward
Feb 10: source corrects record: CEO(B) actually valid Jan 1 onward

Queries differ:

what is currently warranted about Jan 20?
    -> may prefer/support CEO(B), with correction provenance

what did Machine Spirit know on Jan 20?
    -> must expose CEO(A), because the correction had not arrived

Do not rewrite the old epistemic snapshot. This requires bitemporal lifecycle/query semantics downstream in symbolic-memory #6/#7.

Backdated correction is also distinct from an actual world-state transition on Feb 10.

B decision 8 — semantic outcomes need two orthogonal status axes

A-level acceptance was still too easy to overload.

Separate at least:

Semantic acceptance

skeptically_warranted
credulously_warranted
rejected
undefined
undecided
profile_inconsistent

Evaluation completeness

complete
bounded_partial
resource_limited
solver_error
unsupported_query_class

Why:

  • undefined is a semantic result under e.g. WFS negative recursion;
  • undecided can be a legitimate argumentation/default state;
  • credulously_warranted means some but not all admitted models/extensions;
  • resource_limited says the computation did not finish enough to establish the requested semantic status;
  • profile_inconsistent/no-model is not ordinary refutation.

Never collapse computational incompleteness into epistemic uncertainty.

B decision 9 — WFS, ASP, argumentation and paraconsistent views can share ESG only through explicit translation contracts

The attack confirms the A architecture can serve multiple profiles, but there is no semantics-free universal lowering.

Required profile declaration should include something equivalent to:

input admissibility fragment
explicit-negation interpretation
default-negation interpretation
contradiction policy
attack/defeat translation
preference lifting
cycle semantics
skeptical/credulous definition
model/extension failure semantics
query relevance guarantees
explanation mapping

Examples:

  • WFS/WFSX-style profile: unique partial fixed point; undefined negative cycles; explicit negation distinct; a paraconsistent variant may retain contradiction.
  • stable-model profile: may have multiple or zero models; skeptical/credulous are model-relative.
  • structured argumentation profile: constructs arguments/attacks/defeats; grounded vs preferred semantics are separate versions.
  • support-paraconsistent profile: reports evidence topology without importing one of the above non-monotonic consequence relations.

Thus the common ESG is an evidence/justification substrate, not a universal proof theory.

Revised preferred architecture after adversarial attack

#392 propositions/assertions/contexts
              ↓
immutable evidence + lifecycle
              ↓
┌───────────────────────────────────┐
│ EPISTEMIC SUPPORT GRAPH           │
│ positive/negative support         │
│ justifications/assumptions        │
│ valid + transaction time          │
│ provenance/source lineage         │
└────────────────┬──────────────────┘
                 ↓
┌───────────────────────────────────┐
│ TYPED DEFEAT / DEPENDENCE GRAPH   │
│ rebut / undermine / undercut      │
│ invalidate / incompatibility      │
│ source/evidence dependence        │
│ typed partial preferences         │
└────────────────┬──────────────────┘
                 ↓
      explicit profile translator
                 ↓
      profile-specific semantics
 WFSX | stable/ASP | argumentation |
 revision | support-paraconsistent
                 ↓
┌───────────────────────────────────┐
│ WARRANT RECEIPT                   │
│ semantic acceptance               │
│ evaluation completeness           │
│ support + counterevidence         │
│ attacks/defeats/preference basis  │
│ assumptions/models/extensions     │
│ valid-time + transaction-time     │
│ profile/operator/version          │
└───────────────────────────────────┘

This is a stronger architecture than #400A's plain ESG+profiles while preserving A's central insight.

Complexity / scaling implications

  • Typed defeat graph should be demand-generated where possible. Do not materialize every possible structured argument globally.
  • Ordinary direct contradiction/support indexes remain cheap and always available.
  • WFS on finite propositional/general admitted fragments remains attractive for deterministic default queries; known alternating-fixpoint evaluation is polynomial for finite propositional programs, while richer combined fragments can be much harder.
  • Stable-model enumeration is inherently potentially exponential/multi-model; bounds and skeptical-query strategies are mandatory.
  • Argument graph construction can explode combinatorially through alternative derivations. Build arguments query-locally from shared ESG justification DAGs and hash-cons subarguments.
  • Source-dependence analysis can be expensive if modeled as all-pairs source comparison. Persist explicit provenance links when known and use bounded inference for suspected dependence; do not require O(S²) global recomputation on every append.
  • Circular-support detection is naturally SCC-based over dependency graphs and can be incremental.
  • Bitemporal indexes require both valid-time and transaction-time dimensions; current-warrant and historical-knowledge queries must choose the correct axis explicitly.

Epistemic/provenance implications

Add two provenance dimensions beyond #400A's baseline:

defeat provenance
    why/where an attack or preference came from

dependence provenance
    why two evidence episodes are believed to share an origin

Do not treat source-dependence inference as fact without its own evidence/status.

A warrant explanation should now be able to say not only:

P because A + rule R

but:

P is skeptically warranted under profile X because
- J1 supports P;
- rebuttal J2 is defeated by C;
- J1's inference is not undercut in context T;
- B and C share source origin O, so they count as one corroboration component under policy Q;
- the conclusion is valid at world-time V;
- this warrant was evaluated at transaction-time K.

Safety / authority implications

  • Source trust/preference never grants host capability.
  • A high-priority remembered policy statement remains epistemic knowledge, not authorization.
  • An undercut claiming that a safety verifier is unreliable cannot disable the actual runtime verifier; semantic epistemics and host enforcement remain separate.
  • Model-generated source-dependence or priority relations are inert candidates until admitted under the selected semantic policy.
  • No preference relation can resolve by symbol name to executable Prolog or host action.
  • resource_limited cannot be interpreted as permission to choose the most convenient result.

Adversarial fixtures / falsifiable conformance

B adds at least these required fixtures:

  1. Undercutter without negation — looks_red -> red, red-light evidence undercuts the rule; result must lose defeasible warrant for red without gaining support for not red.
  2. Rebuttal vs undercut distinction — opposite camera observation creates negative support; red-light condition attacks inference only. Explanations must differ.
  3. Premise undermining — invalid signature attacks observation admissibility, not world proposition.
  4. Specificity disagreement — general bird default vs penguin exception under two named priority profiles; profile change may change warrant, ledger does not.
  5. Reinstatement — A defeated by B, B defeated by C; grounded/preferred result captured according to named semantics.
  6. Odd defeat cycle — must not select first traversal result.
  7. Floating reinstatement — grounded vs preferred divergence is surfaced, not erased.
  8. Self-support cycle — P<-Q, Q<-P with no external seed must not bootstrap ordinary strict support.
  9. Seeded support cycle — external P support may propagate through strict SCC; explanation retains external seed.
  10. Default negative cycle — WFS returns semantic undefined with residual/cycle explanation.
  11. Stable-model plurality — skeptical vs credulous results differ and are reported explicitly.
  12. No stable model — returns profile/model inconsistency, not false.
  13. Copied-source swarm — ten syndicated copies retain ten assertions but one evidence-origin component under explicit dependence links.
  14. False dependence suspicion — suspected copying cannot be silently treated as proven dependence.
  15. Same publisher independent reports — independence may be preserved when provenance demonstrates separate investigation.
  16. LLM summary echo — multiple summaries of one underlying article cannot count as independent corroboration.
  17. Iterated revision order — evidence sequence A,B,A under two revision operators produces reproducible operator-relative states; canonical ledger unchanged.
  18. Backdated correction — current belief about past time changes; historical known-at query does not rewrite itself.
  19. World change vs correction — actual CEO transition and later correction of old data produce distinct temporal/lifecycle structures.
  20. Conflicting priority dimensions — source policy favors A while rule specificity favors B; no implicit numeric merge; named policy must determine result or return unresolved preference.
  21. Preference cycle — A>B, B>C, C>A must be detected and handled by profile semantics, not sort accident.
  22. Undercut safety boundary — semantic evidence saying verifier is unreliable must not disable runtime verifier/capability gate.
  23. Resource bound during preferred-extension search — returns incomplete/resource-limited evaluation, never arbitrary skeptical warrant.
  24. Profile translation mismatch — unsupported attack type/profile combination must fail profile admission explicitly rather than be dropped.

Cross-profile differential oracle:

same ESG + same typed defeat/dependence graph
        + explicit profile/version
        + same query/context/times
                ↓
rebuild after cache deletion
                ↓
identical semantic warrant/receipt

Different profiles may legitimately disagree, but the disagreement must be attributable to the profile contract.

Canonical changes required from B

prolog-rlm #394

Add:

  • typed rebut/undermine/undercut/invalidate attack semantics;
  • typed partial preference relations with named composition policy;
  • source/evidence dependence input for corroboration-aware profiles;
  • circular-support/SCC handling and external-grounding invariant;
  • reinstatement/cycle semantics declared per profile;
  • bitemporal valid-time vs transaction-time query semantics;
  • split semantic acceptance from evaluation completeness;
  • explicit profile translation/admission contracts.

symbolic-memory #6

Persist enough append-only evidence to reconstruct:

  • typed attacks/defeats and their provenance;
  • partial preference assertions/policies;
  • evidence-origin/source-dependence relations;
  • both valid-time and transaction-time lifecycle;
  • revision-state lineage when a promoted revision projection must be replayable;
  • circular-dependency metadata only where promoted; ordinary SCC caches remain derived.

symbolic-memory #7

Query outcomes should expose:

semantic_acceptance
evaluation_completeness
support/counterevidence
attack/defeat path
preference basis + policy
independence/dependence summary
valid-time
transaction-time
profile/version/operator

Add known_at(TransactionTime) separately from valid_at(WorldTime).

Unresolved questions intentionally preserved for #400C/#400D

  1. Which exact finite default/defeasible profile(s) should be first-class in v1: WFSX-like, defeasible logic, ASPIC+/ABA-derived, preferred ASP, or more than one?
  2. Which preference-lifting principles satisfy the desired rationality postulates for our admitted strict/defeasible rule fragments?
  3. How should source-dependence inference itself combine with trust/probability without circular truth-discovery feedback?
  4. Should contradiction propagation be relation/profile-local or use a standard bilattice layer across selected profiles?
  5. What is the exact bounded algorithm for query-local structured argument generation over shared ESG justifications?
  6. What portions of iterated revision state should be durable versus recomputable from evidence + operator history?
  7. How are epistemic profiles composed across imported theories/contexts without assuming one global non-monotonic semantics? This is a major #400C question.
  8. Which indexes/materializations make bitemporal + attack/dependence queries fast enough at large memory scale? #400D owns execution/scaling.

B conclusion

The A architecture survives, but only after a significant refinement:

Machine Spirit's canonical epistemic substrate should be ESG + a typed Defeat/Dependence Graph. Warrant remains profile-relative. Attacks on conclusions, premises, inference links, and evidence independence are not the same thing; priorities are typed/partial policy data; circular support cannot bootstrap itself; correction requires bitemporal history; and computational incompleteness is separate from epistemic status.

This does not freeze one universal default semantics. #400C must now research composition/interoperability among epistemic profiles/theories and #400D must prove bounded executable behavior.

## Depth 3 / #400B — adversarial epistemics: typed defeat, source dependence, circular support, and iterated correction This is **subpass B only**. It attacks #400A's `Epistemic Support Graph (ESG) + explicit Epistemic Profiles` rather than assuming that architecture is correct. #400 remains open for C/D; do not advance to #401. ### Research questions The A design preserves positive/negative support and profile-relative warrant. B asks whether that is enough when real non-monotonic systems contain attacks on *reasons*, not merely opposite conclusions, and when evidence histories are correlated, cyclic, ordered, and temporally backdated. Specifically: 1. Can one ESG faithfully support WFS, stable-model, argumentation, defeasible/default and revision views without silently identifying their semantics? 2. How should rebuttal, undermining and **undercutting** defeat differ structurally? 3. Can default specificity/priority be represented without turning priority into clause order or one global scalar? 4. How should reinstatement, defeat cycles, skeptical/credulous plurality and self-supporting derivations behave? 5. How do we stop ten copied news stories from looking like ten independent corroborations? 6. How should iterated corrections and backdated evidence affect `what is believed now` versus `what was known then`? 7. Which epistemic outcomes are semantic (`undefined`, `credulous_only`, `profile_inconsistent`) versus operational (`resource_limited`)? --- ## Primary / authoritative sources inspected 1. **John Pollock**, work on defeasible reasoning / *Cognitive Carpentry* tradition. Pollock's crucial distinction is between **rebutting defeaters**, which support a conflicting conclusion, and **undercutting defeaters**, which attack the inference connection itself without supporting the opposite conclusion. This directly exposes a weakness in a proposition-only positive/negative support model. 2. **Sanjay Modgil & Henry Prakken, “The ASPIC+ framework for structured argumentation: a tutorial” (2014)**, Argument & Computation. ASPIC+ constructs arguments using strict vs defeasible rules and distinguishes attacks on ordinary premises, defeasible conclusions and defeasible inference steps; preferences decide when many attacks succeed as defeats, while undercutting attacks target rule applicability itself. It explicitly separates attack from defeat and provides rationality conditions for instantiations. 3. **Phan Minh Dung, “On the Acceptability of Arguments...” (1995)**, Artificial Intelligence 77(2). Grounded/preferred/stable argumentation semantics demonstrate that cycles/reinstatement and skeptical/credulous acceptance are properties of an attack/defeat graph, not reducible to one support bit. 4. **Francesca Toni, Assumption-Based Argumentation tutorial (2014)**. ABA derives attacks from rules, assumptions and contraries and supplies multiple semantics/dispute procedures. It reinforces the value of retaining assumptions as explicit epistemic objects rather than hiding them in procedural negation. 5. **Gerhard Brewka, “Reasoning about Priorities in Default Logic” (AAAI 1994)** and **Brewka & Eiter, “Preferred Answer Sets for Extended Logic Programs” (1998/1999)**. Prioritized non-monotonic reasoning is not safely reducible to arbitrary numeric scores or rule order; different priority semantics can produce different preferred extensions, and priority handling itself needs an explicit semantic contract. 6. **Alferes, Damásio & Pereira, “A Logic Programming System for Nonmonotonic Reasoning” (1995)**. Extended WFS with explicit negation supplies a top-down sound/complete procedure and a **paraconsistent WFSX_p** variant that can represent contradiction without explosion and identify integrity violations. This is strong evidence that WFS-style and paraconsistent behavior can coexist in one implementation family, but only under a precisely defined semantics. 7. **Alcântara, Damásio & Pereira, “An encompassing framework for Paraconsistent Logic Programs” (2005)**. Bilattice-inspired semantics integrate explicit/default negation and define paraconsistent well-founded and coherent answer-set variants. Key lesson: one can combine contradiction and non-monotonicity, but the combination is itself a named semantics—not an automatic property of storing four support states. 8. **Darwiche & Pearl, “On the Logic of Iterated Belief Revision” (1997)**. AGM is too weak for sequences of observations because belief-set contents do not fully determine rational future revisions; revision must operate on richer **epistemic states**. This strongly supports preserving revision policy state/history separately from the evidence ledger. 9. **Cordier & Siegel, “A temporal revision model for reasoning about world change” (1994)**. Distinguishes belief change about a static world from updates tracking an actually changing world. This reinforces A's `temporal change != belief revision` and motivates bitemporal treatment of backdated corrections. 10. **Dong, Berti-Equille & Srivastava, “Integrating Conflicting Data: The Role of Source Dependence” (PVLDB 2009)** plus related CIDR work on source dependence. Truth-discovery accuracy changes materially when sources copy/derive from one another; repeated claims are not independent corroboration. Machine Spirit must therefore preserve **source-dependence lineage** as epistemic evidence rather than counting source IDs. --- # Attack on #400A: what breaks A's ESG can represent: ```text support(P) support(not P) justification(J -> P) ``` but this does **not** distinguish these materially different cases: ```text 1. rebuttal: J1 concludes P J2 concludes not(P) 2. premise undermining: J1 depends on premise A J2 establishes that A is not admissible in this context 3. inference undercutting: J1: looks_red(X) => red(X) J2: red_light(X) attacks applicability/reliability of the inference WITHOUT concluding not(red(X)) 4. source-dependence defeat of corroboration: source B copied source A B's assertion still exists but A+B must not count as two independent supports ``` If every attack is encoded as negative support for `P`, the system fabricates false propositions. If every attack merely toggles a justification inactive, history and profile semantics disappear. Therefore **ESG survives, but must be refined with a typed defeat/attack layer whose targets can be propositions, support episodes, premises, inference applications, assumptions, source-independence claims, or policy/admission decisions.** --- # Candidate architecture A — global priority-ranked defaults Give each default/source/rule a numeric weight or total order. Resolve every conflict by taking the stronger item. ```prolog priority(rule_penguin, 90). priority(rule_bird, 50). trust(reuters, 0.9). ``` ### Strengths - simple; - deterministic; - easy to implement and cache; - intuitive for narrow policy systems. ### Fatal problems - source trust, rule specificity, evidence quality, temporal recency, statistical confidence and authority are different dimensions; - total orders fabricate comparability where none exists; - reinstatement/cycles can depend on *structure*, not just winner weight; - copied sources can inflate evidence despite identical weights; - numeric priority hides why an attack succeeded; - different default semantics interpret the same ordering differently. **Rejected as canonical semantics.** Numeric/ordered preferences may exist inside explicit profiles, but cannot be the substrate. --- # Candidate architecture B — translate everything to ASP/stable models Compile ESG/defaults/priorities into extended logic programs; use answer sets/preferred answer sets as the universal epistemic semantics. ### Strengths - powerful non-monotonic expressiveness; - mature skeptical/credulous semantics; - explicit negation and multiple models; - priorities can be represented with established approaches. ### Failure - ordinary evidence support/counterevidence should remain queryable even when a program has no answer set; - source withdrawals, provenance and bitemporal history are not naturally the canonical object; - undercutting/source-dependence attacks must be encoded into program-specific machinery; - multiple model semantics are correct for some domains and excessive for others; - a profile with zero stable models must not erase the underlying evidence state. **Keep as a profile/engine, not the canonical epistemic representation.** --- # Candidate architecture C — structured argumentation as canonical epistemic store Turn every assertion/rule/derivation into arguments and every conflict/exception into attacks/defeats. Use ASPIC+/ABA-style structures as canonical memory. ### Strengths - naturally represents rebuttal, undercutting, undermining, preferences, reinstatement and cycles; - excellent explanation surface; - clean skeptical/credulous acceptance semantics through Dung-family semantics. ### Failure - massive over-expansion for ordinary monotonic facts/Horn closure; - argument identity is derivative of semantic evidence/justifications and can change with profile/admission policy; - temporal/materialized current views should not require storing all argument trees; - WFS/ASP/revision profiles should be able to consume the same evidence without going through one argumentation translation. **Use as a derived profile/view.** --- # Candidate architecture D — ESG + Typed Defeat Graph + profile-specific acceptance **(preferred)** Refine A into two canonical but distinct graph layers: ```text immutable semantic evidence / lifecycle ↓ EPISTEMIC SUPPORT GRAPH propositions | support episodes | justifications assumptions | validity | provenance | source lineage ↓ TYPED DEFEAT GRAPH rebut | undermine | undercut | invalidate dependence | incompatibility | policy-prefer ↓ named epistemic profile WFS / paraconsistent / argumentation / stable-model / revision / specialized defaults ↓ profile-relative warrant ``` The defeat layer does **not** itself decide acceptance. It preserves the structure required for profiles to do so honestly. Conceptual records: ```prolog ep_attack(AttackId, Kind, % rebut | undermine | undercut | invalidate | dependence AttackerRef, TargetRef, ContextRef, ValidityRef, ProvenanceRef). ep_preference(PreferenceId, Dimension, % rule_priority | specificity | source_policy | recency ... PreferredRef, OtherRef, Scope, BasisRefs, PolicyRef, ProvenanceRef). ep_dependence(DependenceId, SourceOrEvidenceA, SourceOrEvidenceB, Kind, % copied_from | syndicates | derived_from | shared_origin | suspected_dependence StrengthClass, EvidenceRefs, Validity, ProvenanceRef). ``` `ep_preference` is deliberately **partial and typed**. The substrate does not collapse unrelated dimensions into one total ranking. --- # B decision 1 — rebuttal, undermining and undercutting are hard semantic distinctions Adopt a target taxonomy equivalent to: ```text rebut -> attacks a defeasible conclusion with contrary conclusion undermine -> attacks admissibility/credibility of an ordinary premise/support episode undercut -> attacks applicability/reliability of a defeasible inference application invalidate -> deterministic lifecycle/schema/context reason makes a support unusable in the selected query ``` Example: ```text camera says object is red support(P) second calibrated camera says not red rebut(P) record says first camera was disconnected undermine(camera_observation) red floodlight was active undercut(looks_red => red) sensor payload failed signature validation invalidate(assertion) ``` Only the first two need a contrary proposition. **Undercutting must never manufacture `not(P)`.** This is a canonical refinement required for #394 and symbolic-memory #6/#7. --- # B decision 2 — preference is a typed relation, not one magic score Default/source resolution must keep at least these dimensions distinguishable: ```text explicit rule priority logical/schematic specificity source admission policy source independence/dependence recency / transaction order valid-time applicability evidence-quality class compiler/extraction quality operational policy preference ``` A profile may define a composition policy, e.g. lexicographic or partial-order lifting, but the **composition policy itself is named/versioned and appears in the warrant receipt**. No implicit: ```text 0.9 trust + 0.8 confidence + newer timestamp = 2.7 truth ``` And no raw Prolog clause order. B does **not** freeze one universal specificity algorithm. Brewka/Brewka-Eiter demonstrate that priority semantics are substantive and can alter extensions. C/D should decide which bounded profile(s) actually ship. --- # B decision 3 — source correlation is first-class epistemic structure This is a major addition from truth-discovery/source-dependence research. Suppose ten news sites repeat the same wire story: ```text A -> original report P B -> copied from A C -> syndicates B D -> copied from A ... ``` Canonical evidence still contains ten assertion episodes. But a corroboration query must not conclude `10 independent sources`. Introduce an **evidence-origin/dependence graph** and expose both: ```text raw_support_count independent_support_components ``` or equivalent structured summaries. Hard rules: - dependence never deletes the copied assertion; - suspected dependence is not certain dependence; - source identity != evidence-origin identity; - two articles from the same publisher may be independent investigations; - two nominally different publishers may share one wire/service/source; - LLM-generated summaries citing the same underlying page are not independent evidence; - compiler duplication must not create epistemic corroboration. The dependence graph influences selected profiles/admission/corroboration policies but **does not become proposition probability by fiat**. --- # B decision 4 — circular support cannot bootstrap itself into warrant A raw justification graph can contain: ```text P <- Q Q <- P ``` or nastier cycles through defaults/attacks. The system needs an **external-grounding invariant**: > A strongly connected component of support dependencies cannot create warranted support solely from itself unless the selected epistemic profile explicitly gives fixed-point/model semantics that license it. For monotonic strict/Horn support, an SCC with no externally supported seed contributes no new support. For default/negative cycles: - WFS profile may return `undefined`; - stable-model profile may expose multiple/no stable models; - argumentation profile may yield undecided/unaccepted arguments depending on semantics; - paraconsistent support profile simply exposes the cycle and its raw dependencies without converting it to warrant. Therefore `self_supporting` and `circular_dependency` become explanation conditions, not hidden implementation quirks. --- # B decision 5 — reinstatement belongs to acceptance semantics, not ledger mutation Classic pattern: ```text A supports P B defeats A C defeats B ``` Some semantics reinstate A/P; cycles and floating reinstatement can differ under grounded vs preferred semantics. Machine Spirit therefore must never store: ```text P = permanently defeated ``` Canonical state stores attack/defeat candidates and their provenance. The selected profile computes acceptance. Changing from grounded to preferred semantics may change warrant while the ESG/typed defeat graph remains identical. This is exactly why argumentation remains a profile/view rather than canonical truth storage. --- # B decision 6 — iterated revision requires revision-state lineage Darwiche-Pearl shows that the current belief set alone is insufficient for rational iterated revision. Machine Spirit's `revision_projection` must therefore be defined over an explicit **revision epistemic state** and operation sequence, not simply rerun AGM contraction on a set of currently accepted propositions. Conceptual receipt/state: ```prolog ep_revision_state(StateId, ParentStateRef, RevisionOperatorRef, PreferenceStateRef, AdmittedEvidenceRefs, OperationRef, ResultCommitmentRefs, ReceiptRef). ``` Hard invariant: ```text canonical evidence ledger != revision state != revision-projected belief set ``` Revision projections are rebuildable if all operator/version/state inputs are retained. Different revision operators may legitimately produce different commitment states. --- # B decision 7 — backdated corrections require bitemporal epistemics A correction may arrive today stating that a claim was wrong since last month. We must distinguish: ```text valid time when the world/source content is asserted to apply transaction time when Machine Spirit learned/recorded the evidence ``` Example: ```text Jan 10: source says CEO(A), valid Jan 1 onward Feb 10: source corrects record: CEO(B) actually valid Jan 1 onward ``` Queries differ: ```text what is currently warranted about Jan 20? -> may prefer/support CEO(B), with correction provenance what did Machine Spirit know on Jan 20? -> must expose CEO(A), because the correction had not arrived ``` Do not rewrite the old epistemic snapshot. This requires bitemporal lifecycle/query semantics downstream in symbolic-memory #6/#7. Backdated correction is also distinct from an actual world-state transition on Feb 10. --- # B decision 8 — semantic outcomes need two orthogonal status axes A-level `acceptance` was still too easy to overload. Separate at least: ### Semantic acceptance ```text skeptically_warranted credulously_warranted rejected undefined undecided profile_inconsistent ``` ### Evaluation completeness ```text complete bounded_partial resource_limited solver_error unsupported_query_class ``` Why: - `undefined` is a semantic result under e.g. WFS negative recursion; - `undecided` can be a legitimate argumentation/default state; - `credulously_warranted` means some but not all admitted models/extensions; - `resource_limited` says the computation did not finish enough to establish the requested semantic status; - `profile_inconsistent`/no-model is not ordinary refutation. Never collapse computational incompleteness into epistemic uncertainty. --- # B decision 9 — WFS, ASP, argumentation and paraconsistent views can share ESG only through explicit translation contracts The attack confirms the A architecture **can** serve multiple profiles, but there is no semantics-free universal lowering. Required profile declaration should include something equivalent to: ```text input admissibility fragment explicit-negation interpretation default-negation interpretation contradiction policy attack/defeat translation preference lifting cycle semantics skeptical/credulous definition model/extension failure semantics query relevance guarantees explanation mapping ``` Examples: - WFS/WFSX-style profile: unique partial fixed point; undefined negative cycles; explicit negation distinct; a paraconsistent variant may retain contradiction. - stable-model profile: may have multiple or zero models; skeptical/credulous are model-relative. - structured argumentation profile: constructs arguments/attacks/defeats; grounded vs preferred semantics are separate versions. - support-paraconsistent profile: reports evidence topology without importing one of the above non-monotonic consequence relations. Thus the common ESG is an **evidence/justification substrate**, not a universal proof theory. --- ## Revised preferred architecture after adversarial attack ```text #392 propositions/assertions/contexts ↓ immutable evidence + lifecycle ↓ ┌───────────────────────────────────┐ │ EPISTEMIC SUPPORT GRAPH │ │ positive/negative support │ │ justifications/assumptions │ │ valid + transaction time │ │ provenance/source lineage │ └────────────────┬──────────────────┘ ↓ ┌───────────────────────────────────┐ │ TYPED DEFEAT / DEPENDENCE GRAPH │ │ rebut / undermine / undercut │ │ invalidate / incompatibility │ │ source/evidence dependence │ │ typed partial preferences │ └────────────────┬──────────────────┘ ↓ explicit profile translator ↓ profile-specific semantics WFSX | stable/ASP | argumentation | revision | support-paraconsistent ↓ ┌───────────────────────────────────┐ │ WARRANT RECEIPT │ │ semantic acceptance │ │ evaluation completeness │ │ support + counterevidence │ │ attacks/defeats/preference basis │ │ assumptions/models/extensions │ │ valid-time + transaction-time │ │ profile/operator/version │ └───────────────────────────────────┘ ``` This is a stronger architecture than #400A's plain ESG+profiles while preserving A's central insight. --- ## Complexity / scaling implications - **Typed defeat graph** should be demand-generated where possible. Do not materialize every possible structured argument globally. - Ordinary direct contradiction/support indexes remain cheap and always available. - WFS on finite propositional/general admitted fragments remains attractive for deterministic default queries; known alternating-fixpoint evaluation is polynomial for finite propositional programs, while richer combined fragments can be much harder. - Stable-model enumeration is inherently potentially exponential/multi-model; bounds and skeptical-query strategies are mandatory. - Argument graph construction can explode combinatorially through alternative derivations. Build arguments query-locally from shared ESG justification DAGs and hash-cons subarguments. - Source-dependence analysis can be expensive if modeled as all-pairs source comparison. Persist explicit provenance links when known and use bounded inference for suspected dependence; do not require O(S²) global recomputation on every append. - Circular-support detection is naturally SCC-based over dependency graphs and can be incremental. - Bitemporal indexes require both valid-time and transaction-time dimensions; current-warrant and historical-knowledge queries must choose the correct axis explicitly. --- ## Epistemic/provenance implications Add two provenance dimensions beyond #400A's baseline: ```text defeat provenance why/where an attack or preference came from dependence provenance why two evidence episodes are believed to share an origin ``` Do not treat source-dependence inference as fact without its own evidence/status. A warrant explanation should now be able to say not only: ```text P because A + rule R ``` but: ```text P is skeptically warranted under profile X because - J1 supports P; - rebuttal J2 is defeated by C; - J1's inference is not undercut in context T; - B and C share source origin O, so they count as one corroboration component under policy Q; - the conclusion is valid at world-time V; - this warrant was evaluated at transaction-time K. ``` --- ## Safety / authority implications - Source trust/preference never grants host capability. - A high-priority remembered policy statement remains epistemic knowledge, not authorization. - An `undercut` claiming that a safety verifier is unreliable cannot disable the actual runtime verifier; semantic epistemics and host enforcement remain separate. - Model-generated source-dependence or priority relations are inert candidates until admitted under the selected semantic policy. - No preference relation can resolve by symbol name to executable Prolog or host action. - `resource_limited` cannot be interpreted as permission to choose the most convenient result. --- ## Adversarial fixtures / falsifiable conformance B adds at least these required fixtures: 1. **Undercutter without negation** — `looks_red -> red`, red-light evidence undercuts the rule; result must lose defeasible warrant for `red` without gaining support for `not red`. 2. **Rebuttal vs undercut distinction** — opposite camera observation creates negative support; red-light condition attacks inference only. Explanations must differ. 3. **Premise undermining** — invalid signature attacks observation admissibility, not world proposition. 4. **Specificity disagreement** — general bird default vs penguin exception under two named priority profiles; profile change may change warrant, ledger does not. 5. **Reinstatement** — A defeated by B, B defeated by C; grounded/preferred result captured according to named semantics. 6. **Odd defeat cycle** — must not select first traversal result. 7. **Floating reinstatement** — grounded vs preferred divergence is surfaced, not erased. 8. **Self-support cycle** — `P<-Q, Q<-P` with no external seed must not bootstrap ordinary strict support. 9. **Seeded support cycle** — external P support may propagate through strict SCC; explanation retains external seed. 10. **Default negative cycle** — WFS returns semantic `undefined` with residual/cycle explanation. 11. **Stable-model plurality** — skeptical vs credulous results differ and are reported explicitly. 12. **No stable model** — returns profile/model inconsistency, not `false`. 13. **Copied-source swarm** — ten syndicated copies retain ten assertions but one evidence-origin component under explicit dependence links. 14. **False dependence suspicion** — suspected copying cannot be silently treated as proven dependence. 15. **Same publisher independent reports** — independence may be preserved when provenance demonstrates separate investigation. 16. **LLM summary echo** — multiple summaries of one underlying article cannot count as independent corroboration. 17. **Iterated revision order** — evidence sequence A,B,A under two revision operators produces reproducible operator-relative states; canonical ledger unchanged. 18. **Backdated correction** — current belief about past time changes; historical `known-at` query does not rewrite itself. 19. **World change vs correction** — actual CEO transition and later correction of old data produce distinct temporal/lifecycle structures. 20. **Conflicting priority dimensions** — source policy favors A while rule specificity favors B; no implicit numeric merge; named policy must determine result or return unresolved preference. 21. **Preference cycle** — `A>B, B>C, C>A` must be detected and handled by profile semantics, not sort accident. 22. **Undercut safety boundary** — semantic evidence saying verifier is unreliable must not disable runtime verifier/capability gate. 23. **Resource bound during preferred-extension search** — returns incomplete/resource-limited evaluation, never arbitrary skeptical warrant. 24. **Profile translation mismatch** — unsupported attack type/profile combination must fail profile admission explicitly rather than be dropped. Cross-profile differential oracle: ```text same ESG + same typed defeat/dependence graph + explicit profile/version + same query/context/times ↓ rebuild after cache deletion ↓ identical semantic warrant/receipt ``` Different profiles may legitimately disagree, but the disagreement must be attributable to the profile contract. --- ## Canonical changes required from B ### prolog-rlm #394 Add: - typed rebut/undermine/undercut/invalidate attack semantics; - typed partial preference relations with named composition policy; - source/evidence dependence input for corroboration-aware profiles; - circular-support/SCC handling and external-grounding invariant; - reinstatement/cycle semantics declared per profile; - bitemporal valid-time vs transaction-time query semantics; - split semantic acceptance from evaluation completeness; - explicit profile translation/admission contracts. ### symbolic-memory #6 Persist enough append-only evidence to reconstruct: - typed attacks/defeats and their provenance; - partial preference assertions/policies; - evidence-origin/source-dependence relations; - both valid-time and transaction-time lifecycle; - revision-state lineage when a promoted revision projection must be replayable; - circular-dependency metadata only where promoted; ordinary SCC caches remain derived. ### symbolic-memory #7 Query outcomes should expose: ```text semantic_acceptance evaluation_completeness support/counterevidence attack/defeat path preference basis + policy independence/dependence summary valid-time transaction-time profile/version/operator ``` Add `known_at(TransactionTime)` separately from `valid_at(WorldTime)`. --- ## Unresolved questions intentionally preserved for #400C/#400D 1. Which exact finite **default/defeasible profile(s)** should be first-class in v1: WFSX-like, defeasible logic, ASPIC+/ABA-derived, preferred ASP, or more than one? 2. Which preference-lifting principles satisfy the desired rationality postulates for our admitted strict/defeasible rule fragments? 3. How should source-dependence inference itself combine with trust/probability without circular truth-discovery feedback? 4. Should contradiction propagation be relation/profile-local or use a standard bilattice layer across selected profiles? 5. What is the exact bounded algorithm for query-local structured argument generation over shared ESG justifications? 6. What portions of iterated revision state should be durable versus recomputable from evidence + operator history? 7. How are epistemic profiles composed across imported theories/contexts without assuming one global non-monotonic semantics? **This is a major #400C question.** 8. Which indexes/materializations make bitemporal + attack/dependence queries fast enough at large memory scale? **#400D owns execution/scaling.** ## B conclusion The A architecture survives, but only after a significant refinement: > **Machine Spirit's canonical epistemic substrate should be ESG + a typed Defeat/Dependence Graph. Warrant remains profile-relative. Attacks on conclusions, premises, inference links, and evidence independence are not the same thing; priorities are typed/partial policy data; circular support cannot bootstrap itself; correction requires bitemporal history; and computational incompleteness is separate from epistemic status.** This does **not** freeze one universal default semantics. #400C must now research composition/interoperability among epistemic profiles/theories and #400D must prove bounded executable behavior.
nsaspy commented 2026-09-08 01:47:43 +00:00
Author
Owner
Copy link

Depth 3 / #400C — epistemic composition/interoperability: typed federation without one global truth semantics

This is subpass C only. #400 remains open for D. The purpose of C is not to pick a better single non-monotonic logic; it is to define how heterogeneous epistemic theories can exchange evidence and conclusions without silently inheriting each other's negation, default, priority, contradiction, revision, or acceptance semantics.

Research questions

  1. How can a WFS theory, stable-model/ASP theory, paraconsistent support theory, argumentation theory, and revision-projected theory interoperate without flattening to one global consequence relation?
  2. What exactly may cross a theory boundary: raw assertion/evidence, derived conclusion, skeptical warrant, credulous possibility, default, priority, absence, attack, dependence, or revision commitment?
  3. When is a cross-context bridge sound, merely useful, lossy, or explicitly non-composable?
  4. How are contradiction, source dependence, priorities and identity reconciliation contained across theory boundaries?
  5. Can federation remain query-bounded and locally explainable rather than requiring a global equilibrium over all memory?

Primary / authoritative sources inspected

  • Gerhard Brewka & Thomas Eiter, Equilibria in Heterogeneous Nonmonotonic Multi-Context Systems, AAAI 2007. https://aaai.org/Papers/AAAI/2007/AAAI07-060.pdf . This is the strongest direct precedent: an MCS contains contexts that may use arbitrary monotonic or non-monotonic logics, with nonmonotonic bridge rules controlling information flow and equilibria representing acceptable global belief states.
  • Gerhard Brewka, Thomas Eiter, Michael Fink, Antonius Weinzierl, Managed Multi-Context Systems, IJCAI 2011. DOI 10.5591/978-1-57735-516-8/IJCAI11-138; archival record https://repositum.tuwien.at/handle/20.500.12708/53812 . mMCS generalizes bridge effects from adding formulas to arbitrary managed knowledge-base operations such as revision/deletion. Architectural lesson: information flow and local management/revision semantics must be explicit operations, not hidden side effects.
  • Thomas Eiter, Michael Fink, Peter Schüller, Antonius Weinzierl, Finding Explanations of Inconsistency in Multi-Context Systems, KR 2010; Artificial Intelligence 216 (2014), 233–274. Primary preprint https://peterschueller.com/pub/2010/2010_finding_explanations_of_inconsistency_in_multi_context_systems.pdf . Inconsistency in heterogeneous MCSs can be explained in terms of bridge-rule sets whose presence/absence causes inconsistency; diagnosis is modular and nonmonotonic absence itself may be causal.
  • MCS-IE implementation/documentation, TU Wien. https://www.kr.tuwien.ac.at/systems/mcsie/documentation.html . Demonstrates context-local heterogeneous reasoners and system-level inconsistency explanation rather than requiring one implementation logic inside every context.
  • Alex Borgida & Luciano Serafini, Distributed Description Logics: Assimilating Information from Peer Sources, Journal on Data Semantics I, 2003. DOI 10.1007/978-3-540-39733-5_7; archival summary https://scholarship.libraries.rutgers.edu/esploro/outputs/bookChapter/Distributed-Description-Logics-Assimilating-Information-from/991031665889604646 . Particularly relevant to Machine Spirit identity/ontology reconciliation: peer sources can maintain independent domains and bridge mappings need not imply one-to-one global individual identity.
  • Gerhard Brewka et al., Reactive Multi-Context Systems: Heterogeneous Reasoning in Dynamic Environments, 2016. https://arxiv.org/abs/1609.03438 . Extends managed MCSs to streams/dynamic environments and explicitly studies inconsistency handling, nondeterminism, well-founded alternatives and complexity. Strong fit for append-only changing memory.
  • Contextualized Knowledge Repository / multi-relational contextual hierarchy work (Bozzato, Eiter, Kiesel, 2021). https://arxiv.org/abs/2108.03100 . Useful warning: defeasible inheritance/preferences over multiple contextual relations quickly become nontrivial; one generic inheritance order is inadequate.

The older MCS literature is unusually on-point here. It validates the architectural direction of heterogeneous local semantics plus explicit bridges, but it also exposes a trap: global equilibrium semantics is too strong to be Machine Spirit's default federation contract. A globally inconsistent/no-equilibrium subsystem should not automatically make unrelated memories unusable.

Candidate A — flatten all admitted knowledge into one global epistemic profile

Convert every theory into a common rule language/profile, normalize all priorities/defaults/negation, then reason globally.

Strengths

  • simplest query semantics;
  • one solver and one acceptance relation;
  • straightforward materialization.

Fatal problems

  • not P can mean WFS/NAF absence, ASP default negation, explicit refutation, or merely unsupported; flattening changes meaning;
  • stable-model credulous truth cannot become ordinary fact;
  • argumentation defeat and revision commitment are not raw support;
  • local priorities become globally comparable without justification;
  • one inconsistent imported theory can contaminate the whole world model;
  • impossible to preserve independent source/theory epistemic contracts honestly.

Rejected as canonical federation. It may be an explicitly selected export/compilation target only when a compatibility proof says the relevant fragment is semantics-preserving.

Candidate B — classic heterogeneous MCS with mandatory global equilibrium

Each theory is a context with its own logic; bridge rules exchange formulas; global acceptable states are MCS equilibria.

Strengths

  • mathematically clean heterogeneous composition;
  • explicit nonmonotonic bridge rules;
  • direct support for contexts using different logics;
  • mature inconsistency/diagnosis literature.

Problems for Machine Spirit

  • a global equilibrium/no-equilibrium status couples every participating context too strongly;
  • large dynamic memory makes whole-federation equilibrium computation a poor default query path;
  • bridge rules conventionally communicate formulas/beliefs, but Machine Spirit needs richer provenance-bearing acceptance objects;
  • global equilibrium can obscure the distinction between local evidence state and exported local warrant;
  • a news subtheory with no stable model should not disable deterministic project/manual knowledge.

Retain as an optional federation profile, especially for bounded tightly-coupled subtheories whose semantics genuinely requires fixed-point/equilibrium reasoning. Do not make it the memory-wide default.

Candidate C — Typed Epistemic Federation Contracts + query-bounded federation (preferred)

Each theory remains semantically sovereign. It exports epistemic objects, not naked propositions. Bridges have typed import/export contracts describing exactly what local status is being transmitted and what the destination is allowed to do with it.

Theory A / local profile                Theory B / local profile
WFS / ASP / argument / ...              paraconsistent / revision / ...
          │                                        │
          └── epistemic export envelope ───────────┘
                     ↓
          TYPED EPISTEMIC BRIDGE
     mapping + force + admission + loss
     dependence + validity + provenance
                     ↓
           recipient-local admission
                     ↓
            local reasoning continues

Conceptual records:

ep_export(ExportId,
          TheoryRef,
          PropositionRef,
          local_profile(ProfileRef),
          local_support_state(SupportState),
          local_acceptance(Acceptance),
          model_scope(ModelScope),          % all | some | unique | n_of_m | n/a
          AssumptionRefs,
          SupportRefs,
          CounterRefs,
          Validity,
          DependenceRefs,
          ReceiptRef).

ep_bridge(BridgeId,
          FromTheory,
          ToTheory,
          PropositionMapping,
          export_requirement(ExportRequirement),
          import_mode(ImportMode),
          negation_contract(NegationContract),
          priority_contract(PriorityContract),
          identity_contract(IdentityContract),
          dependence_policy(DependencePolicy),
          Status,
          Provenance).

A bridge is not mere P@A -> P@B. It says what A knows/warrants, under which semantics, and how B may treat that information.

Recommended import modes:

evidence_only
    create imported support/refutation evidence in B; B decides warrant locally

skeptical_warrant_as_support
    only conclusions warranted under every admitted local model/environment cross;
    still imported as provenance-bearing support, not source-explicit fact

credulous_candidate
    import as alternative/hypothesis/assumption only; never ordinary support by default

attributed_acceptance
    preserve `A warrants P under profile X` as meta-knowledge without asserting P in B

revision_input
    feed explicitly into a named revision operator/state in B; never mutate canonical history

argument_import
    import an argument/attack/undercut object with its local semantics, not just its conclusion

inert_reference
    cross-link/queryable but not admissible as premise

Critical default

evidence_only or attributed_acceptance is the safe cross-profile default. Stronger imports require explicit compatibility/admission contracts.

Candidate D — argumentation as the universal federation layer

Translate every local accepted conclusion into an argument, then federate through attacks/defeats.

Strengths

  • natural provenance/explanation;
  • can retain contested conclusions from different local reasoners;
  • local rule engines can become argument producers.

Problem

It still imposes argumentation acceptance as the global semantics and can lose important local statuses such as WFS undefined, ASP model multiplicity, revision state lineage, or support-only paraconsistent evidence. Argumentation remains an excellent derived federation profile, not the universal bus.

Preferred design: Epistemic Federation Fabric (EFF)

The surviving architecture is ESG + Typed Defeat/Dependence Graph locally, connected by an Epistemic Federation Fabric.

                     ┌─ theory A / WFS
canonical ledger ────┼─ theory B / ASP
                     ├─ theory C / support-paraconsistent
                     ├─ theory D / argumentation
                     └─ theory E / revision projection
                              │
                    local epistemic outcomes
                              │
                     EPISTEMIC EXPORTS
                              │
                typed/versioned bridge contracts
                              │
             ┌────────────────┴─────────────────┐
             │                                  │
     bounded recipient theory            federation query view
   admits imported evidence locally     aggregates without flattening
             │                                  │
             └────────────────┬─────────────────┘
                              ↓
                    provenance-rich result

Hard interoperability invariants

1. Default negation / absence does not cross an open boundary by default

If A's WFS/ASP logic derives not p because p is absent locally, that cannot become explicit negative support in B.

A: not p (local default/NAF result)
       !=
B: explicit support for ¬p

A bridge may transmit A lacks/would-default-negate p under profile X as meta-knowledge. It may only use absence as a premise in B under an explicit closure contract identifying the closed predicate/domain/time/context and compatible negation semantics.

This is the single most important cross-profile safety rule.

2. Local skeptical/credulous status survives export

ASP example:

models(A) = [M1: P, M2: ¬P]

Export must preserve:

P credulous_only
¬P credulous_only
neither skeptically_warranted

A recipient cannot treat either as ordinary warranted support unless a bridge explicitly imports credulous alternatives as assumptions/hypotheses.

3. undefined, conflicted, no_model, resource_limited, unsupported are non-isomorphic

Do not map them all to unknown when crossing a theory boundary. The export envelope preserves semantic acceptance and evaluation completeness separately.

4. Priorities are namespaced

priority(rule7, high) in A has no ordering relation with B's priority(rule9, high) unless a bridge supplies a typed lifting policy.

Valid forms include:

preserve_local_only
explicit_pairwise_mapping
source-policy lifting
specificity lattice mapping
not_comparable

Never compare arbitrary numeric weights merely because both sides have numbers.

5. Defaults do not inherit globally

Imported default rule D from A is not automatically active in B. Bridge mode must distinguish:

import_default_as_data
import_default_as_candidate
activate_under_profile(Profile, Namespace)

Activation requires B's profile to understand the default's semantics or a declared semantics-changing translation with a loss receipt.

6. Defeat edges preserve type and target

Cross-context rebut/undermine/undercut/invalidate remains typed. An imported undercutter does not turn into ¬P merely because B lacks an equivalent undercut primitive. If B cannot represent the attack semantics, mark it represented_only/noncomposable or route through an argumentation federation view.

7. Source dependence propagates across contexts

If theory A and theory B both ultimately depend on the same Reuters article, federation must preserve that lineage. Crossing a context boundary does not reset independence.

Conceptually:

A:P <- summary_1 <- Reuters R
B:P <- summary_2 <- Reuters R

raw exports = 2
independent evidence components = 1

Bridge receipts therefore carry dependence/source-origin IDs, not only local assertion IDs.

8. Identity/ontology reconciliation is epistemic input, not invisible preprocessing

Suppose A refers to x, B to y, and reconciliation proposes same_entity(x,y).

Merging proposition identity may suddenly make A:P and B:¬P conflict. Therefore identity mappings carry status/provenance and can be conditional assumptions in the federation environment.

ep_identity_bridge(MapId,
                   ARef,
                   BRef,
                   relation(same_as | maybe_same | broader | ...),
                   Status,
                   Evidence,
                   Provenance).

A disputed identity mapping cannot silently rewrite support graphs. Query results must be able to say the conflict exists only under identity assumption I.

Distributed Description Logic work strongly supports preserving peer-local domains and explicit mappings rather than assuming globally identical individuals.

9. Contradiction containment is the default

Conflict in theory A remains local unless:

  • its evidence is explicitly imported;
  • a bridge exports a conflicting accepted conclusion;
  • or a federation query intentionally joins those theories.

no_equilibrium(A) cannot poison unrelated B. A global equilibrium is an optional federation profile, not ambient memory semantics.

10. Federation itself has a profile/version

A federation query must declare how local outcomes are combined.

Candidate modes:

federated_evidence
    union admitted support/counterevidence, preserve local statuses, compute recipient support view

federated_skeptical
    consume only locally skeptical/uniquely warranted exports according to bridge policy

federated_credulous
    retain alternatives/environments; no top-1 collapse

federated_argumentation
    derive cross-context arguments/attacks and run named argument semantics

mcs_equilibrium
    bounded classic heterogeneous MCS-style fixed point over selected contexts/bridges

managed_revision
    execute explicit management/revision operations under a versioned management policy

The query result must expose the federation profile and selected theory/bridge closure.

Bridge compatibility contract

Before an epistemic bridge can be active, validation should classify it approximately as:

exact_preserving
sound_but_incomplete
lossy_declared
status_only
noncomposable
unknown_compatibility

Relevant dimensions:

positive assertion semantics
explicit negation
negation-as-failure / closure assumptions
default semantics
model plurality
undefinedness
attack/defeat semantics
priority ordering
identity assumptions
time/context assumptions
revision semantics
provenance/dependence preservation

noncomposable is a legitimate result. Machine Spirit should be able to remember/query both theories without pretending their reasoning can be merged.

Federation query contract

Conceptual API:

epistemic_federated_query(+Query,
                           +TheoryRefs,
                           +BridgePolicy,
                           +FederationProfile,
                           +Context,
                           +Options,
                           -Outcome).

Outcome should expose at least:

bindings/conclusion
federation_profile + version
participating theories + local profile versions
bridge closure + bridge versions
local outcome vector
imported support/counterevidence
skeptical/credulous/model status retained
identity/mapping assumptions
source dependence components
cross-context attacks/defeats
noncomposable edges
semantic acceptance
evaluation completeness
provenance/explanation receipt

A useful internal intermediate is:

ep_local_outcome(Theory, Query, Profile, Acceptance, Completeness, Receipt).
ep_import_receipt(Bridge, Export, ImportedAs, Loss, Dependence, Receipt).

This creates an auditable path from each local semantics through every cross-context transformation.

Complexity / scaling implications

Classic heterogeneous MCS equilibrium reasoning can inherit the complexity of local logics plus cross-context fixed-point/model search; nonmonotonic bridges introduce additional global search. The inconsistency-diagnosis literature exists precisely because bridge interactions can make whole systems inconsistent in non-obvious ways.

Machine Spirit should therefore not globally materialize all federated equilibria.

Preferred operational strategy:

  1. start from a query and selected context;
  2. traverse only relevant theory exports/bridges;
  3. evaluate local theories under their native profile;
  4. cache local outcome receipts keyed by theory/profile/evidence frontier;
  5. import only demanded exports;
  6. detect bridge SCCs;
  7. use fixed-point/equilibrium evaluation only inside the affected SCC where the selected federation profile requires it;
  8. preserve bounded plurality instead of enumerating unbounded model products;
  9. surface resource_limited separately from semantic undecidedness.

If independent context A has m admissible models and B has n, naïvely constructing a Cartesian product can yield m*n combinations before bridge constraints. More contexts create exponential products. Federation should therefore preserve factored/local model sets and expand combinations only when bridge dependencies make them relevant.

Acyclic positive evidence-only bridges can be evaluated much more cheaply as a topological propagation plan. Negation/default/managed revision across a bridge SCC requires the stronger federation solver/profile.

Epistemic/provenance implications

C adds a new provenance class:

federation provenance

This is distinct from source/compiler/logical/lifecycle/profile provenance and records:

  • local theory/profile outcome;
  • export envelope;
  • bridge/mapping version;
  • semantics/loss classification;
  • recipient admission mode;
  • identity assumptions;
  • dependence propagation;
  • federation profile;
  • final query receipt.

A conclusion may be fully warranted locally but only status_only across a bridge. That is not lower confidence in P; it is a limitation of semantic interoperability.

Likewise, importing a skeptical conclusion as evidence creates a new derived support path whose provenance includes the local warrant receipt. It never turns the upstream source into a direct source of the recipient proposition.

Safety / authority implications

Epistemic federation is not capability federation.

Hard rule:

A warrants should_restart(service)
        !=
B grants restart capability

No bridge may transfer host authority, tool permissions, credentials, principal identity, or effect capability merely because the imported semantic content names an action/policy/permission.

Security principal identity mappings use a stricter authority-owned mechanism than ordinary semantic same_as mappings. A metonymic/ontology/entity reconciliation bridge can never merge principals or capability identities.

Host execution remains behind the existing typed authority/effect boundary.

Adversarial review / failure cases

  1. NAF laundering: A derives not p from local absence; bridge turns it into B's explicit ¬p. Forbidden without explicit closure + negation translation contract.
  2. Credulous laundering: P occurs in one ASP model; recipient stores P as warranted. Forbidden; preserve credulous/model scope.
  3. Priority collision: two contexts both say priority 10; importer compares them globally. Forbidden absent lifting contract.
  4. Default contamination: local medical default imported into legal/policy theory as active universal default. Default stays namespaced/inert unless admitted.
  5. Equilibrium poisoning: one ASP context has no stable model; entire memory query fails. Default federation contains failure locally.
  6. Echo corroboration: two contexts independently summarize the same source and appear as independent support. Dependence lineage must survive bridge.
  7. Identity-induced contradiction: two previously separate entities are reconciled; conflicting propositions suddenly join. Conflict receipt cites identity assumption/mapping.
  8. Ontology mapping overclaim: A:broader-than B translated as equivalence, creating spurious defeaters. Mapping relation/loss must be explicit.
  9. Undefined collapse: WFS undefined imported as false or unsupported. Preserve local undefined status.
  10. No-model collapse: ASP no stable model imported as refutation of every queried proposition. Profile failure, not proposition falsity.
  11. Resource-status laundering: local solver timeout imported as epistemic unknown. Completeness remains separate.
  12. Undercut flattening: A undercuts justification J; B only supports positive/negative propositions and turns attack into ¬conclusion. Reject/noncomposable or retain attack object.
  13. Revision rewrite: managed bridge invokes revision and old evidence disappears. Canonical ledger unchanged; revision output is projection/state lineage.
  14. Authority injection: imported policy says operator may delete X; bridge treats it as host permission. Never.
  15. Bridge cycle bootstrap: A imports P from B, B imports P from A, no external support. Cross-context support SCC cannot ground itself unless federation profile explicitly licenses such a fixed point and receipt exposes it.
  16. Cross-context closed-world leak: B treats missing exports from A as evidence of negation. Absence is meaningless unless bridge declares completeness/closure.
  17. Backdated identity map: later entity reconciliation retroactively changes what was known historically. known_at queries use mapping state available at transaction time.
  18. Lossy translation hidden: stable-model plurality translated to a single WFS answer with no receipt. Bridge classified lossy/noncomposable; cannot masquerade as exact.

Falsifiable / conformance fixtures

C requires at least these executable fixtures later:

  1. WFS not p crossing an open bridge does not create explicit ¬p support.
  2. Closure-qualified bridge may intentionally translate a closed predicate's absence and receipt names the closure contract.
  3. ASP two-model {p} / {¬p} export remains credulous on both sides; no skeptical P.
  4. Skeptical ASP conclusion imported under skeptical_warrant_as_support creates a derived support path with local warrant receipt.
  5. WFS undefined survives round-trip through a federation query.
  6. no_stable_model stays a local profile failure and does not refute unrelated propositions.
  7. Argument undercut crosses only when recipient bridge supports typed attack; otherwise reports noncomposable.
  8. Local priorities with same numeric values remain incomparable absent lifting policy.
  9. Two summaries of one original article produce two assertions but one independent evidence component after federation.
  10. Cross-theory identity assumption induces a conflict only in environments containing that identity mapping.
  11. Retracting/weakening the identity mapping removes that federated conflict without deleting original supports.
  12. A failing/inconsistent context does not block unrelated evidence-only query over another context.
  13. Explicit MCS-equilibrium profile over a bounded cyclic pair reports zero/one/multiple equilibria distinctly.
  14. Positive acyclic evidence-only bridges reach a deterministic topological fixed point.
  15. Pure bridge cycle with no external support cannot bootstrap ordinary support under baseline federation.
  16. Imported default remains inactive unless recipient profile + bridge explicitly admits it.
  17. Source dependence survives theory export/import and prevents false corroboration count.
  18. resource_limited local evaluation remains computational status, not epistemic unknown.
  19. Bitemporal known_at(T) federation uses bridge/identity/profile versions known at T.
  20. Host authority is unchanged by any semantic/epistemic import.
  21. Same ledger + same local profile versions + same bridge versions + same federation profile produces replay-equivalent outcome after cache rebuild.
  22. Lossy/noncomposable bridge emits explicit diagnostic and never silently drops plurality/undefinedness/attack semantics.

Rejected alternatives

  • Universal global WFS: deterministic and convenient but cannot preserve ASP plurality, argumentation acceptance or revision semantics.
  • Universal ASP: expressive but forces all local semantics into stable-model meaning and makes ordinary evidence/support federation unnecessarily model-heavy.
  • Trust-weighted global voting: destroys logical force, copied-source structure, defaults and attacks; multiple assertions are not IID votes.
  • Always-global MCS equilibrium: mathematically valid for selected systems but too brittle/expensive as ambient memory semantics.
  • Argumentation-only bus: excellent derived view, but not faithful to every local outcome type.
  • Bridge by proposition ID only: loses local acceptance/model/profile/provenance and is epistemically unsafe.

Concrete canonical changes recommended

prolog-rlm #392

Keep the existing typed sem_bridge, but its semantic-profile work should allow a bridge to reference an epistemic interoperability contract rather than implying that proposition mapping alone transfers warrant. Semantic proposition mapping and epistemic admission are separate layers.

prolog-rlm #394

Add an Epistemic Federation Fabric contract:

  • local theories retain local epistemic profiles;
  • export local outcome envelopes with support/acceptance/completeness/model scope;
  • typed bridge import modes;
  • NAF/absence cannot cross without explicit closure contract;
  • local priorities/defaults stay namespaced;
  • source dependence propagates;
  • identity mappings become explicit assumptions affecting warrant;
  • federation profile/version required for cross-theory warrant;
  • noncomposable/lossy_declared are valid bridge outcomes;
  • global MCS equilibrium is optional/bounded, not default.

symbolic-memory #6

Persist enough to replay federation:

  • bridge contract/version and status;
  • durable export/import receipts when a federated conclusion is promoted;
  • source dependence lineage across contexts;
  • identity/ontology mapping assumptions and lifecycle;
  • federation profile/version on promoted cross-theory warrant;
  • bitemporal bridge/mapping state.

Do not persist one merged global truth graph.

symbolic-memory #7

Cross-memory query joins need explicit:

TheoryRefs
BridgePolicy
FederationProfile
Context/valid_at/known_at

and must return local outcome vector + bridge/import receipts + noncomposable edges + mapping assumptions + dependence components. all memories is never implicit permission to flatten epistemic semantics.

#397 / #400

Mark #400C complete, keep #400 open, and queue #400D for computational realization/scaling/conformance of ESG + defeat/dependence + federation: query planning, local-result caches, bridge SCC evaluation, incremental invalidation, bounded model/environment products, diagnostics and deterministic differential replay.

Unresolved questions preserved for D/later depths

  • exact minimal bridge type algebra and schema;
  • formal compatibility checks between common profile pairs (WFS↔ASP, WFS↔argumentation, ASP↔argumentation, revision↔support);
  • when skeptical export is sound under incomplete/changed source contexts;
  • incremental maintenance of bridge SCC equilibria;
  • factorized representation of model products across contexts;
  • how much source-dependence inference is trusted vs merely hypothesized;
  • ontology/identity mapping confidence without turning confidence into truth;
  • federated explanation compression for large dependency graphs;
  • privacy/partial-knowledge contexts and information-hiding boundaries;
  • distributed/federated execution across multiple stores/processes (Depth 5/6 may refine);
  • whether a practical Machine Spirit v1 needs full MCS equilibrium at all, versus typed evidence federation + selected local solvers.

C decision

Adopt the Epistemic Federation Fabric: local epistemic sovereignty + typed status-bearing exports + explicit admission bridges + query-bounded federation. Classic heterogeneous MCS equilibrium remains an optional strong federation profile, not global ambient semantics.

This materially extends #400A/B rather than replacing them: ESG + typed defeat/dependence remains the local/canonical epistemic substrate; C defines how those local epistemic worlds communicate without lying about their semantics.

Next: #400D.

## Depth 3 / #400C — epistemic composition/interoperability: typed federation without one global truth semantics This is **subpass C only**. #400 remains open for D. The purpose of C is not to pick a better single non-monotonic logic; it is to define how heterogeneous epistemic theories can exchange evidence and conclusions **without silently inheriting each other's negation, default, priority, contradiction, revision, or acceptance semantics**. ### Research questions 1. How can a WFS theory, stable-model/ASP theory, paraconsistent support theory, argumentation theory, and revision-projected theory interoperate without flattening to one global consequence relation? 2. What exactly may cross a theory boundary: raw assertion/evidence, derived conclusion, skeptical warrant, credulous possibility, default, priority, absence, attack, dependence, or revision commitment? 3. When is a cross-context bridge sound, merely useful, lossy, or explicitly non-composable? 4. How are contradiction, source dependence, priorities and identity reconciliation contained across theory boundaries? 5. Can federation remain query-bounded and locally explainable rather than requiring a global equilibrium over all memory? ## Primary / authoritative sources inspected - **Gerhard Brewka & Thomas Eiter, _Equilibria in Heterogeneous Nonmonotonic Multi-Context Systems_, AAAI 2007.** https://aaai.org/Papers/AAAI/2007/AAAI07-060.pdf . This is the strongest direct precedent: an MCS contains contexts that may use arbitrary monotonic or non-monotonic logics, with nonmonotonic bridge rules controlling information flow and equilibria representing acceptable global belief states. - **Gerhard Brewka, Thomas Eiter, Michael Fink, Antonius Weinzierl, _Managed Multi-Context Systems_, IJCAI 2011.** DOI 10.5591/978-1-57735-516-8/IJCAI11-138; archival record https://repositum.tuwien.at/handle/20.500.12708/53812 . mMCS generalizes bridge effects from adding formulas to arbitrary managed knowledge-base operations such as revision/deletion. Architectural lesson: information flow and local management/revision semantics must be explicit operations, not hidden side effects. - **Thomas Eiter, Michael Fink, Peter Schüller, Antonius Weinzierl, _Finding Explanations of Inconsistency in Multi-Context Systems_, KR 2010; Artificial Intelligence 216 (2014), 233–274.** Primary preprint https://peterschueller.com/pub/2010/2010_finding_explanations_of_inconsistency_in_multi_context_systems.pdf . Inconsistency in heterogeneous MCSs can be explained in terms of bridge-rule sets whose presence/absence causes inconsistency; diagnosis is modular and nonmonotonic absence itself may be causal. - **MCS-IE implementation/documentation, TU Wien.** https://www.kr.tuwien.ac.at/systems/mcsie/documentation.html . Demonstrates context-local heterogeneous reasoners and system-level inconsistency explanation rather than requiring one implementation logic inside every context. - **Alex Borgida & Luciano Serafini, _Distributed Description Logics: Assimilating Information from Peer Sources_, Journal on Data Semantics I, 2003.** DOI 10.1007/978-3-540-39733-5_7; archival summary https://scholarship.libraries.rutgers.edu/esploro/outputs/bookChapter/Distributed-Description-Logics-Assimilating-Information-from/991031665889604646 . Particularly relevant to Machine Spirit identity/ontology reconciliation: peer sources can maintain independent domains and bridge mappings need not imply one-to-one global individual identity. - **Gerhard Brewka et al., _Reactive Multi-Context Systems: Heterogeneous Reasoning in Dynamic Environments_, 2016.** https://arxiv.org/abs/1609.03438 . Extends managed MCSs to streams/dynamic environments and explicitly studies inconsistency handling, nondeterminism, well-founded alternatives and complexity. Strong fit for append-only changing memory. - **Contextualized Knowledge Repository / multi-relational contextual hierarchy work (Bozzato, Eiter, Kiesel, 2021).** https://arxiv.org/abs/2108.03100 . Useful warning: defeasible inheritance/preferences over multiple contextual relations quickly become nontrivial; one generic inheritance order is inadequate. The older MCS literature is unusually on-point here. It validates the architectural direction of heterogeneous local semantics plus explicit bridges, but it also exposes a trap: **global equilibrium semantics is too strong to be Machine Spirit's default federation contract**. A globally inconsistent/no-equilibrium subsystem should not automatically make unrelated memories unusable. --- # Candidate A — flatten all admitted knowledge into one global epistemic profile Convert every theory into a common rule language/profile, normalize all priorities/defaults/negation, then reason globally. ### Strengths - simplest query semantics; - one solver and one acceptance relation; - straightforward materialization. ### Fatal problems - `not P` can mean WFS/NAF absence, ASP default negation, explicit refutation, or merely unsupported; flattening changes meaning; - stable-model credulous truth cannot become ordinary fact; - argumentation defeat and revision commitment are not raw support; - local priorities become globally comparable without justification; - one inconsistent imported theory can contaminate the whole world model; - impossible to preserve independent source/theory epistemic contracts honestly. **Rejected as canonical federation.** It may be an explicitly selected export/compilation target only when a compatibility proof says the relevant fragment is semantics-preserving. --- # Candidate B — classic heterogeneous MCS with mandatory global equilibrium Each theory is a context with its own logic; bridge rules exchange formulas; global acceptable states are MCS equilibria. ### Strengths - mathematically clean heterogeneous composition; - explicit nonmonotonic bridge rules; - direct support for contexts using different logics; - mature inconsistency/diagnosis literature. ### Problems for Machine Spirit - a global equilibrium/no-equilibrium status couples every participating context too strongly; - large dynamic memory makes whole-federation equilibrium computation a poor default query path; - bridge rules conventionally communicate formulas/beliefs, but Machine Spirit needs richer provenance-bearing acceptance objects; - global equilibrium can obscure the distinction between local evidence state and exported local warrant; - a news subtheory with no stable model should not disable deterministic project/manual knowledge. **Retain as an optional federation profile**, especially for bounded tightly-coupled subtheories whose semantics genuinely requires fixed-point/equilibrium reasoning. Do not make it the memory-wide default. --- # Candidate C — Typed Epistemic Federation Contracts + query-bounded federation **(preferred)** Each theory remains semantically sovereign. It exports **epistemic objects**, not naked propositions. Bridges have typed import/export contracts describing exactly what local status is being transmitted and what the destination is allowed to do with it. ```text Theory A / local profile Theory B / local profile WFS / ASP / argument / ... paraconsistent / revision / ... │ │ └── epistemic export envelope ───────────┘ ↓ TYPED EPISTEMIC BRIDGE mapping + force + admission + loss dependence + validity + provenance ↓ recipient-local admission ↓ local reasoning continues ``` Conceptual records: ```prolog ep_export(ExportId, TheoryRef, PropositionRef, local_profile(ProfileRef), local_support_state(SupportState), local_acceptance(Acceptance), model_scope(ModelScope), % all | some | unique | n_of_m | n/a AssumptionRefs, SupportRefs, CounterRefs, Validity, DependenceRefs, ReceiptRef). ep_bridge(BridgeId, FromTheory, ToTheory, PropositionMapping, export_requirement(ExportRequirement), import_mode(ImportMode), negation_contract(NegationContract), priority_contract(PriorityContract), identity_contract(IdentityContract), dependence_policy(DependencePolicy), Status, Provenance). ``` A bridge is **not** mere `P@A -> P@B`. It says what A knows/warrants, under which semantics, and how B may treat that information. Recommended import modes: ```text evidence_only create imported support/refutation evidence in B; B decides warrant locally skeptical_warrant_as_support only conclusions warranted under every admitted local model/environment cross; still imported as provenance-bearing support, not source-explicit fact credulous_candidate import as alternative/hypothesis/assumption only; never ordinary support by default attributed_acceptance preserve `A warrants P under profile X` as meta-knowledge without asserting P in B revision_input feed explicitly into a named revision operator/state in B; never mutate canonical history argument_import import an argument/attack/undercut object with its local semantics, not just its conclusion inert_reference cross-link/queryable but not admissible as premise ``` ### Critical default **`evidence_only` or `attributed_acceptance` is the safe cross-profile default.** Stronger imports require explicit compatibility/admission contracts. --- # Candidate D — argumentation as the universal federation layer Translate every local accepted conclusion into an argument, then federate through attacks/defeats. ### Strengths - natural provenance/explanation; - can retain contested conclusions from different local reasoners; - local rule engines can become argument producers. ### Problem It still imposes argumentation acceptance as the global semantics and can lose important local statuses such as WFS `undefined`, ASP model multiplicity, revision state lineage, or support-only paraconsistent evidence. Argumentation remains an excellent **derived federation profile**, not the universal bus. --- # Preferred design: Epistemic Federation Fabric (EFF) The surviving architecture is **ESG + Typed Defeat/Dependence Graph locally, connected by an Epistemic Federation Fabric**. ```text ┌─ theory A / WFS canonical ledger ────┼─ theory B / ASP ├─ theory C / support-paraconsistent ├─ theory D / argumentation └─ theory E / revision projection │ local epistemic outcomes │ EPISTEMIC EXPORTS │ typed/versioned bridge contracts │ ┌────────────────┴─────────────────┐ │ │ bounded recipient theory federation query view admits imported evidence locally aggregates without flattening │ │ └────────────────┬─────────────────┘ ↓ provenance-rich result ``` ## Hard interoperability invariants ### 1. Default negation / absence does not cross an open boundary by default If A's WFS/ASP logic derives `not p` because `p` is absent locally, that cannot become explicit negative support in B. ```text A: not p (local default/NAF result) != B: explicit support for ¬p ``` A bridge may transmit `A lacks/would-default-negate p under profile X` as meta-knowledge. It may only use absence as a premise in B under an explicit **closure contract** identifying the closed predicate/domain/time/context and compatible negation semantics. This is the single most important cross-profile safety rule. ### 2. Local skeptical/credulous status survives export ASP example: ```text models(A) = [M1: P, M2: ¬P] ``` Export must preserve: ```text P credulous_only ¬P credulous_only neither skeptically_warranted ``` A recipient cannot treat either as ordinary warranted support unless a bridge explicitly imports credulous alternatives as assumptions/hypotheses. ### 3. `undefined`, `conflicted`, `no_model`, `resource_limited`, `unsupported` are non-isomorphic Do not map them all to `unknown` when crossing a theory boundary. The export envelope preserves semantic acceptance and evaluation completeness separately. ### 4. Priorities are namespaced `priority(rule7, high)` in A has no ordering relation with B's `priority(rule9, high)` unless a bridge supplies a typed lifting policy. Valid forms include: ```text preserve_local_only explicit_pairwise_mapping source-policy lifting specificity lattice mapping not_comparable ``` Never compare arbitrary numeric weights merely because both sides have numbers. ### 5. Defaults do not inherit globally Imported default rule D from A is not automatically active in B. Bridge mode must distinguish: ```text import_default_as_data import_default_as_candidate activate_under_profile(Profile, Namespace) ``` Activation requires B's profile to understand the default's semantics or a declared semantics-changing translation with a loss receipt. ### 6. Defeat edges preserve type and target Cross-context rebut/undermine/undercut/invalidate remains typed. An imported undercutter does not turn into ¬P merely because B lacks an equivalent undercut primitive. If B cannot represent the attack semantics, mark it `represented_only`/`noncomposable` or route through an argumentation federation view. ### 7. Source dependence propagates across contexts If theory A and theory B both ultimately depend on the same Reuters article, federation must preserve that lineage. Crossing a context boundary does not reset independence. Conceptually: ```text A:P <- summary_1 <- Reuters R B:P <- summary_2 <- Reuters R raw exports = 2 independent evidence components = 1 ``` Bridge receipts therefore carry dependence/source-origin IDs, not only local assertion IDs. ### 8. Identity/ontology reconciliation is epistemic input, not invisible preprocessing Suppose A refers to `x`, B to `y`, and reconciliation proposes `same_entity(x,y)`. Merging proposition identity may suddenly make A:P and B:¬P conflict. Therefore identity mappings carry status/provenance and can be conditional assumptions in the federation environment. ```prolog ep_identity_bridge(MapId, ARef, BRef, relation(same_as | maybe_same | broader | ...), Status, Evidence, Provenance). ``` A disputed identity mapping cannot silently rewrite support graphs. Query results must be able to say **the conflict exists only under identity assumption I**. Distributed Description Logic work strongly supports preserving peer-local domains and explicit mappings rather than assuming globally identical individuals. ### 9. Contradiction containment is the default Conflict in theory A remains local unless: - its evidence is explicitly imported; - a bridge exports a conflicting accepted conclusion; - or a federation query intentionally joins those theories. `no_equilibrium(A)` cannot poison unrelated B. A global equilibrium is an optional federation profile, not ambient memory semantics. ### 10. Federation itself has a profile/version A federation query must declare how local outcomes are combined. Candidate modes: ```text federated_evidence union admitted support/counterevidence, preserve local statuses, compute recipient support view federated_skeptical consume only locally skeptical/uniquely warranted exports according to bridge policy federated_credulous retain alternatives/environments; no top-1 collapse federated_argumentation derive cross-context arguments/attacks and run named argument semantics mcs_equilibrium bounded classic heterogeneous MCS-style fixed point over selected contexts/bridges managed_revision execute explicit management/revision operations under a versioned management policy ``` The query result must expose the federation profile and selected theory/bridge closure. --- # Bridge compatibility contract Before an epistemic bridge can be active, validation should classify it approximately as: ```text exact_preserving sound_but_incomplete lossy_declared status_only noncomposable unknown_compatibility ``` Relevant dimensions: ```text positive assertion semantics explicit negation negation-as-failure / closure assumptions default semantics model plurality undefinedness attack/defeat semantics priority ordering identity assumptions time/context assumptions revision semantics provenance/dependence preservation ``` `noncomposable` is a legitimate result. Machine Spirit should be able to remember/query both theories without pretending their reasoning can be merged. --- # Federation query contract Conceptual API: ```prolog epistemic_federated_query(+Query, +TheoryRefs, +BridgePolicy, +FederationProfile, +Context, +Options, -Outcome). ``` Outcome should expose at least: ```text bindings/conclusion federation_profile + version participating theories + local profile versions bridge closure + bridge versions local outcome vector imported support/counterevidence skeptical/credulous/model status retained identity/mapping assumptions source dependence components cross-context attacks/defeats noncomposable edges semantic acceptance evaluation completeness provenance/explanation receipt ``` A useful internal intermediate is: ```prolog ep_local_outcome(Theory, Query, Profile, Acceptance, Completeness, Receipt). ep_import_receipt(Bridge, Export, ImportedAs, Loss, Dependence, Receipt). ``` This creates an auditable path from each local semantics through every cross-context transformation. --- # Complexity / scaling implications Classic heterogeneous MCS equilibrium reasoning can inherit the complexity of local logics plus cross-context fixed-point/model search; nonmonotonic bridges introduce additional global search. The inconsistency-diagnosis literature exists precisely because bridge interactions can make whole systems inconsistent in non-obvious ways. Machine Spirit should therefore **not globally materialize all federated equilibria**. Preferred operational strategy: 1. start from a query and selected context; 2. traverse only relevant theory exports/bridges; 3. evaluate local theories under their native profile; 4. cache local outcome receipts keyed by theory/profile/evidence frontier; 5. import only demanded exports; 6. detect bridge SCCs; 7. use fixed-point/equilibrium evaluation only inside the affected SCC where the selected federation profile requires it; 8. preserve bounded plurality instead of enumerating unbounded model products; 9. surface `resource_limited` separately from semantic undecidedness. If independent context A has `m` admissible models and B has `n`, naïvely constructing a Cartesian product can yield `m*n` combinations before bridge constraints. More contexts create exponential products. Federation should therefore preserve factored/local model sets and expand combinations only when bridge dependencies make them relevant. Acyclic positive evidence-only bridges can be evaluated much more cheaply as a topological propagation plan. Negation/default/managed revision across a bridge SCC requires the stronger federation solver/profile. --- # Epistemic/provenance implications C adds a new provenance class: ```text federation provenance ``` This is distinct from source/compiler/logical/lifecycle/profile provenance and records: - local theory/profile outcome; - export envelope; - bridge/mapping version; - semantics/loss classification; - recipient admission mode; - identity assumptions; - dependence propagation; - federation profile; - final query receipt. A conclusion may be fully warranted locally but only `status_only` across a bridge. That is not lower confidence in P; it is a limitation of semantic interoperability. Likewise, importing a skeptical conclusion as evidence creates a **new derived support path** whose provenance includes the local warrant receipt. It never turns the upstream source into a direct source of the recipient proposition. --- # Safety / authority implications Epistemic federation is not capability federation. Hard rule: ```text A warrants should_restart(service) != B grants restart capability ``` No bridge may transfer host authority, tool permissions, credentials, principal identity, or effect capability merely because the imported semantic content names an action/policy/permission. Security principal identity mappings use a stricter authority-owned mechanism than ordinary semantic `same_as` mappings. A metonymic/ontology/entity reconciliation bridge can never merge principals or capability identities. Host execution remains behind the existing typed authority/effect boundary. --- # Adversarial review / failure cases 1. **NAF laundering:** A derives `not p` from local absence; bridge turns it into B's explicit `¬p`. **Forbidden without explicit closure + negation translation contract.** 2. **Credulous laundering:** P occurs in one ASP model; recipient stores P as warranted. **Forbidden; preserve credulous/model scope.** 3. **Priority collision:** two contexts both say priority `10`; importer compares them globally. **Forbidden absent lifting contract.** 4. **Default contamination:** local medical default imported into legal/policy theory as active universal default. **Default stays namespaced/inert unless admitted.** 5. **Equilibrium poisoning:** one ASP context has no stable model; entire memory query fails. **Default federation contains failure locally.** 6. **Echo corroboration:** two contexts independently summarize the same source and appear as independent support. **Dependence lineage must survive bridge.** 7. **Identity-induced contradiction:** two previously separate entities are reconciled; conflicting propositions suddenly join. **Conflict receipt cites identity assumption/mapping.** 8. **Ontology mapping overclaim:** `A:broader-than B` translated as equivalence, creating spurious defeaters. **Mapping relation/loss must be explicit.** 9. **Undefined collapse:** WFS undefined imported as false or unsupported. **Preserve local undefined status.** 10. **No-model collapse:** ASP no stable model imported as refutation of every queried proposition. **Profile failure, not proposition falsity.** 11. **Resource-status laundering:** local solver timeout imported as epistemic unknown. **Completeness remains separate.** 12. **Undercut flattening:** A undercuts justification J; B only supports positive/negative propositions and turns attack into ¬conclusion. **Reject/noncomposable or retain attack object.** 13. **Revision rewrite:** managed bridge invokes revision and old evidence disappears. **Canonical ledger unchanged; revision output is projection/state lineage.** 14. **Authority injection:** imported policy says `operator may delete X`; bridge treats it as host permission. **Never.** 15. **Bridge cycle bootstrap:** A imports P from B, B imports P from A, no external support. **Cross-context support SCC cannot ground itself unless federation profile explicitly licenses such a fixed point and receipt exposes it.** 16. **Cross-context closed-world leak:** B treats missing exports from A as evidence of negation. **Absence is meaningless unless bridge declares completeness/closure.** 17. **Backdated identity map:** later entity reconciliation retroactively changes what was known historically. **`known_at` queries use mapping state available at transaction time.** 18. **Lossy translation hidden:** stable-model plurality translated to a single WFS answer with no receipt. **Bridge classified lossy/noncomposable; cannot masquerade as exact.** --- # Falsifiable / conformance fixtures C requires at least these executable fixtures later: 1. WFS `not p` crossing an open bridge does not create explicit `¬p` support. 2. Closure-qualified bridge may intentionally translate a closed predicate's absence and receipt names the closure contract. 3. ASP two-model `{p}` / `{¬p}` export remains credulous on both sides; no skeptical P. 4. Skeptical ASP conclusion imported under `skeptical_warrant_as_support` creates a derived support path with local warrant receipt. 5. WFS `undefined` survives round-trip through a federation query. 6. `no_stable_model` stays a local profile failure and does not refute unrelated propositions. 7. Argument undercut crosses only when recipient bridge supports typed attack; otherwise reports noncomposable. 8. Local priorities with same numeric values remain incomparable absent lifting policy. 9. Two summaries of one original article produce two assertions but one independent evidence component after federation. 10. Cross-theory identity assumption induces a conflict only in environments containing that identity mapping. 11. Retracting/weakening the identity mapping removes that federated conflict without deleting original supports. 12. A failing/inconsistent context does not block unrelated evidence-only query over another context. 13. Explicit MCS-equilibrium profile over a bounded cyclic pair reports zero/one/multiple equilibria distinctly. 14. Positive acyclic evidence-only bridges reach a deterministic topological fixed point. 15. Pure bridge cycle with no external support cannot bootstrap ordinary support under baseline federation. 16. Imported default remains inactive unless recipient profile + bridge explicitly admits it. 17. Source dependence survives theory export/import and prevents false corroboration count. 18. `resource_limited` local evaluation remains computational status, not epistemic unknown. 19. Bitemporal `known_at(T)` federation uses bridge/identity/profile versions known at T. 20. Host authority is unchanged by any semantic/epistemic import. 21. Same ledger + same local profile versions + same bridge versions + same federation profile produces replay-equivalent outcome after cache rebuild. 22. Lossy/noncomposable bridge emits explicit diagnostic and never silently drops plurality/undefinedness/attack semantics. --- # Rejected alternatives - **Universal global WFS:** deterministic and convenient but cannot preserve ASP plurality, argumentation acceptance or revision semantics. - **Universal ASP:** expressive but forces all local semantics into stable-model meaning and makes ordinary evidence/support federation unnecessarily model-heavy. - **Trust-weighted global voting:** destroys logical force, copied-source structure, defaults and attacks; multiple assertions are not IID votes. - **Always-global MCS equilibrium:** mathematically valid for selected systems but too brittle/expensive as ambient memory semantics. - **Argumentation-only bus:** excellent derived view, but not faithful to every local outcome type. - **Bridge by proposition ID only:** loses local acceptance/model/profile/provenance and is epistemically unsafe. --- # Concrete canonical changes recommended ## prolog-rlm #392 Keep the existing typed `sem_bridge`, but its semantic-profile work should allow a bridge to reference an **epistemic interoperability contract** rather than implying that proposition mapping alone transfers warrant. Semantic proposition mapping and epistemic admission are separate layers. ## prolog-rlm #394 Add an **Epistemic Federation Fabric** contract: - local theories retain local epistemic profiles; - export local outcome envelopes with support/acceptance/completeness/model scope; - typed bridge import modes; - NAF/absence cannot cross without explicit closure contract; - local priorities/defaults stay namespaced; - source dependence propagates; - identity mappings become explicit assumptions affecting warrant; - federation profile/version required for cross-theory warrant; - `noncomposable`/`lossy_declared` are valid bridge outcomes; - global MCS equilibrium is optional/bounded, not default. ## symbolic-memory #6 Persist enough to replay federation: - bridge contract/version and status; - durable export/import receipts when a federated conclusion is promoted; - source dependence lineage across contexts; - identity/ontology mapping assumptions and lifecycle; - federation profile/version on promoted cross-theory warrant; - bitemporal bridge/mapping state. Do **not** persist one merged global truth graph. ## symbolic-memory #7 Cross-memory query joins need explicit: ```text TheoryRefs BridgePolicy FederationProfile Context/valid_at/known_at ``` and must return local outcome vector + bridge/import receipts + noncomposable edges + mapping assumptions + dependence components. `all memories` is never implicit permission to flatten epistemic semantics. ## #397 / #400 Mark #400C complete, keep #400 open, and queue **#400D** for computational realization/scaling/conformance of ESG + defeat/dependence + federation: query planning, local-result caches, bridge SCC evaluation, incremental invalidation, bounded model/environment products, diagnostics and deterministic differential replay. --- # Unresolved questions preserved for D/later depths - exact minimal bridge type algebra and schema; - formal compatibility checks between common profile pairs (WFS↔ASP, WFS↔argumentation, ASP↔argumentation, revision↔support); - when skeptical export is sound under incomplete/changed source contexts; - incremental maintenance of bridge SCC equilibria; - factorized representation of model products across contexts; - how much source-dependence inference is trusted vs merely hypothesized; - ontology/identity mapping confidence without turning confidence into truth; - federated explanation compression for large dependency graphs; - privacy/partial-knowledge contexts and information-hiding boundaries; - distributed/federated execution across multiple stores/processes (Depth 5/6 may refine); - whether a practical Machine Spirit v1 needs full MCS equilibrium at all, versus typed evidence federation + selected local solvers. ## C decision **Adopt the Epistemic Federation Fabric: local epistemic sovereignty + typed status-bearing exports + explicit admission bridges + query-bounded federation.** Classic heterogeneous MCS equilibrium remains an optional strong federation profile, not global ambient semantics. This materially extends #400A/B rather than replacing them: ESG + typed defeat/dependence remains the local/canonical epistemic substrate; C defines how those local epistemic worlds communicate without lying about their semantics. **Next: #400D.**
nsaspy commented 2026-09-08 01:47:43 +00:00
Author
Owner
Copy link

Depth 3 / #400D — computational realization: demand-driven epistemic federation, projected interfaces, SCC execution and replay

This is subpass D only. It operationalizes the surviving A/B/C architecture (ESG + Typed Defeat/Dependence Graph + Epistemic Federation Fabric) without flattening local epistemic semantics. With this result, Depth 3 can be reconciled and closed as design-complete; this is still implementation-unproven.

Research questions

  1. How can a query cross WFS, ASP, paraconsistent, argumentation and revision-profile theories without enumerating the Cartesian product of all local models/environments?
  2. Which derived results are safe to cache, and what exact evidence/profile/bridge changes invalidate them?
  3. How should acyclic/monotone federation differ operationally from cyclic non-monotonic federation?
  4. Can local solver state be reused incrementally without turning implementation state into canonical truth?
  5. How do we preserve skeptical/credulous/undefined/no-model/conflicted/resource-limited status through distributed execution?
  6. What are the actual structural parameters that determine whether federation is cheap or explosive?
  7. What replay/conformance oracle proves that caches, concurrency and incremental evaluation did not change semantics?

Primary / authoritative sources inspected

  • Terrance Swift, Incremental Tabling in Support of Knowledge Representation and Reasoning (2014): https://arxiv.org/abs/1405.3547 . Transparent incremental tabling maintains consistency of tabled queries under updates in three-valued WFS, with dependency-driven and lazy recomputation. Strong evidence for local WFS/result-cache invalidation, not for one universal federation engine.
  • Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Torsten Schaub, Multi-shot ASP solving with clingo, TPLP 19(1), 2019: https://doi.org/10.1017/S1471068418000054 . Solver/grounder state can be retained while programs evolve; learned state and modular subprogram grounding can be reused. This is the right primitive for local ASP contexts or bounded cyclic federation components.
  • Calimeri, Ianni, Pacenza, Perri, Zangari, Incremental Answer Set Programming with Overgrounding, TPLP (2019): https://doi.org/10.1017/S1471068419000292 . Shows a distinct incremental ASP strategy that grows/reuses grounding rather than rebuilding from zero.
  • Brewka, Ellmauthaler, Gonçalves, Knorr, Leite, Pührer, Reactive Multi-Context Systems: Heterogeneous Reasoning in Dynamic Environments (2016): https://arxiv.org/abs/1609.03438 . rMCSs establish that heterogeneous contexts can evolve under streams; the paper also studies computational complexity and points to skeptical/well-founded alternatives to unrestricted nondeterministic equilibrium reasoning.
  • Drescher, Eiter, Fink, Krennwallner, Walsh, Symmetry Breaking for Distributed Multi-Context Systems (2011): https://arxiv.org/abs/1104.3931 . Distributed MCS search can exploit local/partial symmetries and combine them, demonstrating that global equilibrium search need not naïvely traverse all equivalent combinations.
  • Weinzierl, Advancing Multi-Context Systems by Inconsistency Management (2011): https://arxiv.org/abs/1107.2088 . Cross-context inconsistency diagnosis is itself a first-class problem; automatic global repair is not always desirable. This supports explicit bridge/SCC diagnostics instead of silently dropping bridges to recover an answer.
  • Fandinno & Hecher, Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard, AAAI 2021: https://doi.org/10.1609/aaai.v35i7.16784 . Structural density and positive SCC size materially affect ASP difficulty; cycle/interface structure is a real execution-planning signal.
  • Hecher, Morak, Woltran, Structural Decompositions of Epistemic Logic Programs, AAAI 2020: https://doi.org/10.1609/aaai.v34i03.5672 . Structural decomposition can bound solver calls / yield tractability for bounded treewidth. Useful precedent for bridge-interface decomposition.
  • Bliem, Morak, Woltran, D-FLAT: Declarative Problem Solving Using Tree Decompositions and ASP: https://arxiv.org/abs/1210.1931 . Tree decomposition can make small-width instances substantially cheaper and supports dynamic-programming-style factorization.
  • Fichte & Hecher, Exploiting Treewidth for Counting Projected Answer Sets, KR 2018. Projection is crucial here: many full answer sets can be equivalent once restricted to interface atoms; the projected problem remains hard in general, so projection is an optimization/semantic quotient, not a complexity miracle.
  • Benedikt, Motik, Tsamoura, Goal-Driven Query Answering for Existential Rules With Equality, AAAI 2018: https://doi.org/10.1609/aaai.v32i1.11563 . Query relevance + magic-set-like transformation can turn otherwise infeasible inference into practical goal-directed evaluation; supports demand slicing before federation.

What A/B/C got right

Keep all of these:

  • immutable ESG evidence; derived warrant remains profile-relative;
  • rebut / undermine / undercut / invalidate remain distinct;
  • source-dependence prevents echo corroboration;
  • valid_at and known_at are independent;
  • local theories retain local epistemic semantics;
  • NAF/absence never crosses a theory boundary as explicit negative evidence without closure/admission contracts;
  • bridge compatibility may be lossy or noncomposable;
  • global MCS equilibrium is optional, not ambient truth;
  • evaluation completeness is separate from semantic acceptance.

The missing piece was an execution model that does not turn those distinctions into a combinatorial global-model explosion.

Candidate A — eagerly materialize one global epistemic closure

Translate every local theory, bridge, attack, preference and identity mapping into one global program/materialized closure and keep it continuously updated.

Strengths: simple query path after materialization; easy global indexing.

Failure: semantically wrong for noncomposable profiles and computationally hostile. A local model change can invalidate huge global state; ASP/default model plurality becomes global Cartesian multiplication; one broken/no-model context can contaminate unrelated queries. Reject as canonical execution.

Candidate B — classic distributed MCS equilibrium enumerator

Each context is a local solver. Enumerate local belief states and bridge applications until a federation-wide equilibrium is found; distribute search and add symmetry breaking.

Strengths: clean formal global semantics for a deliberately coupled MCS; heterogeneous engines remain local; mature theory exists for equilibria/inconsistency.

Failure: still too expensive and too strong as default. Most Machine Spirit queries do not need a global equilibrium, and full local models contain huge amounts of information invisible to bridges. Retain only as an explicit bounded mcs_equilibrium profile.

Candidate C — compile everything to one ASP/meta-interpreter

Encode WFS, argumentation, source policies and bridge semantics into one ASP program and use one optimized solver.

Strengths: powerful mature solver; compact deployment; skeptical/credulous query support can be implemented.

Failure: collapses profile semantics into an encoding layer whose correctness becomes the whole system; non-ASP theories become simulations; incremental invalidation and explanations become opaque; authority of profile translators grows dangerously. Reject as universal architecture. ASP remains one backend.

Candidate D — Demand-Driven Interface-Factored Epistemic Executor (preferred)

Compile each federated query into an explicit Epistemic Query Plan (EQP). The planner reasons over theory interfaces and dependencies, not full local world models.

Query + context + epistemic/federation profile
                     ↓
            relevance / capability slice
                     ↓
       bridge dependency graph for this query
                     ↓
            SCC condensation DAG
                     ↓
   local projected interface summaries (cached)
                     ↓
 acyclic delta propagation OR SCC-specific evaluation
                     ↓
 factorized interface-choice / constraint graph
                     ↓
        acceptance + completeness + receipt

Conceptual API:

epistemic_prepare_query(+TheoryGraph,
                        +QueryIR,
                        +Context,
                        +FederationProfile,
                        +Options,
                        -EpistemicQueryPlan).

epistemic_execute_plan(+EpistemicQueryPlan,
                       +RuntimeState,
                       -Outcome).

The existing runtime/scheduler executes plan nodes. EQP is not a second scheduler.

1. Demand slice before reasoning

Start from query predicates/entities/context and walk backward through:

  • local rule/justification dependencies;
  • bridge heads/bodies;
  • identity mappings;
  • defeat/dependence edges;
  • profile compatibility declarations.

Unreachable theories and bridges are excluded. This is analogous in spirit to goal-directed rewriting/magic sets: federation work should be proportional to the relevant dependency region, not total memory size.

The plan must record why each theory/bridge was included.

2. The epistemic interface is the expensive object — not the full local model

For federation, two local states that differ internally but produce the same bridge-visible epistemic exports are equivalent for the current federation query.

Define a projected summary keyed by an explicit boundary signature:

ep_interface_summary(
    SummaryId,
    TheoryRef,
    LocalProfileRef,
    EvidenceFrontier,
    ContextFingerprint,
    InterfaceSignature,
    IncomingBoundary,
    ExportedStatuses,
    AssumptionProjection,
    DependenceProjection,
    LocalReceiptRef).

InterfaceSignature contains only propositions/status dimensions actually visible to selected outgoing bridges or the query.

Hard rule:

full local models M1 != M2
but project_interface(M1) = project_interface(M2)
⇒ federation may quotient them to one interface state

This quotient must not be used for local queries that distinguish M1/M2.

For ASP contexts, prefer solver-native brave/cautious queries or projected answer-set interfaces over enumerating every full answer set. Full model enumeration happens only when the requested semantics genuinely needs it.

3. Condense bridge dependencies into SCCs

Build a query-local dependency graph over theory-interface nodes and bridge edges, then compute strongly connected components.

Acyclic component DAG

Evaluate topologically. Positive/evidence-only edges propagate deltas once their prerequisites change. No global fixed point is required.

Monotone cyclic SCC

Use least-fixed-point / semi-naive delta iteration over the finite admitted status lattice/interface domain when profile contracts prove monotonicity.

WFS-compatible SCC

Use tabled/alternating-fixed-point machinery; local incremental tabling can invalidate/recompute affected tables lazily. Preserve undefined and residual conditions.

ASP / nonmonotonic equilibrium SCC

Do not pretend monotone fixed-point evaluation is sound. Compile a bounded interface search using local solver oracles / multi-shot ASP where compatible. Search over projected interface assignments, not full model Cartesian products. Preserve zero/multiple equilibrium outcomes.

Argumentation SCC

Grounded semantics can use its deterministic fixed-point evaluation. Preferred/stable/etc. semantics require explicit bounded search/enumeration and skeptical/credulous reporting.

Noncomposable SCC

Return noncomposable/partial federation diagnosis. Do not create a synthetic common semantics merely to make the query executable.

4. Factorized epistemic choice graph (FECG)

When a cyclic/nonmonotonic federation requires alternatives, represent them as a shared AND/OR + constraint DAG, not as a materialized list of global worlds.

Conceptual nodes:

AND      independent compatible subchoices
OR       alternative local/interface choices
GUARD    bridge/profile condition
NOGOOD   incompatible assumption/interface combination
LINK     identity/dependence constraint
LEAF     local projected summary / receipt

This is an engine-neutral factorization contract. Implementations may choose BDD/ZDD/d-DNNF/tree-decomposition/solver-native structures where profitable, but none becomes canonical semantics.

Treewidth/separator size of the query-local interface graph, SCC size, number of bridge-visible atoms/statuses and number of genuine alternative interface projections become planning metrics. Structural decomposition literature shows these parameters can materially change feasibility, while also warning that ASP remains hard even at modest structural width. The planner must expose estimates/limits, not promise tractability.

5. Cache immutable derived summaries by exact epistemic frontier

Cache key must include at least:

theory + theory version
local epistemic profile + version
active evidence/lifecycle frontier digest
valid_at + known_at/context fingerprint
query/interface signature
incoming bridge/interface assignment digest where needed
identity/dependence generation
bridge/mapping/profile generation
solver/translation contract version

A cache hit means same derived semantics for that exact frontier, not “same proposition text.”

Ordinary caches remain disposable. Durable promoted decisions/actions retain a replay receipt referencing the exact frontiers and plan.

6. Incremental invalidation is dependency-directed

Maintain derived dependency indexes equivalent to:

evidence/lifecycle → local summaries
local summary/export → outgoing bridge applications
bridge/mapping/identity/dependence → affected SCC
SCC result → downstream SCC/query caches
profile/translator version → all summaries under that profile

Examples:

  • a source withdrawal invalidates only local summaries depending on that support, then changed exports and reachable downstream SCCs;
  • a mapping/identity revision invalidates bridge/interface products that used that mapping, not unrelated local evidence;
  • changing one ASP profile version invalidates that profile's summaries, not WFS caches elsewhere;
  • if recomputation yields the same projected interface digest, downstream invalidation stops at that boundary.

That last rule is important: internal churn that does not alter the federation interface must not cascade globally.

7. Local incremental engine strategy

Backend choices are profile capabilities:

  • WFS / tabled logic: incremental tabling / lazy recomputation where available;
  • ASP: multi-shot solving, retained grounding/learned clauses, or overgrounding for dynamic program fragments;
  • monotone support/Datalog: semi-naive delta maintenance;
  • argumentation: incremental attack/acceptance maintenance when the selected semantics/backend supports it, otherwise rebuild the bounded relevant graph;
  • revision projection: memoize by exact parent epistemic-state/operator/evidence frontier, but revision state is derived lineage, not canonical evidence.

Do not write one fake generic incremental algorithm over semantics it cannot preserve.

8. Query planning must expose structural cost and hard ceilings

An EQP records explicit ceilings such as:

max selected theories / bridge edges
max SCC size
max bridge-visible propositions/status dimensions
max projected local interface states
max solver/oracle calls
max alternative FECG nodes / nogoods
max treewidth/separator estimate accepted for decomposition
max proof/diagnostic bytes
CPU / wall / memory bounds

LLM/model calls are not a fallback for epistemic solver exhaustion. resource_limited remains resource-limited. Once semantics are compiled, all #400 conformance fixtures must be zero-model.

9. Evaluation result separates semantics from execution

Required shape:

semantic acceptance:
  skeptically_warranted | credulously_warranted | rejected |
  undefined | undecided | conflicted | profile_inconsistent |
  noncomposable

evaluation completeness:
  complete | bounded_partial | resource_limited |
  backend_unavailable | solver_error | stale

A complete result may legitimately be undefined or no equilibrium; a partial timeout may not be relabeled unknown or false.

10. Explanation compression

Do not copy giant proof/model trees into every answer. Return a shared receipt DAG:

query-plan receipt
  → selected theory/interface summaries
  → bridge application receipts
  → SCC/fixed-point or search receipt
  → local justification/solver receipts
  → source assertions

Default explanation is a bounded synopsis with IDs and counterevidence; callers can expand local receipts/source spans. Alternative derivations share nodes. For a conflict/noncomposable result, diagnostics must identify the minimal known relevant bridge/profile/interface causes when available; never claim a globally minimal diagnosis unless the algorithm actually proved minimality.

11. Deterministic concurrency

The actor/runtime may evaluate independent SCC-DAG nodes concurrently, but semantic results are identified by immutable plan/frontier/interface keys and combined in deterministic canonical order.

For identical canonical inputs/profile versions/budgets:

scheduler interleaving != semantic result

A race that changes skeptical/credulous/complete status is a correctness bug.

Complexity / scaling contract

No universal polynomial claim is allowed.

  • indexed support lookup / acyclic evidence-only bridge propagation can be database/Datalog-like and incremental;
  • grounded WFS fragments can exploit tabling and unique partial semantics;
  • grounded argumentation semantics is comparatively cheap, while preferred/stable variants can require combinatorial search;
  • ASP brave/skeptical/equilibrium reasoning retains its inherent non-monotonic complexity;
  • global federation can multiply local alternatives, but projecting to bridge interfaces and factorizing by SCC/separators can avoid materializing irrelevant internal combinations;
  • projected model counting itself can remain very hard, so interface width/model budgets must be explicit;
  • cycles and SCC/interface structure are execution-relevant hardness indicators, not mere graph metadata.

Therefore the target is output-/interface-sensitive bounded execution, not a claim that arbitrary heterogeneous epistemic federation is tractable.

Epistemic / provenance implications

  • a cached interface summary preserves local profile/version and support/counterevidence; it is never promoted into source evidence;
  • projection quotienting records what distinctions were intentionally hidden by the federation interface;
  • source dependence is preserved through summaries so federation never multiplies corroboration by model count;
  • identity assumptions and closure/NAF contracts remain explicit FECG guards/receipt dependencies;
  • rebuilding caches must reproduce the same warrant under the same canonical evidence/frontier/profile, modulo explicitly nondeterministic backend artifacts whose semantic outcome is compared extensionally.

Safety / authority implications

  • federation exports remain semantic/epistemic data; no bridge, solver result or warrant grants host capability;
  • resource_limited never triggers an implicit LLM or unsafe executable fallback;
  • imported rule/default/priority names cannot resolve to host predicates;
  • caches are never authority stores;
  • a stale cache cannot satisfy VERIFY/action admission;
  • bounded execution must be cancellation-aware through the existing runtime; EQP/FECG do not create a second autonomous scheduler.

Adversarial failure cases / conformance corpus

At minimum add fixtures for:

  1. irrelevant-theory pruning — 1,000 unrelated theories must not be evaluated for a local query;
  2. DAG propagation — acyclic evidence bridge chain yields same result as clean global evaluation without fixed-point iteration;
  3. interface quotient — 100 local ASP models with two distinct bridge projections produce two interface states, not 100 federation branches;
  4. internal-change frontier stop — local evidence changes but exported interface digest remains identical; downstream caches stay valid;
  5. WFS cycle — negative cycle returns undefined, survives caching/rebuild;
  6. ASP plurality — local/multi-context multiple models preserve skeptical vs credulous status;
  7. no equilibrium — cyclic federation with no equilibrium reports profile failure, not falsehood and not unrelated-theory failure;
  8. noncomposable bridge SCC — query returns bounded noncomposable diagnosis without flattening profiles;
  9. source-dependence projection — many local models/assertions derived from one origin still count as one dependence component;
  10. identity invalidation — changing maybe_same(x,y) invalidates only bridge/SCC results that consumed it;
  11. closure-contract invalidation — changing a cross-theory closed-world contract invalidates NAF-dependent results;
  12. profile upgrade — WFS profile version change invalidates WFS summaries but not unrelated paraconsistent support caches;
  13. bridge edit — changing one bridge invalidates only its SCC/downstream reachable summaries;
  14. budget exhaustion — interface/model budget returns resource_limited, never top-1 truth;
  15. concurrency determinism — different safe interleavings produce the same canonical semantic result/receipt digest;
  16. cache differential oracle — cold evaluation == warm-cache evaluation == cache-rebuilt evaluation under same frontiers;
  17. incremental differential oracle — incremental result == full from-scratch result on the same canonical evidence/profile snapshot;
  18. bitemporal replay — known_at(Tpast) reproduces historical warrant even after later corrections and cache rebuild;
  19. explanation compression — shared derivations are referenced once while all source paths remain expandable;
  20. zero-model execution — all fixtures execute with provider-call count exactly zero;
  21. stale-cache authority — stale/reused derived result is rejected from action/VERIFY admission;
  22. projected-vs-full local check — interface quotient produces federation-equivalent result to full local-model enumeration on a bounded oracle fixture.

Rejected alternatives

  • global eager truth materialization — rejects profile plurality and scales badly;
  • always-global MCS equilibrium — mathematically valid for selected profiles, operationally/epistemically too strong as default;
  • one universal ASP encoding — backend convenience would become hidden universal semantics;
  • full local model Cartesian product — wastes internal distinctions invisible to federation;
  • global ATMS environment enumeration — environment explosion; keep bounded/factorized/query-local;
  • one universal BDD/d-DNNF representation — useful optional compilation technique but can itself blow up and does not encode all profile semantics uniformly;
  • LLM fallback on solver exhaustion — changes a deterministic epistemic failure into untracked heuristic inference; prohibited.

Canonical decision

Adopt the Demand-Driven Interface-Factored Epistemic Executor as the Depth-3 D architecture:

ESG + defeat/dependence + immutable ledger
              ↓
       Epistemic Query Plan
 relevance slice + bridge SCC condensation
              ↓
 local profile-specific projected summaries
              ↓
 acyclic delta flow / profile-specific SCC evaluator
              ↓
 factorized interface alternatives + constraints
              ↓
 warrant + completeness + compressed replay receipt

The canonical semantic history remains in Symbolic Memory; all EQP plans, interface summaries, WFS/ASP tables, FECGs and ordinary warrant caches are rebuildable derived state unless a promoted action/decision requires a durable replay receipt.

Unresolved questions handed forward

  • exact first implementation subset of profile/federation combinations;
  • whether SWI incremental tabling alone is sufficient for intended WFS fragments or an XSB-compatible backend is worth supporting;
  • exact ASP backend/FFI/process isolation contract for multi-shot solving;
  • which optional factorization representation is best for bridge interfaces (solver-native clauses vs BDD/ZDD/d-DNNF/tree-DP);
  • efficient incremental argumentation beyond bounded rebuild;
  • empirical thresholds for SCC/interface-width cutoffs;
  • long-term distribution across processes/nodes belongs primarily to Depth 5 world-model/runtime scaling, not this semantic contract.

Depth-3 conclusion

A/B/C/D now form one coherent design:

A: ESG + explicit epistemic profiles
B: typed defeat/dependence + bitemporal/iterated epistemics
C: local-semantic sovereignty + Epistemic Federation Fabric
D: demand-driven, interface-factored, SCC/incremental execution

Depth 3 is therefore design-complete, implementation-unproven. Canonical handoffs should land on #394, #376 and symbolic-memory #6/#7 before advancing to #401A.

## Depth 3 / #400D — computational realization: demand-driven epistemic federation, projected interfaces, SCC execution and replay This is **subpass D only**. It operationalizes the surviving A/B/C architecture (`ESG + Typed Defeat/Dependence Graph + Epistemic Federation Fabric`) without flattening local epistemic semantics. With this result, Depth 3 can be reconciled and closed as design-complete; this is still **implementation-unproven**. ### Research questions 1. How can a query cross WFS, ASP, paraconsistent, argumentation and revision-profile theories without enumerating the Cartesian product of all local models/environments? 2. Which derived results are safe to cache, and what exact evidence/profile/bridge changes invalidate them? 3. How should acyclic/monotone federation differ operationally from cyclic non-monotonic federation? 4. Can local solver state be reused incrementally without turning implementation state into canonical truth? 5. How do we preserve skeptical/credulous/undefined/no-model/conflicted/resource-limited status through distributed execution? 6. What are the actual structural parameters that determine whether federation is cheap or explosive? 7. What replay/conformance oracle proves that caches, concurrency and incremental evaluation did not change semantics? ## Primary / authoritative sources inspected - Terrance Swift, **Incremental Tabling in Support of Knowledge Representation and Reasoning** (2014): https://arxiv.org/abs/1405.3547 . Transparent incremental tabling maintains consistency of tabled queries under updates in three-valued WFS, with dependency-driven and lazy recomputation. Strong evidence for local WFS/result-cache invalidation, not for one universal federation engine. - Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Torsten Schaub, **Multi-shot ASP solving with clingo**, TPLP 19(1), 2019: https://doi.org/10.1017/S1471068418000054 . Solver/grounder state can be retained while programs evolve; learned state and modular subprogram grounding can be reused. This is the right primitive for local ASP contexts or bounded cyclic federation components. - Calimeri, Ianni, Pacenza, Perri, Zangari, **Incremental Answer Set Programming with Overgrounding**, TPLP (2019): https://doi.org/10.1017/S1471068419000292 . Shows a distinct incremental ASP strategy that grows/reuses grounding rather than rebuilding from zero. - Brewka, Ellmauthaler, Gonçalves, Knorr, Leite, Pührer, **Reactive Multi-Context Systems: Heterogeneous Reasoning in Dynamic Environments** (2016): https://arxiv.org/abs/1609.03438 . rMCSs establish that heterogeneous contexts can evolve under streams; the paper also studies computational complexity and points to skeptical/well-founded alternatives to unrestricted nondeterministic equilibrium reasoning. - Drescher, Eiter, Fink, Krennwallner, Walsh, **Symmetry Breaking for Distributed Multi-Context Systems** (2011): https://arxiv.org/abs/1104.3931 . Distributed MCS search can exploit local/partial symmetries and combine them, demonstrating that global equilibrium search need not naïvely traverse all equivalent combinations. - Weinzierl, **Advancing Multi-Context Systems by Inconsistency Management** (2011): https://arxiv.org/abs/1107.2088 . Cross-context inconsistency diagnosis is itself a first-class problem; automatic global repair is not always desirable. This supports explicit bridge/SCC diagnostics instead of silently dropping bridges to recover an answer. - Fandinno & Hecher, **Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard**, AAAI 2021: https://doi.org/10.1609/aaai.v35i7.16784 . Structural density and positive SCC size materially affect ASP difficulty; cycle/interface structure is a real execution-planning signal. - Hecher, Morak, Woltran, **Structural Decompositions of Epistemic Logic Programs**, AAAI 2020: https://doi.org/10.1609/aaai.v34i03.5672 . Structural decomposition can bound solver calls / yield tractability for bounded treewidth. Useful precedent for bridge-interface decomposition. - Bliem, Morak, Woltran, **D-FLAT: Declarative Problem Solving Using Tree Decompositions and ASP**: https://arxiv.org/abs/1210.1931 . Tree decomposition can make small-width instances substantially cheaper and supports dynamic-programming-style factorization. - Fichte & Hecher, **Exploiting Treewidth for Counting Projected Answer Sets**, KR 2018. Projection is crucial here: many full answer sets can be equivalent once restricted to interface atoms; the projected problem remains hard in general, so projection is an optimization/semantic quotient, not a complexity miracle. - Benedikt, Motik, Tsamoura, **Goal-Driven Query Answering for Existential Rules With Equality**, AAAI 2018: https://doi.org/10.1609/aaai.v32i1.11563 . Query relevance + magic-set-like transformation can turn otherwise infeasible inference into practical goal-directed evaluation; supports demand slicing before federation. ## What A/B/C got right Keep all of these: - immutable ESG evidence; derived warrant remains profile-relative; - rebut / undermine / undercut / invalidate remain distinct; - source-dependence prevents echo corroboration; - `valid_at` and `known_at` are independent; - local theories retain local epistemic semantics; - NAF/absence never crosses a theory boundary as explicit negative evidence without closure/admission contracts; - bridge compatibility may be lossy or noncomposable; - global MCS equilibrium is optional, not ambient truth; - evaluation completeness is separate from semantic acceptance. The missing piece was an execution model that does not turn those distinctions into a combinatorial global-model explosion. --- # Candidate A — eagerly materialize one global epistemic closure Translate every local theory, bridge, attack, preference and identity mapping into one global program/materialized closure and keep it continuously updated. **Strengths:** simple query path after materialization; easy global indexing. **Failure:** semantically wrong for noncomposable profiles and computationally hostile. A local model change can invalidate huge global state; ASP/default model plurality becomes global Cartesian multiplication; one broken/no-model context can contaminate unrelated queries. Reject as canonical execution. --- # Candidate B — classic distributed MCS equilibrium enumerator Each context is a local solver. Enumerate local belief states and bridge applications until a federation-wide equilibrium is found; distribute search and add symmetry breaking. **Strengths:** clean formal global semantics for a deliberately coupled MCS; heterogeneous engines remain local; mature theory exists for equilibria/inconsistency. **Failure:** still too expensive and too strong as default. Most Machine Spirit queries do not need a global equilibrium, and full local models contain huge amounts of information invisible to bridges. Retain only as an explicit bounded `mcs_equilibrium` profile. --- # Candidate C — compile everything to one ASP/meta-interpreter Encode WFS, argumentation, source policies and bridge semantics into one ASP program and use one optimized solver. **Strengths:** powerful mature solver; compact deployment; skeptical/credulous query support can be implemented. **Failure:** collapses profile semantics into an encoding layer whose correctness becomes the whole system; non-ASP theories become simulations; incremental invalidation and explanations become opaque; authority of profile translators grows dangerously. Reject as universal architecture. ASP remains one backend. --- # Candidate D — Demand-Driven Interface-Factored Epistemic Executor **(preferred)** Compile each federated query into an explicit **Epistemic Query Plan (EQP)**. The planner reasons over *theory interfaces and dependencies*, not full local world models. ```text Query + context + epistemic/federation profile ↓ relevance / capability slice ↓ bridge dependency graph for this query ↓ SCC condensation DAG ↓ local projected interface summaries (cached) ↓ acyclic delta propagation OR SCC-specific evaluation ↓ factorized interface-choice / constraint graph ↓ acceptance + completeness + receipt ``` Conceptual API: ```prolog epistemic_prepare_query(+TheoryGraph, +QueryIR, +Context, +FederationProfile, +Options, -EpistemicQueryPlan). epistemic_execute_plan(+EpistemicQueryPlan, +RuntimeState, -Outcome). ``` The existing runtime/scheduler executes plan nodes. **EQP is not a second scheduler.** ## 1. Demand slice before reasoning Start from query predicates/entities/context and walk backward through: - local rule/justification dependencies; - bridge heads/bodies; - identity mappings; - defeat/dependence edges; - profile compatibility declarations. Unreachable theories and bridges are excluded. This is analogous in spirit to goal-directed rewriting/magic sets: federation work should be proportional to the relevant dependency region, not total memory size. The plan must record why each theory/bridge was included. ## 2. The epistemic interface is the expensive object — not the full local model For federation, two local states that differ internally but produce the same bridge-visible epistemic exports are equivalent *for the current federation query*. Define a projected summary keyed by an explicit boundary signature: ```prolog ep_interface_summary( SummaryId, TheoryRef, LocalProfileRef, EvidenceFrontier, ContextFingerprint, InterfaceSignature, IncomingBoundary, ExportedStatuses, AssumptionProjection, DependenceProjection, LocalReceiptRef). ``` `InterfaceSignature` contains only propositions/status dimensions actually visible to selected outgoing bridges or the query. Hard rule: ```text full local models M1 != M2 but project_interface(M1) = project_interface(M2) ⇒ federation may quotient them to one interface state ``` This quotient **must not** be used for local queries that distinguish M1/M2. For ASP contexts, prefer solver-native brave/cautious queries or projected answer-set interfaces over enumerating every full answer set. Full model enumeration happens only when the requested semantics genuinely needs it. ## 3. Condense bridge dependencies into SCCs Build a query-local dependency graph over theory-interface nodes and bridge edges, then compute strongly connected components. ### Acyclic component DAG Evaluate topologically. Positive/evidence-only edges propagate deltas once their prerequisites change. No global fixed point is required. ### Monotone cyclic SCC Use least-fixed-point / semi-naive delta iteration over the finite admitted status lattice/interface domain when profile contracts prove monotonicity. ### WFS-compatible SCC Use tabled/alternating-fixed-point machinery; local incremental tabling can invalidate/recompute affected tables lazily. Preserve `undefined` and residual conditions. ### ASP / nonmonotonic equilibrium SCC Do **not** pretend monotone fixed-point evaluation is sound. Compile a bounded interface search using local solver oracles / multi-shot ASP where compatible. Search over **projected interface assignments**, not full model Cartesian products. Preserve zero/multiple equilibrium outcomes. ### Argumentation SCC Grounded semantics can use its deterministic fixed-point evaluation. Preferred/stable/etc. semantics require explicit bounded search/enumeration and skeptical/credulous reporting. ### Noncomposable SCC Return `noncomposable`/partial federation diagnosis. Do not create a synthetic common semantics merely to make the query executable. ## 4. Factorized epistemic choice graph (FECG) When a cyclic/nonmonotonic federation requires alternatives, represent them as a shared **AND/OR + constraint DAG**, not as a materialized list of global worlds. Conceptual nodes: ```text AND independent compatible subchoices OR alternative local/interface choices GUARD bridge/profile condition NOGOOD incompatible assumption/interface combination LINK identity/dependence constraint LEAF local projected summary / receipt ``` This is an engine-neutral factorization contract. Implementations may choose BDD/ZDD/d-DNNF/tree-decomposition/solver-native structures where profitable, but none becomes canonical semantics. Treewidth/separator size of the **query-local interface graph**, SCC size, number of bridge-visible atoms/statuses and number of genuine alternative interface projections become planning metrics. Structural decomposition literature shows these parameters can materially change feasibility, while also warning that ASP remains hard even at modest structural width. The planner must expose estimates/limits, not promise tractability. ## 5. Cache immutable derived summaries by exact epistemic frontier Cache key must include at least: ```text theory + theory version local epistemic profile + version active evidence/lifecycle frontier digest valid_at + known_at/context fingerprint query/interface signature incoming bridge/interface assignment digest where needed identity/dependence generation bridge/mapping/profile generation solver/translation contract version ``` A cache hit means **same derived semantics for that exact frontier**, not “same proposition text.” Ordinary caches remain disposable. Durable promoted decisions/actions retain a replay receipt referencing the exact frontiers and plan. ## 6. Incremental invalidation is dependency-directed Maintain derived dependency indexes equivalent to: ```text evidence/lifecycle → local summaries local summary/export → outgoing bridge applications bridge/mapping/identity/dependence → affected SCC SCC result → downstream SCC/query caches profile/translator version → all summaries under that profile ``` Examples: - a source withdrawal invalidates only local summaries depending on that support, then changed exports and reachable downstream SCCs; - a mapping/identity revision invalidates bridge/interface products that used that mapping, not unrelated local evidence; - changing one ASP profile version invalidates that profile's summaries, not WFS caches elsewhere; - if recomputation yields the **same projected interface digest**, downstream invalidation stops at that boundary. That last rule is important: internal churn that does not alter the federation interface must not cascade globally. ## 7. Local incremental engine strategy Backend choices are profile capabilities: - WFS / tabled logic: incremental tabling / lazy recomputation where available; - ASP: multi-shot solving, retained grounding/learned clauses, or overgrounding for dynamic program fragments; - monotone support/Datalog: semi-naive delta maintenance; - argumentation: incremental attack/acceptance maintenance when the selected semantics/backend supports it, otherwise rebuild the bounded relevant graph; - revision projection: memoize by exact parent epistemic-state/operator/evidence frontier, but revision state is derived lineage, not canonical evidence. Do not write one fake generic incremental algorithm over semantics it cannot preserve. ## 8. Query planning must expose structural cost and hard ceilings An EQP records explicit ceilings such as: ```text max selected theories / bridge edges max SCC size max bridge-visible propositions/status dimensions max projected local interface states max solver/oracle calls max alternative FECG nodes / nogoods max treewidth/separator estimate accepted for decomposition max proof/diagnostic bytes CPU / wall / memory bounds ``` LLM/model calls are **not** a fallback for epistemic solver exhaustion. `resource_limited` remains resource-limited. Once semantics are compiled, all #400 conformance fixtures must be zero-model. ## 9. Evaluation result separates semantics from execution Required shape: ```text semantic acceptance: skeptically_warranted | credulously_warranted | rejected | undefined | undecided | conflicted | profile_inconsistent | noncomposable evaluation completeness: complete | bounded_partial | resource_limited | backend_unavailable | solver_error | stale ``` A complete result may legitimately be `undefined` or `no equilibrium`; a partial timeout may not be relabeled `unknown` or `false`. ## 10. Explanation compression Do not copy giant proof/model trees into every answer. Return a shared receipt DAG: ```text query-plan receipt → selected theory/interface summaries → bridge application receipts → SCC/fixed-point or search receipt → local justification/solver receipts → source assertions ``` Default explanation is a bounded synopsis with IDs and counterevidence; callers can expand local receipts/source spans. Alternative derivations share nodes. For a conflict/noncomposable result, diagnostics must identify the minimal *known* relevant bridge/profile/interface causes when available; never claim a globally minimal diagnosis unless the algorithm actually proved minimality. ## 11. Deterministic concurrency The actor/runtime may evaluate independent SCC-DAG nodes concurrently, but semantic results are identified by immutable plan/frontier/interface keys and combined in deterministic canonical order. For identical canonical inputs/profile versions/budgets: ```text scheduler interleaving != semantic result ``` A race that changes skeptical/credulous/complete status is a correctness bug. ## Complexity / scaling contract No universal polynomial claim is allowed. - indexed support lookup / acyclic evidence-only bridge propagation can be database/Datalog-like and incremental; - grounded WFS fragments can exploit tabling and unique partial semantics; - grounded argumentation semantics is comparatively cheap, while preferred/stable variants can require combinatorial search; - ASP brave/skeptical/equilibrium reasoning retains its inherent non-monotonic complexity; - global federation can multiply local alternatives, but **projecting to bridge interfaces and factorizing by SCC/separators can avoid materializing irrelevant internal combinations**; - projected model counting itself can remain very hard, so interface width/model budgets must be explicit; - cycles and SCC/interface structure are execution-relevant hardness indicators, not mere graph metadata. Therefore the target is **output-/interface-sensitive bounded execution**, not a claim that arbitrary heterogeneous epistemic federation is tractable. ## Epistemic / provenance implications - a cached interface summary preserves local profile/version and support/counterevidence; it is never promoted into source evidence; - projection quotienting records what distinctions were intentionally hidden by the federation interface; - source dependence is preserved through summaries so federation never multiplies corroboration by model count; - identity assumptions and closure/NAF contracts remain explicit FECG guards/receipt dependencies; - rebuilding caches must reproduce the same warrant under the same canonical evidence/frontier/profile, modulo explicitly nondeterministic backend artifacts whose semantic outcome is compared extensionally. ## Safety / authority implications - federation exports remain semantic/epistemic data; no bridge, solver result or warrant grants host capability; - `resource_limited` never triggers an implicit LLM or unsafe executable fallback; - imported rule/default/priority names cannot resolve to host predicates; - caches are never authority stores; - a stale cache cannot satisfy VERIFY/action admission; - bounded execution must be cancellation-aware through the existing runtime; EQP/FECG do not create a second autonomous scheduler. ## Adversarial failure cases / conformance corpus At minimum add fixtures for: 1. **irrelevant-theory pruning** — 1,000 unrelated theories must not be evaluated for a local query; 2. **DAG propagation** — acyclic evidence bridge chain yields same result as clean global evaluation without fixed-point iteration; 3. **interface quotient** — 100 local ASP models with two distinct bridge projections produce two interface states, not 100 federation branches; 4. **internal-change frontier stop** — local evidence changes but exported interface digest remains identical; downstream caches stay valid; 5. **WFS cycle** — negative cycle returns `undefined`, survives caching/rebuild; 6. **ASP plurality** — local/multi-context multiple models preserve skeptical vs credulous status; 7. **no equilibrium** — cyclic federation with no equilibrium reports profile failure, not falsehood and not unrelated-theory failure; 8. **noncomposable bridge SCC** — query returns bounded noncomposable diagnosis without flattening profiles; 9. **source-dependence projection** — many local models/assertions derived from one origin still count as one dependence component; 10. **identity invalidation** — changing `maybe_same(x,y)` invalidates only bridge/SCC results that consumed it; 11. **closure-contract invalidation** — changing a cross-theory closed-world contract invalidates NAF-dependent results; 12. **profile upgrade** — WFS profile version change invalidates WFS summaries but not unrelated paraconsistent support caches; 13. **bridge edit** — changing one bridge invalidates only its SCC/downstream reachable summaries; 14. **budget exhaustion** — interface/model budget returns `resource_limited`, never top-1 truth; 15. **concurrency determinism** — different safe interleavings produce the same canonical semantic result/receipt digest; 16. **cache differential oracle** — cold evaluation == warm-cache evaluation == cache-rebuilt evaluation under same frontiers; 17. **incremental differential oracle** — incremental result == full from-scratch result on the same canonical evidence/profile snapshot; 18. **bitemporal replay** — `known_at(Tpast)` reproduces historical warrant even after later corrections and cache rebuild; 19. **explanation compression** — shared derivations are referenced once while all source paths remain expandable; 20. **zero-model execution** — all fixtures execute with provider-call count exactly zero; 21. **stale-cache authority** — stale/reused derived result is rejected from action/VERIFY admission; 22. **projected-vs-full local check** — interface quotient produces federation-equivalent result to full local-model enumeration on a bounded oracle fixture. ## Rejected alternatives - **global eager truth materialization** — rejects profile plurality and scales badly; - **always-global MCS equilibrium** — mathematically valid for selected profiles, operationally/epistemically too strong as default; - **one universal ASP encoding** — backend convenience would become hidden universal semantics; - **full local model Cartesian product** — wastes internal distinctions invisible to federation; - **global ATMS environment enumeration** — environment explosion; keep bounded/factorized/query-local; - **one universal BDD/d-DNNF representation** — useful optional compilation technique but can itself blow up and does not encode all profile semantics uniformly; - **LLM fallback on solver exhaustion** — changes a deterministic epistemic failure into untracked heuristic inference; prohibited. ## Canonical decision Adopt the **Demand-Driven Interface-Factored Epistemic Executor** as the Depth-3 D architecture: ```text ESG + defeat/dependence + immutable ledger ↓ Epistemic Query Plan relevance slice + bridge SCC condensation ↓ local profile-specific projected summaries ↓ acyclic delta flow / profile-specific SCC evaluator ↓ factorized interface alternatives + constraints ↓ warrant + completeness + compressed replay receipt ``` The canonical semantic history remains in Symbolic Memory; all EQP plans, interface summaries, WFS/ASP tables, FECGs and ordinary warrant caches are rebuildable derived state unless a promoted action/decision requires a durable replay receipt. ## Unresolved questions handed forward - exact first implementation subset of profile/federation combinations; - whether SWI incremental tabling alone is sufficient for intended WFS fragments or an XSB-compatible backend is worth supporting; - exact ASP backend/FFI/process isolation contract for multi-shot solving; - which optional factorization representation is best for bridge interfaces (solver-native clauses vs BDD/ZDD/d-DNNF/tree-DP); - efficient incremental argumentation beyond bounded rebuild; - empirical thresholds for SCC/interface-width cutoffs; - long-term distribution across processes/nodes belongs primarily to Depth 5 world-model/runtime scaling, not this semantic contract. ### Depth-3 conclusion A/B/C/D now form one coherent design: ```text A: ESG + explicit epistemic profiles B: typed defeat/dependence + bitemporal/iterated epistemics C: local-semantic sovereignty + Epistemic Federation Fabric D: demand-driven, interface-factored, SCC/incremental execution ``` Depth 3 is therefore **design-complete, implementation-unproven**. Canonical handoffs should land on #394, #376 and symbolic-memory #6/#7 before advancing to #401A.
Sign in to join this conversation.
No Branch/Tag specified
Branches Tags
main
feat/prolog-rlm-language
codex/claude-api-provider
codex/symbolic-experts
codex/openai-api-provider
feat/zai-provider-protocols
hardening/project-semantic-20260911
hardening/ws7-nix-ci-pinning
chore/track-prolog
rage/98-semantic-project-knowledge
fix/339-agent-zero-skill-graph
ci/tree-sitter-runner-labels
issue-293
research/text-streaming
docs/agent-editor-handoff
icon-add
hydra/fleet-jobs-20260904
rage/355-d6-11-plan-native-dispatch
cd/nix-installer-action-url
issue-355
rage/97-query-capture-apis
research/expert-direct-tool-projection
rage/96-versioned-syntax-facts
fix/direct-deadline-typing
dogfood/auto-dig-native-tools
feature/rage-feature-freeze
fix/323-native-batch-cardinality
fix/328-direct-user-namespace-text-string
fix/transient-provider-retry-2026-09-01
fix/openrouter-dotted-tool-result-name
rage/325-native-call-isolation
fix/316-original-batch-effect-isolation
fix/313-per-call-preflight
fix/312-peek-schema-contract
docs/agents-worktree-rule
fix/child-native-capability-narrowing
test/paid-lane-glm-53-flash
docs/spec-seeded-symbolic-plans
rage/290-spec-plan-authority
fix/304-context-peek-selector-contract
fix/298-native-any-json-schema
rage/288-spec-plan-graph-executor
feat/spec-plan-flow-api
prolog-rlm-v1
gpt-5-6-sol-high/questions-for-rlm-prolog-and-lambda-rlm
rage/277-planner-protocol-context
research-approval/rlm-research-026-task-deadlines-20260827135838
research-approval/rlm-research-025-lem-ui-20260827135751
rage/183-live-operator-behavior
agent/127-agentprolog-config
recovery/132-agentprolog-monorepo
rage/223-durable-context-mount-recovery
rage/223-constraint-benchmark-recovery
research-approval/rlm-research-011-managed-context-tool-discovery-20260827054019
feat/research-approval-schema
agent/rrlm-control-plane-research
docs/219-adrrd-review
salvage/231-runtime-status
salvage/231-runtime-status-run
tmp
tmp2
tmp3
rage/245-planner-structural-retry
rage/168-skill-selection-eval
rage/250-skill-catalog-graph
rage/56-result-acceptance
rage/172-parent-resume-replan
rage/175-deadline-policy-recovery
rage/257-provider-tool-choice-normalization
agent/tool-result-projection-presets
fix/234-numeric-schema-bounds
feature/231-rlm-cli-reference-harness
feature/223-durable-context-mounts
feature/223-real-constraint-benchmark
feature/223-real-constraint-benchmark-clean
feature/223-real-constraint-benchmark-final
feature/223-real-constraint-benchmark-impl
feature/223-real-constraint-benchmark-now
feature/223-real-constraint-benchmark-tdd
feature/223-real-constraint-benchmark-work
rage/176-root-planner-tool-projection
rage/172-typed-delegation-policy
rage/175-subagent-deadline-policy
rage/206-prompt-command-runtime
rage/203-subagent-skill-role-provenance
rage/200-permanent-rlm-context
fix/190-cli-help-success
archive/pr-132-agentprolog-config-20260827
feature/117-prolog-skill-activation-linear
feature/117-prolog-skill-activation
fix/194-completion-budget-usage
fix/191-capability-filtered-tool-schemas
fix/185-reasoning-effort
ci/report-workflow-failures-20260825
cleanup/186-remove-legacy-harnesses
fix/185-reasoning-routing
agent/evolution-async-evaluator
rage/181-binding-replay-race
agent/124-deepseek-harness-prolog
rage/144-fallback-closure
rage/164-conversation-metadata
agent/subagent-supervised-call-conformance
fix/160-context-adapter-closed-data
codex/move-agent-zero-adaptor
codex/sol-high-integration
fix/151-plunit-gate
fix/165-evolution-closed-data
fix/162-async-control-exceptions
fix/158-prompt-compiler-closed-dicts
fix/151-plunit-main-ownership
fix/156-registry-destroy-hooks
fix/154-anonymous-dict-canonicalization
fix/flake-lock-reproducibility
agent/issue-142-evolution-kernel
agent/141-flake-runtime-package
agent/rlm-subagent-runtime
agent/144-subagent-fallback-a
agent/107-bound-adapter-metadata
validation/clean-pack-install
fix/45-authoritative-nested-model-events
fix/46-router-safe-live-streaming
agent/prompt-context-compiler
agent/42-canonical-recursive-fingerprints
agent/136-static-load-errors-fail-ci
agent/44-completion-error-usage
fix/67-loader-registry-cleanup
agent/opentui-solid-reference-client-current
agent/95-project-source-registry
feature/issue-117-prolog-skill-compiler
backlog/roadmap-86-merged
agent/opentui-solid-reference-client
79-tool-effect-boundary
agent/prolog-agent-ui-research
agent/conversation-cold-context
agent/94-tree-sitter-ffi
agent/conversation-warm-context
111-opentui-solid-reference-client
109-prolog-agent-ui-v1
agent/conversation-runtime
agent/spec-mode-language
agent/spec-verify-foundation
agent/prompt-compiler-research
reconcile-backlog-postmerge
reconcile-backlog-issues
agent/prolog-agent-roadmap
feature/issue-84-effect-store-migration
fix/issue-80-effect-substrate-adversarial-hardening
feature/issue-57-effect-identity
agent/mcp-declaration-security
agent/external-tool-category-boundary
feature/issue-53-authority-pending-async
feature/issue-54-agent-graph-canonical-async
feature/issue-54-tools-mcp-canonical-async
feature/issue-54-async-canonical-runtime
agent/dual-sync-async-runtime
agent/reconcile-todo-status
feature/issue-20-deep-recursion-experiments
feature/issue-19-cli-demo-trace
feature/issue-18-benchmark-conformance
feature/issue-17-adaptive-recursion
feature/issue-16-durable-artifacts
feature/issue-15-mcp-2026-dual-version
feature/issue-14-mcp-2025-11-25
hotfix/live-tool-native-openrouter
feature/issue-13-chain-runtime
fix/stable-live-repair-gate
fix/live-repair-strategy-parser
feature/issue-12-durable-graph
feature/issue-11-agent-supervision
feature/issue-10-structured-outcomes-repair
feature/issue-9-rlm-completion
feature/issue-8-capability-tools
feature/issue-7-typed-plan-runtime
feature/issue-6-context-store
fix/openrouter-reasoning-response
fix/live-openrouter-smoke-stability
feature/issue-5-openrouter-provider
feature/issue-4-swi-bootstrap
agent/agentic-harness-research
agent/prolog-rlm-foundation
No results found.
Labels
Clear labels   
bug
Something isn't working

  
documentation
Improvements or additions to documentation

  
duplicate
This issue or pull request already exists

  
enhancement
New feature or request

  
good first issue
Good for newcomers

  
help wanted
Extra attention is needed

  
invalid
This doesn't seem right

  
question
Further information is requested

  
wontfix
This will not be worked on

No labels
bug
documentation
duplicate
enhancement
good first issue
help wanted
invalid
question
wontfix
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
nsaspy/prolog-rlm#398
No description provided.