nsaspy/prolog-rlm

Fork 0

[semantic-reasoning] Safe lowering and reasoning semantics for negation, defaults, exceptions, uncertainty, time, causality, and constraints #404

New issue

Open

opened 2026-09-08 01:29:19 +00:00 by nsaspy · 6 comments

nsaspy commented

2026-09-08 01:29:19 +00:00

Owner

Parent: #388
Depends on: #392

Goal

Define the trusted reasoning/lowering layer that turns validated semantic IR into queryable Prolog semantics without treating arbitrary generated terms as executable code.

Required semantics

Implement safe handling for at least:

strict implication;
conjunction and bounded alternatives;
explicit negation;
open-world unknown;
declared closed-world scopes where explicitly configured;
defaults / normally;
exceptions / unless;
defeasible conclusions and competing rules;
attributed claims/beliefs;
uncertainty/modal qualification;
temporal validity and event ordering;
causal/diagnostic relations;
procedural ordering/branches;
arithmetic/cardinality/unit constraints;
hypothesis/scenario/counterfactual scope;
provenance-aware derivation/explanation.

Hard distinction

semantic relation named restart
        !=
trusted predicate restart/1
        !=
capability to restart anything

Unknown/open vocabulary remains data interpreted by generic semantic predicates. Only trusted closed constructors/adapters may lower to executable/queryable Prolog predicates or constraint calls.

Negation / unknown

Do not use ordinary Prolog failure as a universal semantic false.

The layer must distinguish:

true
explicit_false
unknown
conflicted
unsupported

and preserve source scope/provenance.

Defaults / exceptions

Provide explicit representation and evaluation policy for natural-language defaults such as:

Birds normally fly.
Penguins do not fly.

The implementation may use priorities/specificity/defeasible records, but behavior must be deterministic, inspectable and provenance-preserving. Do not silently encode default reasoning as raw clause order.

Conflicts

Contradictory assertions/rules may coexist. Query outcomes need to expose conflict rather than arbitrary winner selection unless an explicit trusted resolution policy applies.

Temporal reasoning

Support reusable trusted predicates over explicit time/interval data:

before/after/during/overlap
valid_at
valid_during
historical/current
sequence/deadline

Unresolved relative time remains unresolved rather than being invented.

Constraint lowering

Validated safe quantitative forms should lower to trusted CLP facilities where appropriate:

CLP(FD) for integer/cardinality/finite-domain constraints;
CLP(Q/R) for rational/real arithmetic where supported;
unit/dimension normalization before comparison.

Unknown expressions remain symbolic rather than evaluated through arbitrary Prolog.

Explanation

Every derived result should be able to return a proof/evidence structure identifying:

semantic rule(s) applied;
premises;
defaults/exceptions;
source/provenance refs;
unresolved/conflicting premises;
constraint solver result where used;
scope/time assumptions.

MACHINE-SPIRIT #400A epistemic foundation: support graph + explicit profiles

Depth 3A found that truth, support, and acceptance must be separate layers.

The canonical reasoning boundary should consume an Epistemic Support Graph (ESG) built over #392 propositions/assertions/contexts/justifications:

positive and negative support are independent;
support/refutation may coexist without explosion;
justifications are explicit dependency hyperedges;
assumption/context environments are explicit;
withdrawals, corrections, supersession and derivation invalidation are lifecycle events, not aliases for negation;
temporal change is resolved by validity/context before epistemic conflict detection;
derived acceptance is always relative to an explicit versioned epistemic profile.

Base support state should be representable independently of final acceptance:

no positive + no negative -> neither
positive + no negative    -> supported_only
no positive + negative    -> refuted_only
positive + negative       -> both/conflicted

This Belnap-like support summary is not itself the universal consequence relation.

Candidate profile family established by #400A:

support_paraconsistent   preserve/report support and counterevidence; no automatic winner
well_founded_default     candidate deterministic default profile for admitted tabled logic-program fragments
stable_models            optional multi-model default/nonmonotonic profile; expose skeptical vs credulous results
argumentation            derived argument/attack/defeat view for contested/default reasoning
revision_projection      AGM-inspired coherent operational belief projection; never canonical destructive storage

Do not silently choose a profile from predicate name or Prolog clause order.

Conceptual query 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)).

Hard invariants added by #400A:

withdraw(assertion(P)) != assert(not(P))
temporal_change != belief_revision
defeated_default(P) != explicit_false(P)
source_trust != proposition_probability
supersession != destruction
warranted(semantic_action(A)) != capability(A)

A source correction that explicitly asserts the opposite may add negative support, but mere withdrawal must not manufacture it.

Defaults must be explicit semantic objects with conditions, conclusion, exceptions, priority/specificity metadata, scope and provenance. Exact default-priority/reinstatement semantics remain intentionally open for #400B; do not freeze them as raw clause ordering.

Implementation direction: canonical ESG inputs are immutable; current support/warrant indexes are rebuildable derived state. Premise/lifecycle/context changes invalidate only dependent justifications/profile views. For SWI-compatible bounded default fragments, tabled Well-Founded Semantics via tnot/1 is a strong candidate implementation primitive because it provides a unique partial result and residual undefined conditions; it must not conflate explicit negation with negation-as-failure.

Acceptance

Explicit false differs from unknown.
Default + exception fixture yields expected defeasible result with explanation.
Conflicting sources return conflict rather than clause-order winner.
Attributed belief does not satisfy an unqualified-world query automatically.
Historical fact cannot satisfy a current-only query outside its validity interval.
Hypothetical/counterfactual facts remain scenario-scoped.
Safe CLP fixture solves numeric/cardinality constraints from semantic IR.
Unknown domain predicate cannot reach arbitrary call/1.
Symbolic procedure steps remain inert until explicitly mapped to trusted capabilities.
Derived result exposes supporting semantic/provenance path.
Positive and negative support can coexist and remain queryable without explosion.
Withdrawal removes current support without synthesizing explicit negative support.
Two independent derivations survive loss of only one derivation path.
A selected epistemic profile/version is visible in every nontrivial warranted-result receipt.
Stable/multi-model profiles expose skeptical/credulous plurality rather than selecting the first model.
Resource exhaustion in environment/model exploration returns bounded undecided/resource-limited state, not arbitrary truth.

Non-goals

no natural-language parsing;
no host action execution;
no persistent memory database;
no final universal default-priority/reinstatement policy before Machine Spirit #400B-#400D.

Refs #388 #392 #56 #93 #397 #400.

Parent: #388 Depends on: #392 ## Goal Define the trusted reasoning/lowering layer that turns validated semantic IR into queryable Prolog semantics without treating arbitrary generated terms as executable code. ## Required semantics Implement safe handling for at least: - strict implication; - conjunction and bounded alternatives; - explicit negation; - open-world unknown; - declared closed-world scopes where explicitly configured; - defaults / normally; - exceptions / unless; - defeasible conclusions and competing rules; - attributed claims/beliefs; - uncertainty/modal qualification; - temporal validity and event ordering; - causal/diagnostic relations; - procedural ordering/branches; - arithmetic/cardinality/unit constraints; - hypothesis/scenario/counterfactual scope; - provenance-aware derivation/explanation. ## Hard distinction ```text semantic relation named restart != trusted predicate restart/1 != capability to restart anything ``` Unknown/open vocabulary remains data interpreted by generic semantic predicates. Only trusted closed constructors/adapters may lower to executable/queryable Prolog predicates or constraint calls. ## Negation / unknown Do not use ordinary Prolog failure as a universal semantic `false`. The layer must distinguish: ```text true explicit_false unknown conflicted unsupported ``` and preserve source scope/provenance. ## Defaults / exceptions Provide explicit representation and evaluation policy for natural-language defaults such as: ```text Birds normally fly. Penguins do not fly. ``` The implementation may use priorities/specificity/defeasible records, but behavior must be deterministic, inspectable and provenance-preserving. Do not silently encode default reasoning as raw clause order. ## Conflicts Contradictory assertions/rules may coexist. Query outcomes need to expose conflict rather than arbitrary winner selection unless an explicit trusted resolution policy applies. ## Temporal reasoning Support reusable trusted predicates over explicit time/interval data: ```text before/after/during/overlap valid_at valid_during historical/current sequence/deadline ``` Unresolved relative time remains unresolved rather than being invented. ## Constraint lowering Validated safe quantitative forms should lower to trusted CLP facilities where appropriate: - CLP(FD) for integer/cardinality/finite-domain constraints; - CLP(Q/R) for rational/real arithmetic where supported; - unit/dimension normalization before comparison. Unknown expressions remain symbolic rather than evaluated through arbitrary Prolog. ## Explanation Every derived result should be able to return a proof/evidence structure identifying: - semantic rule(s) applied; - premises; - defaults/exceptions; - source/provenance refs; - unresolved/conflicting premises; - constraint solver result where used; - scope/time assumptions. ## MACHINE-SPIRIT #400A epistemic foundation: support graph + explicit profiles Depth 3A found that `truth`, `support`, and `acceptance` must be separate layers. The canonical reasoning boundary should consume an **Epistemic Support Graph (ESG)** built over #392 propositions/assertions/contexts/justifications: - positive and negative support are independent; - support/refutation may coexist without explosion; - justifications are explicit dependency hyperedges; - assumption/context environments are explicit; - withdrawals, corrections, supersession and derivation invalidation are lifecycle events, not aliases for negation; - temporal change is resolved by validity/context before epistemic conflict detection; - derived acceptance is always relative to an explicit versioned epistemic profile. Base support state should be representable independently of final acceptance: ```text no positive + no negative -> neither positive + no negative -> supported_only no positive + negative -> refuted_only positive + negative -> both/conflicted ``` This Belnap-like support summary is **not itself the universal consequence relation**. Candidate profile family established by #400A: ```text support_paraconsistent preserve/report support and counterevidence; no automatic winner well_founded_default candidate deterministic default profile for admitted tabled logic-program fragments stable_models optional multi-model default/nonmonotonic profile; expose skeptical vs credulous results argumentation derived argument/attack/defeat view for contested/default reasoning revision_projection AGM-inspired coherent operational belief projection; never canonical destructive storage ``` Do not silently choose a profile from predicate name or Prolog clause order. Conceptual query 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)). ``` Hard invariants added by #400A: ```text withdraw(assertion(P)) != assert(not(P)) temporal_change != belief_revision defeated_default(P) != explicit_false(P) source_trust != proposition_probability supersession != destruction warranted(semantic_action(A)) != capability(A) ``` A source correction that explicitly asserts the opposite may add negative support, but mere withdrawal must not manufacture it. Defaults must be explicit semantic objects with conditions, conclusion, exceptions, priority/specificity metadata, scope and provenance. **Exact default-priority/reinstatement semantics remain intentionally open for #400B; do not freeze them as raw clause ordering.** Implementation direction: canonical ESG inputs are immutable; current support/warrant indexes are rebuildable derived state. Premise/lifecycle/context changes invalidate only dependent justifications/profile views. For SWI-compatible bounded default fragments, tabled Well-Founded Semantics via `tnot/1` is a strong candidate implementation primitive because it provides a unique partial result and residual undefined conditions; it must not conflate explicit negation with negation-as-failure. ## Acceptance - [ ] Explicit false differs from unknown. - [ ] Default + exception fixture yields expected defeasible result with explanation. - [ ] Conflicting sources return conflict rather than clause-order winner. - [ ] Attributed belief does not satisfy an unqualified-world query automatically. - [ ] Historical fact cannot satisfy a current-only query outside its validity interval. - [ ] Hypothetical/counterfactual facts remain scenario-scoped. - [ ] Safe CLP fixture solves numeric/cardinality constraints from semantic IR. - [ ] Unknown domain predicate cannot reach arbitrary `call/1`. - [ ] Symbolic procedure steps remain inert until explicitly mapped to trusted capabilities. - [ ] Derived result exposes supporting semantic/provenance path. - [ ] Positive and negative support can coexist and remain queryable without explosion. - [ ] Withdrawal removes current support without synthesizing explicit negative support. - [ ] Two independent derivations survive loss of only one derivation path. - [ ] A selected epistemic profile/version is visible in every nontrivial warranted-result receipt. - [ ] Stable/multi-model profiles expose skeptical/credulous plurality rather than selecting the first model. - [ ] Resource exhaustion in environment/model exploration returns bounded undecided/resource-limited state, not arbitrary truth. ## Non-goals - no natural-language parsing; - no host action execution; - no persistent memory database; - no final universal default-priority/reinstatement policy before Machine Spirit #400B-#400D. Refs #388 #392 #56 #93 #397 #400.

nsaspy referenced this issue

2026-09-08 01:29:21 +00:00

[EPIC][expert] Repair / diagnosis expert: failure hypotheses, evidence gaps, bounded repair, and no-progress detection #413

nsaspy referenced this issue

2026-09-08 01:29:22 +00:00

[EPIC][expert] Planner / coordinator expert: symbolic decomposition, expert assignment, and bounded replanning #419

nsaspy referenced this issue

2026-09-08 01:46:20 +00:00

[EPIC][P0] First-class Prolog expert system: registry, routing, specialists, and closed-loop Spec→Plan→Expert→Verify→Repair #422

nsaspy referenced this issue

2026-09-08 01:46:24 +00:00

[EPIC][experts] Canonical expert runtime: contract, registry, symbolic selection, invocation, recursion, and projections #421

nsaspy referenced this issue

2026-09-08 01:46:24 +00:00

[EPIC][experts] Canonical expert runtime: contract, registry, symbolic selection, invocation, recursion, and projections #421

nsaspy referenced this issue

2026-09-08 01:46:24 +00:00

[EPIC][experts] Canonical expert runtime: contract, registry, symbolic selection, invocation, recursion, and projections #421

nsaspy referenced this issue

2026-09-08 01:46:31 +00:00

[EPIC][expert] Planner / coordinator expert: symbolic decomposition, expert assignment, and bounded replanning #419

nsaspy referenced this issue

2026-09-08 01:46:48 +00:00

[EPIC][expert] VERIFY expert: evidence plans, independent validation, proof-carrying outcomes, and exact Frozen-Spec acceptance #414

nsaspy referenced this issue

2026-09-08 01:46:50 +00:00

[EPIC][expert] Repair / diagnosis expert: failure hypotheses, evidence gaps, bounded repair, and no-progress detection #413

nsaspy referenced this issue

2026-09-08 01:46:50 +00:00

[EPIC][expert] Repair / diagnosis expert: failure hypotheses, evidence gaps, bounded repair, and no-progress detection #413

nsaspy referenced this issue

2026-09-08 01:46:52 +00:00

[EPIC][expert] Review / critic expert: adversarial change analysis, regression discovery, and evidence-backed findings #412

nsaspy referenced this issue

2026-09-08 01:47:15 +00:00

[semantic-compiler] Multi-pass semantic induction: discourse, coreference, events, rules, procedures, constraints, and cross-sentence linking #405

nsaspy commented

2026-09-08 01:47:18 +00:00

Author

Owner

MACHINE-SPIRIT #398D handoff — compile semantic reasoning into explicit deductive plans

Depth-1 KR research now requires #394 to expose a backend-neutral deductive plan compilation boundary rather than treating semantic_lower/3 as a direct IR→Prolog-clause transform.

Recommended conceptual split:

semantic_prepare_query(+TheoryGraph, +QueryIR, +Options, -DeductivePlan).
semantic_execute_plan(+DeductivePlan, +RuntimeState, -Outcome).

A plan should record at least:

selected theories/versions and theory edges
semantic profiles and compatibility contracts
query signature/bindings
normalized closed safe rules
rule SCC/stratification metadata where applicable
chosen evaluation strategy per component
required indexes/materializations/tables
demand/magic-set-style transformations where used
trusted CLP/CHR solver nodes
resource ceilings
proof/justification capture policy
unsupported/preservation-only semantics
semantic dependency/freshness generation
plan fingerprint

Required evaluation-strategy semantics

For admitted fragments, support strategy selection equivalent to:

indexed ground lookup
function-free Horn/Datalog semi-naive materialization
demand-transformed/magic-set-style bottom-up evaluation
tabled query-directed evaluation
incremental invalidation/re-evaluation
trusted CLP(FD), CLP(Q/R), temporal/other solver profiles
trusted CHR profile for explicitly admitted solver/normalization programs
preservation/structural query only for unsupported quantified semantics

Do not use an LLM to choose among strategies when deterministic query/profile/theory metadata suffices.

Outcome semantics

Execution status must not collapse into logical truth:

true / explicit_false / unknown / conflicted
!=
unsupported / resource_exhausted / backend_unavailable / stale

Timeout/resource exhaustion is never semantic false.

Freshness and explanation

Derived tables/materializations are rebuildable caches keyed to semantic/theory generations. Changes to assertions, theory mappings, bridges, rules or lifecycle status invalidate only dependent derived state where backend capability permits it.

Successful material conclusions/action-relevant evidence should be able to carry a replayable derivation receipt referencing plan fingerprint, rules, premises, theory edges, solver receipts and semantic generation.

This is architecture input only; exact default/negation/paraconsistent semantics remain owned by #394/#400 rather than being accidentally defined by the execution backend. Full design and sources are preserved in #398D.

## MACHINE-SPIRIT #398D handoff — compile semantic reasoning into explicit deductive plans Depth-1 KR research now requires #394 to expose a backend-neutral **deductive plan compilation boundary** rather than treating `semantic_lower/3` as a direct IR→Prolog-clause transform. Recommended conceptual split: ```prolog semantic_prepare_query(+TheoryGraph, +QueryIR, +Options, -DeductivePlan). semantic_execute_plan(+DeductivePlan, +RuntimeState, -Outcome). ``` A plan should record at least: ```text selected theories/versions and theory edges semantic profiles and compatibility contracts query signature/bindings normalized closed safe rules rule SCC/stratification metadata where applicable chosen evaluation strategy per component required indexes/materializations/tables demand/magic-set-style transformations where used trusted CLP/CHR solver nodes resource ceilings proof/justification capture policy unsupported/preservation-only semantics semantic dependency/freshness generation plan fingerprint ``` ### Required evaluation-strategy semantics For admitted fragments, support strategy selection equivalent to: ```text indexed ground lookup function-free Horn/Datalog semi-naive materialization demand-transformed/magic-set-style bottom-up evaluation tabled query-directed evaluation incremental invalidation/re-evaluation trusted CLP(FD), CLP(Q/R), temporal/other solver profiles trusted CHR profile for explicitly admitted solver/normalization programs preservation/structural query only for unsupported quantified semantics ``` Do not use an LLM to choose among strategies when deterministic query/profile/theory metadata suffices. ### Outcome semantics Execution status must not collapse into logical truth: ```text true / explicit_false / unknown / conflicted != unsupported / resource_exhausted / backend_unavailable / stale ``` Timeout/resource exhaustion is never semantic false. ### Freshness and explanation Derived tables/materializations are rebuildable caches keyed to semantic/theory generations. Changes to assertions, theory mappings, bridges, rules or lifecycle status invalidate only dependent derived state where backend capability permits it. Successful material conclusions/action-relevant evidence should be able to carry a replayable derivation receipt referencing plan fingerprint, rules, premises, theory edges, solver receipts and semantic generation. This is architecture input only; exact default/negation/paraconsistent semantics remain owned by #394/#400 rather than being accidentally defined by the execution backend. Full design and sources are preserved in #398D.

nsaspy commented

2026-09-08 01:47:19 +00:00

Author

Owner

MACHINE-SPIRIT #400B canonical handoff — typed defeat/dependence semantics

Depth 3B adversarially stress-tested #400A and refined the reasoning contract. Strong additions for this issue:

distinguish rebut, undermine, undercut, and deterministic invalidate; undercutting an inference must not synthesize explicit negation of its conclusion;
treat preferences as typed, partial, scoped, provenance-bearing relations (rule priority, specificity, source policy, recency, etc.), with a named/versioned profile-specific composition/lifting policy; no raw clause order or universal numeric score;
support source/evidence dependence so copied/syndicated/LLM-summary echoes do not count as independent corroboration while their assertion episodes remain preserved;
reject unsupported self-bootstrap: support SCCs with no external seed cannot create ordinary strict warrant; default/negative cycles are handled by the chosen profile (e.g. WFS undefined, stable-model plurality/no-model, argumentation undecided);
reinstatement/cycle behavior is profile semantics, not canonical ledger mutation;
distinguish valid time from transaction/knowledge time for backdated corrections;
split query result into semantic acceptance (skeptically_warranted, credulously_warranted, rejected, undefined, undecided, profile_inconsistent) and evaluation completeness (complete, bounded_partial, resource_limited, solver_error, unsupported_query_class);
each profile must declare an explicit translation/admission contract for explicit/default negation, contradiction, attacks/defeats, preference lifting, cycles, skeptical/credulous semantics, and no-model/failure behavior.

Preferred refined substrate is ESG + Typed Defeat/Dependence Graph -> explicit profile translator -> profile-specific semantics -> warrant receipt.

Full research, alternatives, primary sources, 24 adversarial fixtures and unresolved questions are preserved on #400 in the Depth 3 / #400B comment. Do not freeze one universal priority/default semantics before #400C/#400D.

## MACHINE-SPIRIT #400B canonical handoff — typed defeat/dependence semantics Depth 3B adversarially stress-tested #400A and refined the reasoning contract. Strong additions for this issue: - distinguish **rebut**, **undermine**, **undercut**, and deterministic **invalidate**; undercutting an inference must not synthesize explicit negation of its conclusion; - treat preferences as **typed, partial, scoped, provenance-bearing relations** (rule priority, specificity, source policy, recency, etc.), with a named/versioned profile-specific composition/lifting policy; no raw clause order or universal numeric score; - support **source/evidence dependence** so copied/syndicated/LLM-summary echoes do not count as independent corroboration while their assertion episodes remain preserved; - reject unsupported self-bootstrap: support SCCs with no external seed cannot create ordinary strict warrant; default/negative cycles are handled by the chosen profile (e.g. WFS `undefined`, stable-model plurality/no-model, argumentation undecided); - reinstatement/cycle behavior is profile semantics, not canonical ledger mutation; - distinguish **valid time** from **transaction/knowledge time** for backdated corrections; - split query result into **semantic acceptance** (`skeptically_warranted`, `credulously_warranted`, `rejected`, `undefined`, `undecided`, `profile_inconsistent`) and **evaluation completeness** (`complete`, `bounded_partial`, `resource_limited`, `solver_error`, `unsupported_query_class`); - each profile must declare an explicit translation/admission contract for explicit/default negation, contradiction, attacks/defeats, preference lifting, cycles, skeptical/credulous semantics, and no-model/failure behavior. Preferred refined substrate is `ESG + Typed Defeat/Dependence Graph -> explicit profile translator -> profile-specific semantics -> warrant receipt`. Full research, alternatives, primary sources, 24 adversarial fixtures and unresolved questions are preserved on #400 in the `Depth 3 / #400B` comment. Do not freeze one universal priority/default semantics before #400C/#400D.

nsaspy commented

2026-09-08 01:47:19 +00:00

Author

Owner

MACHINE-SPIRIT #400C handoff — Epistemic Federation Fabric

Depth 3C requires cross-theory epistemics to preserve local semantics rather than flattening all contexts into one non-monotonic logic.

Add a trusted Epistemic Federation Fabric (EFF) above local ESG/profile evaluation:

local theory + local profile
        ↓
status-bearing ep_export
        ↓
typed/versioned ep_bridge
        ↓
recipient-local admission or federation query view

Required bridge/export semantics:

export proposition + local profile/version + support state + acceptance + evaluation completeness + model scope + assumptions + support/counterevidence + validity + dependence/source lineage + receipt;
bridge import modes distinguish at least evidence_only, skeptical_warrant_as_support, credulous_candidate, attributed_acceptance, revision_input, argument_import, and inert_reference;
local negation-as-failure/default absence never becomes explicit negative support across an open bridge. Any absence-sensitive translation requires an explicit closure contract over predicate/domain/context/time and compatible negation semantics;
ASP/stable-model plurality survives export: credulous != skeptical;
undefined, conflicted, no_model, resource_limited, and unsupported remain distinct;
local defaults/priorities stay namespaced unless a typed lifting/admission policy explicitly maps them;
rebut/undermine/undercut/invalidate preserve attack type across bridges; unsupported attack semantics yields noncomposable, never synthetic negation;
source/evidence dependence survives context boundaries so syndicated/LLM-summary echoes do not reset as independent evidence;
identity/ontology mappings are explicit provenance-bearing assumptions that may induce conflict and must be visible in the warrant receipt;
contradiction/no-equilibrium in one context is contained by default and does not poison unrelated theories;
federation queries require a named/versioned federation profile (federated_evidence, federated_skeptical, federated_credulous, federated_argumentation, optional bounded mcs_equilibrium, managed revision, etc.);
bridge compatibility may be exact_preserving, sound_but_incomplete, lossy_declared, status_only, noncomposable, or unknown_compatibility.

Classic Brewka/Eiter heterogeneous Multi-Context Systems are the main formal precedent; Machine Spirit deliberately keeps global equilibrium as an optional bounded profile rather than ambient memory semantics because a no-equilibrium context must not globally disable unrelated memory.

Cross-theory warrant must expose participating theories/profile versions, bridge closure/versions, local outcome vector, mapping/identity assumptions, source-dependence components, imports/loss, semantic acceptance and evaluation completeness.

Security invariant remains unchanged: semantic/epistemic import never transfers host capability/authority.

## MACHINE-SPIRIT #400C handoff — Epistemic Federation Fabric Depth 3C requires cross-theory epistemics to preserve local semantics rather than flattening all contexts into one non-monotonic logic. Add a trusted **Epistemic Federation Fabric (EFF)** above local ESG/profile evaluation: ```text local theory + local profile ↓ status-bearing ep_export ↓ typed/versioned ep_bridge ↓ recipient-local admission or federation query view ``` Required bridge/export semantics: - export proposition + local profile/version + support state + acceptance + evaluation completeness + model scope + assumptions + support/counterevidence + validity + dependence/source lineage + receipt; - bridge import modes distinguish at least `evidence_only`, `skeptical_warrant_as_support`, `credulous_candidate`, `attributed_acceptance`, `revision_input`, `argument_import`, and `inert_reference`; - **local negation-as-failure/default absence never becomes explicit negative support across an open bridge**. Any absence-sensitive translation requires an explicit closure contract over predicate/domain/context/time and compatible negation semantics; - ASP/stable-model plurality survives export: credulous != skeptical; - `undefined`, `conflicted`, `no_model`, `resource_limited`, and `unsupported` remain distinct; - local defaults/priorities stay namespaced unless a typed lifting/admission policy explicitly maps them; - rebut/undermine/undercut/invalidate preserve attack type across bridges; unsupported attack semantics yields `noncomposable`, never synthetic negation; - source/evidence dependence survives context boundaries so syndicated/LLM-summary echoes do not reset as independent evidence; - identity/ontology mappings are explicit provenance-bearing assumptions that may induce conflict and must be visible in the warrant receipt; - contradiction/no-equilibrium in one context is contained by default and does not poison unrelated theories; - federation queries require a named/versioned federation profile (`federated_evidence`, `federated_skeptical`, `federated_credulous`, `federated_argumentation`, optional bounded `mcs_equilibrium`, managed revision, etc.); - bridge compatibility may be `exact_preserving`, `sound_but_incomplete`, `lossy_declared`, `status_only`, `noncomposable`, or `unknown_compatibility`. Classic Brewka/Eiter heterogeneous Multi-Context Systems are the main formal precedent; Machine Spirit deliberately keeps global equilibrium as an optional bounded profile rather than ambient memory semantics because a no-equilibrium context must not globally disable unrelated memory. Cross-theory warrant must expose participating theories/profile versions, bridge closure/versions, local outcome vector, mapping/identity assumptions, source-dependence components, imports/loss, semantic acceptance and evaluation completeness. Security invariant remains unchanged: semantic/epistemic import never transfers host capability/authority.

nsaspy commented

2026-09-08 01:47:19 +00:00

Author

Owner

MACHINE-SPIRIT #400D canonical handoff — demand-driven interface-factored epistemic execution

Depth 3D completes the execution contract for ESG + Typed Defeat/Dependence + EFF.

Add an explicit Epistemic Query Plan (EQP) layer above the existing deductive-plan/runtime boundary. EQP is data executed by the one canonical runtime/scheduler; it is not a second scheduler.

Required execution semantics:

query/context/federation profile
        ↓
demand/relevance slice
        ↓
query-local bridge dependency graph
        ↓
SCC condensation DAG
        ↓
profile-specific projected local interface summaries
        ↓
acyclic delta propagation OR profile-specific SCC evaluation
        ↓
factorized interface alternatives / constraints
        ↓
semantic acceptance + evaluation completeness + replay receipt

Project interfaces, not full local worlds

Federation must normally reason over bridge-visible projected interface states. If multiple local WFS/ASP/argumentation states differ internally but export the same status-bearing interface for the selected query, they may be quotiented for federation. Do not enumerate a Cartesian product of full local models merely to discover identical exports.

Projected summaries must remain keyed by theory/profile/evidence frontier/context/interface/identity/dependence/bridge generations and retain a local receipt. Quotienting is federation-query-specific and must not erase local distinctions.

SCC-specific evaluators

acyclic evidence-only/monotone edges: topological delta propagation;
monotone finite cyclic SCC: least-fixed-point / semi-naive deltas;
WFS-compatible SCC: tabled/alternating fixed point, preserving undefined and residual conditions;
ASP/nonmonotonic equilibrium SCC: bounded interface search via compatible solver oracle/multi-shot solving; preserve zero/multiple models/equilibria;
grounded argumentation: deterministic fixed point; preferred/stable variants require explicit bounded search;
noncomposable SCC: return a diagnostic/partial result rather than inventing common semantics.

Incremental invalidation

Derived dependency indexes must track evidence/lifecycle -> local summaries -> bridge applications -> SCC results -> downstream query caches. Identity, dependence, mapping, closure-contract, bridge and profile version changes invalidate only consumers. If local recomputation produces the same projected interface digest, invalidation stops at that boundary.

Local backends may use SWI/XSB-style incremental tabling, multi-shot ASP/overgrounding, semi-naive Datalog, or profile-specific incremental machinery; do not fake one universal incremental algorithm.

Factorized alternatives

When alternatives genuinely cross a cyclic federation, use a shared AND/OR + guard/nogood/link graph (engine-neutral FECG) or a backend-specific compact representation. BDD/ZDD/d-DNNF/tree-decomposition techniques are optional optimizations, not canonical semantics. Plan cost should expose SCC size, bridge-interface width/treewidth/separators, projected state count, solver calls and hard CPU/memory/work ceilings.

Hard outcome/replay invariants

semantic acceptance != evaluation completeness
resource_limited != unknown/false
no_equilibrium != refuted
scheduler interleaving != semantic result

For the same canonical evidence/context/profile/bridge versions and budgets:

cold evaluation == warm-cache evaluation == cache-rebuilt evaluation
incremental evaluation == full from-scratch evaluation

where equality is semantic/receipt-normalized and nondeterministic backend internals are not mistaken for source truth.

All compiled-semantic #400 conformance fixtures must execute with zero provider/LLM calls. Solver exhaustion never triggers implicit LLM fallback.

Full D research, sources, alternatives, complexity analysis and 22 adversarial fixtures are preserved on #400.

## MACHINE-SPIRIT #400D canonical handoff — demand-driven interface-factored epistemic execution Depth 3D completes the execution contract for ESG + Typed Defeat/Dependence + EFF. Add an explicit **Epistemic Query Plan (EQP)** layer above the existing deductive-plan/runtime boundary. EQP is data executed by the one canonical runtime/scheduler; it is not a second scheduler. Required execution semantics: ```text query/context/federation profile ↓ demand/relevance slice ↓ query-local bridge dependency graph ↓ SCC condensation DAG ↓ profile-specific projected local interface summaries ↓ acyclic delta propagation OR profile-specific SCC evaluation ↓ factorized interface alternatives / constraints ↓ semantic acceptance + evaluation completeness + replay receipt ``` ### Project interfaces, not full local worlds Federation must normally reason over **bridge-visible projected interface states**. If multiple local WFS/ASP/argumentation states differ internally but export the same status-bearing interface for the selected query, they may be quotiented for federation. Do not enumerate a Cartesian product of full local models merely to discover identical exports. Projected summaries must remain keyed by theory/profile/evidence frontier/context/interface/identity/dependence/bridge generations and retain a local receipt. Quotienting is federation-query-specific and must not erase local distinctions. ### SCC-specific evaluators - acyclic evidence-only/monotone edges: topological delta propagation; - monotone finite cyclic SCC: least-fixed-point / semi-naive deltas; - WFS-compatible SCC: tabled/alternating fixed point, preserving `undefined` and residual conditions; - ASP/nonmonotonic equilibrium SCC: bounded interface search via compatible solver oracle/multi-shot solving; preserve zero/multiple models/equilibria; - grounded argumentation: deterministic fixed point; preferred/stable variants require explicit bounded search; - `noncomposable` SCC: return a diagnostic/partial result rather than inventing common semantics. ### Incremental invalidation Derived dependency indexes must track evidence/lifecycle -> local summaries -> bridge applications -> SCC results -> downstream query caches. Identity, dependence, mapping, closure-contract, bridge and profile version changes invalidate only consumers. **If local recomputation produces the same projected interface digest, invalidation stops at that boundary.** Local backends may use SWI/XSB-style incremental tabling, multi-shot ASP/overgrounding, semi-naive Datalog, or profile-specific incremental machinery; do not fake one universal incremental algorithm. ### Factorized alternatives When alternatives genuinely cross a cyclic federation, use a shared AND/OR + guard/nogood/link graph (engine-neutral FECG) or a backend-specific compact representation. BDD/ZDD/d-DNNF/tree-decomposition techniques are optional optimizations, not canonical semantics. Plan cost should expose SCC size, bridge-interface width/treewidth/separators, projected state count, solver calls and hard CPU/memory/work ceilings. ### Hard outcome/replay invariants ```text semantic acceptance != evaluation completeness resource_limited != unknown/false no_equilibrium != refuted scheduler interleaving != semantic result ``` For the same canonical evidence/context/profile/bridge versions and budgets: ```text cold evaluation == warm-cache evaluation == cache-rebuilt evaluation incremental evaluation == full from-scratch evaluation ``` where equality is semantic/receipt-normalized and nondeterministic backend internals are not mistaken for source truth. All compiled-semantic #400 conformance fixtures must execute with **zero provider/LLM calls**. Solver exhaustion never triggers implicit LLM fallback. Full D research, sources, alternatives, complexity analysis and 22 adversarial fixtures are preserved on #400.

nsaspy commented

2026-09-08 01:47:19 +00:00

Author

Owner

MACHINE-SPIRIT #402C boundary — CLFM below epistemic federation

Depth 5C does not add a second truth/warrant layer. CLFM provides #394/#400 with status-bearing durable observations:

which logical ledger/source origin?
which exact frontier/checkpoint/cut?
what causal predecessors?
replica/mirror/independent-source dependence?
what issuer/receipt/integrity status?
what local admission status?
what payload/redaction/replay status?

#394/EFF still decides epistemic support/warrant under the selected profile. Thus:

replica convergence != semantic agreement
valid receipt       != warranted proposition
remote unavailable  != refutation
storage fork        != arbitrary epistemic winner

Source-dependence accounting must collapse replica/mirror/multi-TS observation paths back to the underlying assertion origin where appropriate. Full CLFM design and fixtures: #402C.

### MACHINE-SPIRIT #402C boundary — CLFM below epistemic federation Depth 5C does not add a second truth/warrant layer. CLFM provides #394/#400 with status-bearing durable observations: ```text which logical ledger/source origin? which exact frontier/checkpoint/cut? what causal predecessors? replica/mirror/independent-source dependence? what issuer/receipt/integrity status? what local admission status? what payload/redaction/replay status? ``` #394/EFF still decides epistemic support/warrant under the selected profile. Thus: ```text replica convergence != semantic agreement valid receipt != warranted proposition remote unavailable != refutation storage fork != arbitrary epistemic winner ``` Source-dependence accounting must collapse replica/mirror/multi-TS observation paths back to the underlying assertion origin where appropriate. Full CLFM design and fixtures: #402C.

nsaspy commented

2026-09-08 01:47:19 +00:00

Author

Owner

#405C CONCORDAT-MS handoff

Cross-domain epistemic composition must preserve local theory/profile semantics rather than importing remote conclusions as ambient truth.

Hard rules:

foreign credulous != local skeptical warrant
foreign undefined != local explicit false
foreign conflict != local winner
foreign verifier/authentication != local warrant

Bridge support/status/justification with an explicit target-local appraisal/profile step. Global MCS/equilibrium reasoning remains a named bounded profile, not the default union of all memories. Missing bridge semantics, private provenance, no equilibrium, multiple equilibria and exhausted search stay typed outcomes.

Canonical detail + fixtures C8-C13: #405C.

## #405C CONCORDAT-MS handoff Cross-domain epistemic composition must preserve local theory/profile semantics rather than importing remote conclusions as ambient truth. Hard rules: ```text foreign credulous != local skeptical warrant foreign undefined != local explicit false foreign conflict != local winner foreign verifier/authentication != local warrant ``` Bridge support/status/justification with an explicit target-local appraisal/profile step. Global MCS/equilibrium reasoning remains a named bounded profile, not the default union of all memories. Missing bridge semantics, private provenance, no equilibrium, multiple equilibria and exhausted search stay typed outcomes. Canonical detail + fixtures C8-C13: #405C.

nsaspy referenced this issue

2026-09-08 01:47:23 +00:00

[semantic-eval] Cross-domain semantic conformance corpus and meaning-preservation / hallucination-loss metrics #403

nsaspy referenced this issue

2026-09-08 01:47:30 +00:00

[AUTO-RESEARCH][MACHINE-SPIRIT] Eight-depth × four-subpass design program for general symbolic intelligence #401

nsaspy referenced this issue

2026-09-08 01:47:46 +00:00

[MACHINE-SPIRIT 4/8] Procedural intelligence and expert systems: production rules, blackboards, HTN planning, CBR, diagnosis and repair #397

nsaspy referenced this issue

2026-09-08 01:47:46 +00:00

[MACHINE-SPIRIT 4/8] Procedural intelligence and expert systems: production rules, blackboards, HTN planning, CBR, diagnosis and repair #397