nsaspy/prolog-rlm

Fork 0

[semantic-ir] General semantic knowledge algebra v1: domain-neutral kernel, typing, modality, provenance, and extensions #406

New issue

Open

opened 2026-09-08 01:29:20 +00:00 by nsaspy · 9 comments

nsaspy commented

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

Owner

Parent: #388

Goal

Design and implement the immutable/versioned general semantic knowledge algebra / IR v1 used by the semantic compiler.

The IR must represent materially different kinds of knowledge without requiring one bespoke schema per domain and without embedding arbitrary executable Prolog.

Architecture

Use a small closed semantic kernel plus open typed domain vocabulary.

closed kernel constructors
        +
open concept/relation/type vocabulary as inert data
        ↓
normalized ground semantic records
        ↓
validated safe reasoning/lowering

Published IR versions are immutable. A semantic change creates a new version.

Kernel coverage

The v1 algebra must be able to represent and compose at least:

entities, identity, aliases, typing, part-whole and roles;
taxonomy, definitions, equivalence/distinction;
assertions, explicit negation and n-ary relations;
strict rules / implication with variables and conditions;
procedures, steps, goals, pre/postconditions, branches and recovery;
events, actions, states and state transitions;
temporal relations, intervals, recurrence and validity ranges;
causal, diagnostic, symptom, prevention and recovery relations;
quantitative knowledge, units, ranges, cardinality and constraints;
spatial relations;
normative/deontic modalities: required/permitted/forbidden/recommended;
goals, intentions, plans, preferences and priorities;
attributed claims, beliefs, denials and assumptions;
uncertainty, alternatives and confidence metadata;
defaults, exceptions and defeasible statements;
comparisons/rankings;
hypotheses, scenarios and counterfactual scope;
examples/cases/precedents;
provenance, trust class, scope, derivation and lifecycle meta-knowledge.

Semantic distinctions that MUST survive encoding

asserted(P) != source_claims(S,P)
not(P) != unknown(P)
strict_rule != default_rule
possible_cause != cause
recommended != required
historical(P,T) != current(P)
example(P) != universal_rule(P)
hypothesis(P) != asserted(P)
model_inferred(P) != explicitly_stated(P)
semantic_action(A) != executable_capability(A)

Ground IR

Prefer explicit IDs/references and normalized ground records over model-produced callable structures.

Conceptual shape only:

sem_entity(Id, Type, Meta).
sem_relation(Id, Predicate, Args, Qualifiers, Meta).
sem_rule(Id, Kind, HeadRef, BodyRefs, Qualifiers, Meta).
sem_event(Id, Kind, Participants, Time, Qualifiers, Meta).
sem_procedure(Id, Goal, Qualifiers, Meta).
sem_step(Id, Procedure, Order, ActionRef, Conditions, Meta).
sem_constraint(Id, Kind, Expression, Scope, Meta).
sem_modal(Id, Modality, PropositionRef, Context, Meta).
sem_provenance(Id, SourceRef, Span, Derivation, Meta).

Exact API/records should follow repository conventions after fixture-driven design.

Extension mechanism

Allow domains to add typed concepts/relations as data without core changes.

Need a validated mechanism for:

concept declaration
relation signature / arity
argument roles/types
subtyping
aliases
unit/dimension declarations
optional trusted semantic extension adapters

Unknown domain vocabulary remains inert symbolic data. It must not become a host predicate merely because its name matches one.

Quantification / variables

Define safe representations for:

constants;
variables;
universal/existential interpretation where supported;
quantifier scope;
cardinality;
anaphoric/entity references.

Avoid silently losing quantifiers such as every, some, no, exactly one, at least, at most.

Context and scope

Records must support explicit contextual scoping for:

time
source/speaker
hypothetical/scenario
namespace/domain
location
validity conditions
assumptions

Provenance fields

Every material semantic record must support linkage to:

source identity/hash;
exact span(s);
document/segment identity;
compiler/IR version;
extraction/derivation class;
explicit vs inferred status;
model/provider identity when applicable;
confidence/ambiguity;
parent semantic records for derived records.

Immutability and fingerprints

IR v1 definition has deterministic schema fingerprint;
same canonical record yields stable fingerprint;
changing meaning requires new schema version;
extension declarations are versioned/fingerprinted;
no semantic record is accepted under an unknown incompatible schema.

MACHINE-SPIRIT pass #398 research decision: proposition/assertion split + semantic profiles

Auto-Research #398 found that the kernel should not promise one universal reasoning semantics. The strongest precedent across RIF and OWL is a shared interchange/core vocabulary plus explicitly restricted dialects/profiles with different computational guarantees.

Adopt these additional v1 invariants:

Proposition identity is separate from assertion identity. The same abstract proposition may be asserted, denied, attributed, hypothesized or derived by multiple sources/contexts without duplicating or mutating the proposition itself.
N-ary relations are native internally. RDF/triples are an interoperability projection, not the mandatory canonical shape.
Quantified/composed semantics use a closed ground formula AST. Variables and connectives are represented as data constructors; domain relation names remain inert symbols.
Every theory/package declares one or more versioned semantic profiles/dialects. Representation does not imply local entailment or safe lowering.
Support levels are explicit: at minimum distinguish represented, validated, queryable/entailed, and safely_lowerable.
Profiles gate reasoning/lowering. Candidate standard profiles include a ground kernel, function-free Horn/Datalog-safe rules, temporal event semantics, interval constraints, trusted CLP(FD)/CLP(Q/R) constraints, procedural semantics, defeasible/default semantics, and a preservation-only quantified-FOL profile.
Events/change are first-class. Standardize event/fluent/change relations semantically equivalent to occurrence + initiates + terminates, with current/holds views allowed as rebuildable materializations.
Frames are views, not primitive executable semantics. Object/slot projections are useful ergonomically, but defaults/procedural attachments lower to explicit semantic records and never hidden callbacks.
Structural proposition fingerprints are distinct from source-specific assertion IDs. Fingerprints are scoped by the semantic vocabulary/schema version; cross-memory real-world identity remains explicit reversible knowledge downstream.
Unknown/open extension vocabulary cannot resolve by name to host predicates. A semantic symbol such as restart or delete remains data until a trusted host adapter separately maps it to a capability.

Conceptual preferred layering:

terms + versioned signatures
        ↓
first-class propositions / closed formula AST
        ↓
assertion + stance + context + provenance
        ↓
event/state/change objects where applicable
        ↓
explicit semantic profile(s)
        ↓
trusted profile-specific reasoner/lowerer
        ↓
materialized/query/export views

This decision is based on Machine Spirit pass #398. The full research, alternatives and sources are preserved in that issue and must remain design input rather than being silently collapsed into this summary.

MACHINE-SPIRIT #398B depth decision: contextual theories + scoped witnesses + justifications

A second, deeper pass over #398 stress-tested the IR against the actual intended source classes: historical LLM logs, Wikipedia/encyclopedia revisions, news with attributed/conflicting claims, manuals/policies, scientific prose, heterogeneous ontology versions and hypothetical scenarios.

The result is that proposition + assertion + profile is necessary but still insufficient. Adopt these further v1 requirements.

1. Context and theory are first-class semantic objects

A source assertion must live in an explicit context/theory rather than an implicit global union.

Distinguish:

source revision/context contains P
       !=
general world/domain theory asserts P

Use opaque context/theory IDs with normalized facets such as source, speaker, time, scenario, domain, jurisdiction or ontology version. Do not eagerly create a Cartesian product of context dimensions.

A context describes the semantic viewpoint/scope in which statements live. A theory identifies an inference set: assertions/rules/vocabulary/profiles/imports considered together. They may correspond closely but are not identical.

Conceptual forms:

sem_context(ContextId, Kind, Facets, ParentRefs, VocabularyVersion, Meta).
sem_theory(TheoryId, ContextId, ProfileRefs, ImportRefs, Meta).

2. Context/theory imports and bridge rules are explicit

Knowledge moves between source/microtheory/domain contexts only through explicit imports/bridges with provenance and status.

Conceptual form:

sem_bridge(BridgeId, FromTheory, ToTheory,
           PatternRef, ConditionsRef, SemanticsProfile,
           Status, Provenance).

Bridge rules may promote/map knowledge, but compiler/model-generated bridge proposals are inert until admitted by the trusted semantic-policy boundary. A semantic bridge still does not grant host execution authority.

RDF named graphs may be used as an export/storage projection, but RDF dataset semantics do not provide the canonical context semantics required here.

3. Existential witnesses are distinct from globally identified entities

Text frequently contains existential knowledge:

some sample expressed N
an official said P
every project has a maintainer

Represent unknown witnesses explicitly and scope them to the originating formula/assertion/derivation.

Conceptual form:

sem_witness(WitnessId,
            ScopeFormulaOrAssertion,
            TypeConstraintRefs,
            OriginRef,
            IdentityStatus).

Hard invariants:

an existential witness is not automatically a real/global entity ID;
witnesses from separate assertions are not assumed equal;
equality with a known entity is a separate provenance-bearing assertion/derivation;
existential reasoning is lowerable only under an explicitly admitted decidable/bounded profile (e.g. guarded/warded/acyclic existential rules) or remains preservation-only;
a witness can never grant capability/authority.

Add an existential_warded/equivalent candidate profile to the profile-design work; exact fragment selection follows implementation evaluation.

4. Justification/derivation structure is first-class

The representation must preserve why a derived conclusion follows without conflating derivation state with immutable source truth.

Conceptual form:

sem_justification(JustificationId,
                  ConclusionAssertion,
                  RuleRef,
                  PremiseAssertionRefs,
                  AssumptionRefs,
                  ContextId,
                  ProfileRef,
                  ProvenanceRef).

Alternative derivations are separate hyperedges. This enables explanation, dependency tracking, corroboration, truth-maintenance experiments, provenance algebra and VERIFY/Review expert evidence.

Do not require every expanded proof tree to be durable. The justification schema/dependency model is canonical, while ordinary intermediate proof/materialization nodes may be rebuildable caches. Durable promoted conclusions/actions should retain replayable derivation receipts.

5. Preserve support and refutation independently

The ledger must retain enough polarity/evidence structure to compute an information state equivalent to:

no support + no refutation -> neither / unknown
support + no refutation    -> supported
no support + refutation    -> refuted
support + refutation       -> both / conflicted

This is an information summary inspired by four-valued/paraconsistent KR, not a decision that every profile uses one universal four-valued consequence relation. Pass #400 owns the exact non-monotonic/paraconsistent/default semantics.

6. Separate five provenance classes

Preserve distinct, linkable provenance for:

immutable source/span provenance;
semantic interpretation/compiler provenance;
logical derivation/justification provenance;
append-only lifecycle provenance (supersession/retraction/conflict/corroboration);
runtime/execution verification evidence.

Do not flatten these into a single confidence or generic metadata blob.

A provenance-semiring/annotation algebra may be supported by selected profiles, but probability, confidence, trust, cost and provenance are not assumed to share one arithmetic.

7. Canonical semantic state and derived/materialized state are different layers

Canonical append-only semantic data may include:

source objects/spans
vocabulary/signatures
formulae/propositions
assertion episodes
contexts/theories/bridges
rules/procedures
existential witnesses
supersession/retraction/conflict events
materially promoted derivation receipts

Rebuildable derived state includes ordinary:

current-active indexes
Horn consequences
transitive closures
holds/current views
query caches
relevance indexes
intermediate proof structures

Incremental tabling/materialized-view machinery is an implementation strategy, not canonical truth. The API must permit invalidation/rebuild/replay from durable semantics.

8. Profile capability contracts become explicit

A semantic profile should declare at least:

accepted constructors
quantifier/variable restrictions
negation semantics
identity assumptions
context/world assumptions
supported query classes
decidability/complexity guarantees where known
trusted lowerer/reasoner
materialization strategy
incremental capabilities
explanation/provenance capability
compatibility/import rules

Expose capability levels equivalent to:

represented
schema_validated
profile_admitted
query_supported(QueryClass)
decidable_for(PackageClass, QueryClass)   % where known
lowerable(Target)
materializable
incremental_capability(...)
explainable(...)

Never infer stronger operational guarantees merely because a semantic package is representable.

9. Validation schema is separate from inference semantics

The write-once IR/schema/signature layer validates the shape/type of semantic records. Validation does not by itself entail the data or select a reasoner. SHACL-style shape validation is a useful interoperability precedent, but semantic inference profiles remain separate.

10. Revised preferred architecture

immutable source / exact spans
          ↓
versioned vocabulary + signatures
          ↓
term / formula algebra
          ↓
first-class proposition identity
          ↓
assertion episode
  stance / polarity / validity / source
          ↓
context + theory
  facets / imports / explicit bridges
          ↓
scoped existential witnesses
          ↓
justification / derivation hypergraph
          ↓
declared reasoning profiles
          ↓
trusted profile-specific reasoners
          ↓
rebuildable materialized/query/export views

This is now the canonical design direction to be attacked by #399-#405, not a claim that every downstream semantic decision is settled.

Acceptance

One normalized IR represents every knowledge class listed above.
A mixed passage can produce multiple linked semantic forms without flattening.
Strict rule/default/exception are distinguishable.
Claim attribution cannot become unqualified assertion accidentally.
Explicit negation cannot be confused with missing knowledge.
Temporal/hypothetical scopes do not leak into current-world assertions.
Numeric quantity/unit/cardinality survive round trip.
New biology and software vocabularies can be added without changing kernel code.
Unknown domain predicate cannot become executable host code.
Every record preserves provenance/derivation identity.
Proposition identity and assertion identity round-trip independently.
A package can be representable but explicitly non-lowerable under an unsupported profile.
The same proposition can have multiple source/context assertions without payload duplication or provenance loss.
Source context assertion and promoted/domain-theory assertion remain distinguishable.
Context/theory bridge use is explicit and provenance-bearing.
An existential statement round-trips without inventing a globally identified entity.
Existential witnesses remain scoped until explicit identity evidence links them.
A derived answer can expose justification/premise/rule/source paths.
Positive and negative evidence can coexist without destructive last-write-wins.
Canonical history can rebuild ordinary derived/current materializations.
v1 schema fingerprint is stable; incompatible mutation is rejected.

Non-goals

no giant fixed ontology of all human concepts;
no natural-language parsing in this issue;
no persistent memory store;
no arbitrary Prolog execution;
no promise that every representable semantic form is decidable or executable by one reasoner;
no final stable-model/well-founded/default/paraconsistent/belief-revision policy here (see Machine Spirit epistemics pass #400).

Refs #388 #376 #377 #93 #380 #397 #398 and downstream lost-rob0t/symbolic-memory#4/#6.

Parent: #388 ## Goal Design and implement the immutable/versioned **general semantic knowledge algebra / IR v1** used by the semantic compiler. The IR must represent materially different kinds of knowledge without requiring one bespoke schema per domain and without embedding arbitrary executable Prolog. ## Architecture Use a small closed semantic kernel plus open typed domain vocabulary. ```text closed kernel constructors + open concept/relation/type vocabulary as inert data ↓ normalized ground semantic records ↓ validated safe reasoning/lowering ``` Published IR versions are immutable. A semantic change creates a new version. ## Kernel coverage The v1 algebra must be able to represent and compose at least: - entities, identity, aliases, typing, part-whole and roles; - taxonomy, definitions, equivalence/distinction; - assertions, explicit negation and n-ary relations; - strict rules / implication with variables and conditions; - procedures, steps, goals, pre/postconditions, branches and recovery; - events, actions, states and state transitions; - temporal relations, intervals, recurrence and validity ranges; - causal, diagnostic, symptom, prevention and recovery relations; - quantitative knowledge, units, ranges, cardinality and constraints; - spatial relations; - normative/deontic modalities: required/permitted/forbidden/recommended; - goals, intentions, plans, preferences and priorities; - attributed claims, beliefs, denials and assumptions; - uncertainty, alternatives and confidence metadata; - defaults, exceptions and defeasible statements; - comparisons/rankings; - hypotheses, scenarios and counterfactual scope; - examples/cases/precedents; - provenance, trust class, scope, derivation and lifecycle meta-knowledge. ## Semantic distinctions that MUST survive encoding ```text asserted(P) != source_claims(S,P) not(P) != unknown(P) strict_rule != default_rule possible_cause != cause recommended != required historical(P,T) != current(P) example(P) != universal_rule(P) hypothesis(P) != asserted(P) model_inferred(P) != explicitly_stated(P) semantic_action(A) != executable_capability(A) ``` ## Ground IR Prefer explicit IDs/references and normalized ground records over model-produced callable structures. Conceptual shape only: ```prolog sem_entity(Id, Type, Meta). sem_relation(Id, Predicate, Args, Qualifiers, Meta). sem_rule(Id, Kind, HeadRef, BodyRefs, Qualifiers, Meta). sem_event(Id, Kind, Participants, Time, Qualifiers, Meta). sem_procedure(Id, Goal, Qualifiers, Meta). sem_step(Id, Procedure, Order, ActionRef, Conditions, Meta). sem_constraint(Id, Kind, Expression, Scope, Meta). sem_modal(Id, Modality, PropositionRef, Context, Meta). sem_provenance(Id, SourceRef, Span, Derivation, Meta). ``` Exact API/records should follow repository conventions after fixture-driven design. ## Extension mechanism Allow domains to add typed concepts/relations as data without core changes. Need a validated mechanism for: ```text concept declaration relation signature / arity argument roles/types subtyping aliases unit/dimension declarations optional trusted semantic extension adapters ``` Unknown domain vocabulary remains inert symbolic data. It must not become a host predicate merely because its name matches one. ## Quantification / variables Define safe representations for: - constants; - variables; - universal/existential interpretation where supported; - quantifier scope; - cardinality; - anaphoric/entity references. Avoid silently losing quantifiers such as `every`, `some`, `no`, `exactly one`, `at least`, `at most`. ## Context and scope Records must support explicit contextual scoping for: ```text time source/speaker hypothetical/scenario namespace/domain location validity conditions assumptions ``` ## Provenance fields Every material semantic record must support linkage to: - source identity/hash; - exact span(s); - document/segment identity; - compiler/IR version; - extraction/derivation class; - explicit vs inferred status; - model/provider identity when applicable; - confidence/ambiguity; - parent semantic records for derived records. ## Immutability and fingerprints - IR v1 definition has deterministic schema fingerprint; - same canonical record yields stable fingerprint; - changing meaning requires new schema version; - extension declarations are versioned/fingerprinted; - no semantic record is accepted under an unknown incompatible schema. ## MACHINE-SPIRIT pass #398 research decision: proposition/assertion split + semantic profiles Auto-Research #398 found that the kernel should **not promise one universal reasoning semantics**. The strongest precedent across RIF and OWL is a shared interchange/core vocabulary plus explicitly restricted dialects/profiles with different computational guarantees. Adopt these additional v1 invariants: 1. **Proposition identity is separate from assertion identity.** The same abstract proposition may be asserted, denied, attributed, hypothesized or derived by multiple sources/contexts without duplicating or mutating the proposition itself. 2. **N-ary relations are native internally.** RDF/triples are an interoperability projection, not the mandatory canonical shape. 3. **Quantified/composed semantics use a closed ground formula AST.** Variables and connectives are represented as data constructors; domain relation names remain inert symbols. 4. **Every theory/package declares one or more versioned semantic profiles/dialects.** Representation does not imply local entailment or safe lowering. 5. **Support levels are explicit:** at minimum distinguish `represented`, `validated`, `queryable/entailed`, and `safely_lowerable`. 6. **Profiles gate reasoning/lowering.** Candidate standard profiles include a ground kernel, function-free Horn/Datalog-safe rules, temporal event semantics, interval constraints, trusted CLP(FD)/CLP(Q/R) constraints, procedural semantics, defeasible/default semantics, and a preservation-only quantified-FOL profile. 7. **Events/change are first-class.** Standardize event/fluent/change relations semantically equivalent to occurrence + initiates + terminates, with current/holds views allowed as rebuildable materializations. 8. **Frames are views, not primitive executable semantics.** Object/slot projections are useful ergonomically, but defaults/procedural attachments lower to explicit semantic records and never hidden callbacks. 9. **Structural proposition fingerprints are distinct from source-specific assertion IDs.** Fingerprints are scoped by the semantic vocabulary/schema version; cross-memory real-world identity remains explicit reversible knowledge downstream. 10. **Unknown/open extension vocabulary cannot resolve by name to host predicates.** A semantic symbol such as `restart` or `delete` remains data until a trusted host adapter separately maps it to a capability. Conceptual preferred layering: ```text terms + versioned signatures ↓ first-class propositions / closed formula AST ↓ assertion + stance + context + provenance ↓ event/state/change objects where applicable ↓ explicit semantic profile(s) ↓ trusted profile-specific reasoner/lowerer ↓ materialized/query/export views ``` This decision is based on Machine Spirit pass #398. The full research, alternatives and sources are preserved in that issue and must remain design input rather than being silently collapsed into this summary. ## MACHINE-SPIRIT #398B depth decision: contextual theories + scoped witnesses + justifications A second, deeper pass over #398 stress-tested the IR against the actual intended source classes: historical LLM logs, Wikipedia/encyclopedia revisions, news with attributed/conflicting claims, manuals/policies, scientific prose, heterogeneous ontology versions and hypothetical scenarios. The result is that `proposition + assertion + profile` is necessary but still insufficient. Adopt these further v1 requirements. ### 1. Context and theory are first-class semantic objects A source assertion must live in an explicit context/theory rather than an implicit global union. Distinguish: ```text source revision/context contains P != general world/domain theory asserts P ``` Use opaque context/theory IDs with normalized facets such as source, speaker, time, scenario, domain, jurisdiction or ontology version. Do **not** eagerly create a Cartesian product of context dimensions. A `context` describes the semantic viewpoint/scope in which statements live. A `theory` identifies an inference set: assertions/rules/vocabulary/profiles/imports considered together. They may correspond closely but are not identical. Conceptual forms: ```prolog sem_context(ContextId, Kind, Facets, ParentRefs, VocabularyVersion, Meta). sem_theory(TheoryId, ContextId, ProfileRefs, ImportRefs, Meta). ``` ### 2. Context/theory imports and bridge rules are explicit Knowledge moves between source/microtheory/domain contexts only through explicit imports/bridges with provenance and status. Conceptual form: ```prolog sem_bridge(BridgeId, FromTheory, ToTheory, PatternRef, ConditionsRef, SemanticsProfile, Status, Provenance). ``` Bridge rules may promote/map knowledge, but compiler/model-generated bridge proposals are inert until admitted by the trusted semantic-policy boundary. A semantic bridge still does not grant host execution authority. RDF named graphs may be used as an export/storage projection, but RDF dataset semantics do not provide the canonical context semantics required here. ### 3. Existential witnesses are distinct from globally identified entities Text frequently contains existential knowledge: ```text some sample expressed N an official said P every project has a maintainer ``` Represent unknown witnesses explicitly and scope them to the originating formula/assertion/derivation. Conceptual form: ```prolog sem_witness(WitnessId, ScopeFormulaOrAssertion, TypeConstraintRefs, OriginRef, IdentityStatus). ``` Hard invariants: - an existential witness is not automatically a real/global entity ID; - witnesses from separate assertions are not assumed equal; - equality with a known entity is a separate provenance-bearing assertion/derivation; - existential reasoning is lowerable only under an explicitly admitted decidable/bounded profile (e.g. guarded/warded/acyclic existential rules) or remains preservation-only; - a witness can never grant capability/authority. Add an `existential_warded`/equivalent candidate profile to the profile-design work; exact fragment selection follows implementation evaluation. ### 4. Justification/derivation structure is first-class The representation must preserve *why* a derived conclusion follows without conflating derivation state with immutable source truth. Conceptual form: ```prolog sem_justification(JustificationId, ConclusionAssertion, RuleRef, PremiseAssertionRefs, AssumptionRefs, ContextId, ProfileRef, ProvenanceRef). ``` Alternative derivations are separate hyperedges. This enables explanation, dependency tracking, corroboration, truth-maintenance experiments, provenance algebra and VERIFY/Review expert evidence. Do not require every expanded proof tree to be durable. The **justification schema/dependency model is canonical**, while ordinary intermediate proof/materialization nodes may be rebuildable caches. Durable promoted conclusions/actions should retain replayable derivation receipts. ### 5. Preserve support and refutation independently The ledger must retain enough polarity/evidence structure to compute an information state equivalent to: ```text no support + no refutation -> neither / unknown support + no refutation -> supported no support + refutation -> refuted support + refutation -> both / conflicted ``` This is an information summary inspired by four-valued/paraconsistent KR, **not a decision that every profile uses one universal four-valued consequence relation**. Pass #400 owns the exact non-monotonic/paraconsistent/default semantics. ### 6. Separate five provenance classes Preserve distinct, linkable provenance for: 1. immutable source/span provenance; 2. semantic interpretation/compiler provenance; 3. logical derivation/justification provenance; 4. append-only lifecycle provenance (supersession/retraction/conflict/corroboration); 5. runtime/execution verification evidence. Do not flatten these into a single `confidence` or generic metadata blob. A provenance-semiring/annotation algebra may be supported by selected profiles, but probability, confidence, trust, cost and provenance are **not** assumed to share one arithmetic. ### 7. Canonical semantic state and derived/materialized state are different layers Canonical append-only semantic data may include: ```text source objects/spans vocabulary/signatures formulae/propositions assertion episodes contexts/theories/bridges rules/procedures existential witnesses supersession/retraction/conflict events materially promoted derivation receipts ``` Rebuildable derived state includes ordinary: ```text current-active indexes Horn consequences transitive closures holds/current views query caches relevance indexes intermediate proof structures ``` Incremental tabling/materialized-view machinery is an implementation strategy, not canonical truth. The API must permit invalidation/rebuild/replay from durable semantics. ### 8. Profile capability contracts become explicit A semantic profile should declare at least: ```text accepted constructors quantifier/variable restrictions negation semantics identity assumptions context/world assumptions supported query classes decidability/complexity guarantees where known trusted lowerer/reasoner materialization strategy incremental capabilities explanation/provenance capability compatibility/import rules ``` Expose capability levels equivalent to: ```text represented schema_validated profile_admitted query_supported(QueryClass) decidable_for(PackageClass, QueryClass) % where known lowerable(Target) materializable incremental_capability(...) explainable(...) ``` Never infer stronger operational guarantees merely because a semantic package is representable. ### 9. Validation schema is separate from inference semantics The write-once IR/schema/signature layer validates the shape/type of semantic records. Validation does not by itself entail the data or select a reasoner. SHACL-style shape validation is a useful interoperability precedent, but semantic inference profiles remain separate. ### 10. Revised preferred architecture ```text immutable source / exact spans ↓ versioned vocabulary + signatures ↓ term / formula algebra ↓ first-class proposition identity ↓ assertion episode stance / polarity / validity / source ↓ context + theory facets / imports / explicit bridges ↓ scoped existential witnesses ↓ justification / derivation hypergraph ↓ declared reasoning profiles ↓ trusted profile-specific reasoners ↓ rebuildable materialized/query/export views ``` This is now the canonical design direction to be attacked by #399-#405, not a claim that every downstream semantic decision is settled. ## Acceptance - [ ] One normalized IR represents every knowledge class listed above. - [ ] A mixed passage can produce multiple linked semantic forms without flattening. - [ ] Strict rule/default/exception are distinguishable. - [ ] Claim attribution cannot become unqualified assertion accidentally. - [ ] Explicit negation cannot be confused with missing knowledge. - [ ] Temporal/hypothetical scopes do not leak into current-world assertions. - [ ] Numeric quantity/unit/cardinality survive round trip. - [ ] New biology and software vocabularies can be added without changing kernel code. - [ ] Unknown domain predicate cannot become executable host code. - [ ] Every record preserves provenance/derivation identity. - [ ] Proposition identity and assertion identity round-trip independently. - [ ] A package can be representable but explicitly non-lowerable under an unsupported profile. - [ ] The same proposition can have multiple source/context assertions without payload duplication or provenance loss. - [ ] Source context assertion and promoted/domain-theory assertion remain distinguishable. - [ ] Context/theory bridge use is explicit and provenance-bearing. - [ ] An existential statement round-trips without inventing a globally identified entity. - [ ] Existential witnesses remain scoped until explicit identity evidence links them. - [ ] A derived answer can expose justification/premise/rule/source paths. - [ ] Positive and negative evidence can coexist without destructive last-write-wins. - [ ] Canonical history can rebuild ordinary derived/current materializations. - [ ] v1 schema fingerprint is stable; incompatible mutation is rejected. ## Non-goals - no giant fixed ontology of all human concepts; - no natural-language parsing in this issue; - no persistent memory store; - no arbitrary Prolog execution; - no promise that every representable semantic form is decidable or executable by one reasoner; - no final stable-model/well-founded/default/paraconsistent/belief-revision policy here (see Machine Spirit epistemics pass #400). Refs #388 #376 #377 #93 #380 #397 #398 and downstream `lost-rob0t/symbolic-memory#4/#6`.

nsaspy commented

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

Author

Owner

MACHINE-SPIRIT #398C/#398D canonical delta — theory composition + deductive plan plane

Depth-1 subpasses C/D add two implementation-significant requirements beyond #398A/B.

C: theory composition is typed, not generic `imports`

The semantic IR/theory layer should support:

first-class export signatures
versioned theory/vocabulary interfaces
typed theory edges
explicit symbol/ontology mappings
compatibility/query-preservation contracts
bounded query-specific theory composition

Recommended edge kinds/semantics include include, reference, translate, bridge, conservative_extension, query_preserve, project, and cross-domain link relations. Exact names are design/implementation details, but one undifferentiated imports/2 is insufficient.

A theory edge/mapping must retain provenance and status. Model/compiler-proposed mappings are inert until admitted for inference. Historical records remain tied to the original vocabulary/theory version.

This follows modular-KR evidence from E-connections / distributed DLs and conservative-extension/query-inseparability work: safe combination is contract- and application-dependent, not synonymous with set union.

D: add explicit three-plane separation

Canonical architecture must preserve:

1. CANONICAL SEMANTIC PLANE
   immutable/versioned semantic records and theory graph

2. DEDUCTIVE PLAN PLANE
   compiled query/theory slice, normalized safe rules,
   profile/back-end selection, demand transforms, solver nodes,
   dependency/freshness plan, plan fingerprint

3. DERIVED STATE PLANE
   tabled answers, materializations, current views, closures,
   caches and ordinary intermediate proof structures

Planes 2/3 are rebuildable and must never become semantic source-of-truth.

For admitted Horn/Datalog fragments, the design should support semi-naive materialization and query-demand transformation (e.g. Magic-Set-style planning) rather than either full closure or naive SLD as the only strategy. Tabled/incremental evaluation is another backend strategy; CLP/CHR-style profiles remain trusted solver profiles rather than arbitrary model-generated programs.

Additional v1 acceptance implications

Theory/module exports and mappings round-trip independently of assertions.
Query can be executed against a bounded composed theory graph without global union.
Unverified mapping cannot silently affect authoritative conclusions.
Compiled deductive plan has a stable fingerprint for fixed semantic generation/query/options.
Derived tables/materializations carry freshness/dependency generation and can be invalidated/rebuilt.
Logical false/unknown remains distinct from unsupported or resource_exhausted execution outcome.
A fully known Horn/constraint task can execute with provider/model disabled.

Full research, alternatives, sources and adversarial fixtures are preserved in #398 subpasses C/D and parent #397.

## MACHINE-SPIRIT #398C/#398D canonical delta — theory composition + deductive plan plane Depth-1 subpasses C/D add two implementation-significant requirements beyond #398A/B. ### C: theory composition is typed, not generic `imports` The semantic IR/theory layer should support: ```text first-class export signatures versioned theory/vocabulary interfaces typed theory edges explicit symbol/ontology mappings compatibility/query-preservation contracts bounded query-specific theory composition ``` Recommended edge kinds/semantics include `include`, `reference`, `translate`, `bridge`, `conservative_extension`, `query_preserve`, `project`, and cross-domain link relations. Exact names are design/implementation details, but **one undifferentiated `imports/2` is insufficient**. A theory edge/mapping must retain provenance and status. Model/compiler-proposed mappings are inert until admitted for inference. Historical records remain tied to the original vocabulary/theory version. This follows modular-KR evidence from E-connections / distributed DLs and conservative-extension/query-inseparability work: safe combination is contract- and application-dependent, not synonymous with set union. ### D: add explicit three-plane separation Canonical architecture must preserve: ```text 1. CANONICAL SEMANTIC PLANE immutable/versioned semantic records and theory graph 2. DEDUCTIVE PLAN PLANE compiled query/theory slice, normalized safe rules, profile/back-end selection, demand transforms, solver nodes, dependency/freshness plan, plan fingerprint 3. DERIVED STATE PLANE tabled answers, materializations, current views, closures, caches and ordinary intermediate proof structures ``` Planes 2/3 are rebuildable and must never become semantic source-of-truth. For admitted Horn/Datalog fragments, the design should support semi-naive materialization and query-demand transformation (e.g. Magic-Set-style planning) rather than either full closure or naive SLD as the only strategy. Tabled/incremental evaluation is another backend strategy; CLP/CHR-style profiles remain trusted solver profiles rather than arbitrary model-generated programs. ### Additional v1 acceptance implications - [ ] Theory/module exports and mappings round-trip independently of assertions. - [ ] Query can be executed against a bounded composed theory graph without global union. - [ ] Unverified mapping cannot silently affect authoritative conclusions. - [ ] Compiled deductive plan has a stable fingerprint for fixed semantic generation/query/options. - [ ] Derived tables/materializations carry freshness/dependency generation and can be invalidated/rebuilt. - [ ] Logical `false/unknown` remains distinct from `unsupported` or `resource_exhausted` execution outcome. - [ ] A fully known Horn/constraint task can execute with provider/model disabled. Full research, alternatives, sources and adversarial fixtures are preserved in #398 subpasses C/D and parent #397.

nsaspy commented

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

Author

Owner

MACHINE-SPIRIT #400C bridge-layer clarification

Depth 3C confirms that the existing semantic sem_bridge concept must not imply epistemic warrant transfer.

Keep two layers distinct:

semantic mapping/bridge
    maps proposition/formula/vocabulary/context meaning

Epistemic Federation Fabric bridge
    controls what local support/acceptance status may be admitted by another theory

A semantically exact proposition mapping can still be epistemically noncomposable because source and destination use incompatible negation/default/model/priority semantics. Conversely, a recipient may retain another theory's acceptance as attributed meta-knowledge without admitting the mapped proposition as a premise.

#400C therefore recommends that sem_bridge may reference an epistemic interoperability-contract ID, but the semantic IR itself must not manufacture or assume that contract. This preserves the #398 rule that representation/mapping != local entailment/lowering/warrant.

## MACHINE-SPIRIT #400C bridge-layer clarification Depth 3C confirms that the existing semantic `sem_bridge` concept must **not imply epistemic warrant transfer**. Keep two layers distinct: ```text semantic mapping/bridge maps proposition/formula/vocabulary/context meaning Epistemic Federation Fabric bridge controls what local support/acceptance status may be admitted by another theory ``` A semantically exact proposition mapping can still be epistemically noncomposable because source and destination use incompatible negation/default/model/priority semantics. Conversely, a recipient may retain another theory's acceptance as attributed meta-knowledge without admitting the mapped proposition as a premise. #400C therefore recommends that `sem_bridge` may reference an epistemic interoperability-contract ID, but the semantic IR itself must not manufacture or assume that contract. This preserves the #398 rule that representation/mapping != local entailment/lowering/warrant.

nsaspy commented

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

Author

Owner

Machine Spirit #401A procedural-IR handoff

Depth 4A recommends refining the existing general procedure/step/event/causal coverage with a procedural semantic profile that preserves these distinctions without creating arbitrary executable Prolog:

task / goal schema
procedure method
partial-order task network
primitive symbolic operator
control/applicability rule
case / precedent
diagnostic problem
execution/run receipt

Conceptual forms from the research include sem_task, sem_method, sem_task_network, sem_operator, sem_control_rule, sem_case, and a diagnostic-problem object reusing the existing causal/hypothesis/provenance kernel.

Hard IR distinction:

method knowledge
  != decomposition decision
  != plan graph instance
  != expert invocation
  != effect attempt
  != observed transition
  != VERIFY result

sem_operator predicted effects are planning expectations, not observations. sem_case is episodic evidence, not a universal rule. A semantic action/capability requirement remains inert until the trusted host mapping + ordinary authority/effect boundary admits execution.

Exact constructor normalization should follow fixture-driven #392 implementation rather than expanding the kernel mechanically. Full rationale and A1-A20 fixtures are on #401; #401B must attack contingent/open-world/temporal procedural semantics before Depth 4 is considered settled.

## Machine Spirit #401A procedural-IR handoff Depth 4A recommends refining the existing general `procedure/step/event/causal` coverage with a **procedural semantic profile** that preserves these distinctions without creating arbitrary executable Prolog: ```text task / goal schema procedure method partial-order task network primitive symbolic operator control/applicability rule case / precedent diagnostic problem execution/run receipt ``` Conceptual forms from the research include `sem_task`, `sem_method`, `sem_task_network`, `sem_operator`, `sem_control_rule`, `sem_case`, and a diagnostic-problem object reusing the existing causal/hypothesis/provenance kernel. Hard IR distinction: ```text method knowledge != decomposition decision != plan graph instance != expert invocation != effect attempt != observed transition != VERIFY result ``` `sem_operator` predicted effects are planning expectations, not observations. `sem_case` is episodic evidence, not a universal rule. A semantic action/capability requirement remains inert until the trusted host mapping + ordinary authority/effect boundary admits execution. Exact constructor normalization should follow fixture-driven #392 implementation rather than expanding the kernel mechanically. Full rationale and A1-A20 fixtures are on #401; #401B must attack contingent/open-world/temporal procedural semantics before Depth 4 is considered settled.

nsaspy commented

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

Author

Owner

Machine Spirit #401B procedural-profile refinement

Depth 4B requires the procedural semantic profile to preserve more than procedure + steps + pre/postconditions.

Required representable inert semantics:

condition kind:
  hard_guard | observation_gate | branch_guard |
  assumption | monitor_invariant | success_condition

epistemic requirement:
  warranted | explicitly_refuted | closed_world_absent |
  permitted_unknown | profile-specific

outcome alternatives:
  deterministic/nondeterministic outcome classes
  predicted effects remain distinct from observations

procedure guarantee:
  deterministic | weak | strong | strong_cyclic | best_effort
  + explicit fairness/environment assumptions

temporal/resource contracts:
  duration / deadline / window / during-invariant
  mutex / required concurrency
  capacity/calendar/lease requirements

repair provenance:
  execution-continuation repair
  plan-instance repair
  method reselection
  inert reusable-method defect/supersession candidate

Unknown/refuted/conflicted guard states come from explicit epistemic profiles; raw Prolog NAF must not become universal procedural falsehood. Semantic actions and branches remain inert and cannot self-bind to host capabilities. Full rationale/sources/fixtures: #401 Depth-4B.

## Machine Spirit #401B procedural-profile refinement Depth 4B requires the procedural semantic profile to preserve more than `procedure + steps + pre/postconditions`. Required representable inert semantics: ```text condition kind: hard_guard | observation_gate | branch_guard | assumption | monitor_invariant | success_condition epistemic requirement: warranted | explicitly_refuted | closed_world_absent | permitted_unknown | profile-specific outcome alternatives: deterministic/nondeterministic outcome classes predicted effects remain distinct from observations procedure guarantee: deterministic | weak | strong | strong_cyclic | best_effort + explicit fairness/environment assumptions temporal/resource contracts: duration / deadline / window / during-invariant mutex / required concurrency capacity/calendar/lease requirements repair provenance: execution-continuation repair plan-instance repair method reselection inert reusable-method defect/supersession candidate ``` Unknown/refuted/conflicted guard states come from explicit epistemic profiles; raw Prolog NAF must not become universal procedural falsehood. Semantic actions and branches remain inert and cannot self-bind to host capabilities. Full rationale/sources/fixtures: #401 Depth-4B.

nsaspy commented

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

Author

Owner

Machine Spirit #401C handoff — procedural interoperability IR

Depth 4C now requires the procedural IR to keep five distinct objects rather than flattening them into one generic procedure:

native procedural artifact + formalism/version
Procedural Semantic Contract (PSC)
typed procedure bridge/mapping + loss/guarantee receipt
trusted host action binding metadata
host-specific execution projection/receipt

Hard boundary:

semantic procedure/action identity != host binding != capability != authority != effect admission

Native HTN/HDDL, Golog/ConGolog, Behavior Tree, BPMN/workflow and PDDL2.1 semantics may share bridge-visible interfaces, but unsupported sensing, RUNNING, interrupt, compensation, temporal/resource, fairness or guarantee semantics must yield explicit loss/noncomposable state rather than disappear. Host bindings are trusted adapter/configuration facts and cannot be manufactured by semantic names. See #401 Depth-4C full PIFF/PSC research and C1-C28 fixtures. #401D will define executable/scaling details.

## Machine Spirit #401C handoff — procedural interoperability IR Depth 4C now requires the procedural IR to keep five distinct objects rather than flattening them into one generic `procedure`: ```text native procedural artifact + formalism/version Procedural Semantic Contract (PSC) typed procedure bridge/mapping + loss/guarantee receipt trusted host action binding metadata host-specific execution projection/receipt ``` Hard boundary: ```text semantic procedure/action identity != host binding != capability != authority != effect admission ``` Native HTN/HDDL, Golog/ConGolog, Behavior Tree, BPMN/workflow and PDDL2.1 semantics may share bridge-visible interfaces, but unsupported sensing, `RUNNING`, interrupt, compensation, temporal/resource, fairness or guarantee semantics must yield explicit loss/noncomposable state rather than disappear. Host bindings are trusted adapter/configuration facts and cannot be manufactured by semantic names. See #401 Depth-4C full PIFF/PSC research and C1-C28 fixtures. #401D will define executable/scaling details.

nsaspy commented

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

Author

Owner

MACHINE-SPIRIT #402C handoff — federation metadata remains inert semantic data

Depth 5C (#402C, CLFM) adds cross-ledger composition requirements but does not move physical federation into Prolog-RLM.

Where #392 represents persistent/federated references, preserve typed/versioned distinctions for logical ledger identity, authority domain, remote event/statement identity, per-ledger frontier/checkpoint, causal-edge evidence, federation-link/mapping generation, integrity/admission/redaction/replay status, and replica-vs-independent-source classification.

Hard semantic boundary:

remote issuer/principal != local authority
receipt/inclusion        != truth
cross-ledger timestamp   != causal edge
same fingerprint         != same assertion episode

Unknown remote schemas/extensions remain inert/opaque where necessary. symbolic-memory owns durable federation links/frontiers/import history; #392 owns only the safe semantic representation/bridge vocabulary needed by consumers. Full design: #402C.

### MACHINE-SPIRIT #402C handoff — federation metadata remains inert semantic data Depth 5C (`#402C`, CLFM) adds cross-ledger composition requirements but does **not** move physical federation into Prolog-RLM. Where #392 represents persistent/federated references, preserve typed/versioned distinctions for logical ledger identity, authority domain, remote event/statement identity, per-ledger frontier/checkpoint, causal-edge evidence, federation-link/mapping generation, integrity/admission/redaction/replay status, and replica-vs-independent-source classification. Hard semantic boundary: ```text remote issuer/principal != local authority receipt/inclusion != truth cross-ledger timestamp != causal edge same fingerprint != same assertion episode ``` Unknown remote schemas/extensions remain inert/opaque where necessary. symbolic-memory owns durable federation links/frontiers/import history; #392 owns only the safe semantic representation/bridge vocabulary needed by consumers. Full design: #402C.

nsaspy commented

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

Author

Owner

MACHINE-SPIRIT #404A handoff — learning meta-semantics

EPOCH requires the semantic algebra to preserve learning status/provenance without confusing induced knowledge with source assertion.

Representable semantic/meta distinctions must support the equivalent of:

experience episode
candidate learned rule/method/control policy
admitted learned rule/method/control policy
suspended/superseded learned object
promotion/evaluation receipt

A learned payload may reuse ordinary sem_rule / procedure / policy constructors, but its origin and lifecycle are separate meta-knowledge: learner/version, hypothesis/operationality profile, source experiences, assumptions, positives/negatives/counterexamples, evaluation cuts/fixtures and promotion policy/version. This does not make promotion itself a semantic entailment rule and never creates a host binding/capability.

Ref #404A EPOCH.

## MACHINE-SPIRIT #404A handoff — learning meta-semantics EPOCH requires the semantic algebra to preserve learning status/provenance without confusing induced knowledge with source assertion. Representable semantic/meta distinctions must support the equivalent of: ```text experience episode candidate learned rule/method/control policy admitted learned rule/method/control policy suspended/superseded learned object promotion/evaluation receipt ``` A learned payload may reuse ordinary `sem_rule` / procedure / policy constructors, but its **origin and lifecycle are separate meta-knowledge**: learner/version, hypothesis/operationality profile, source experiences, assumptions, positives/negatives/counterexamples, evaluation cuts/fixtures and promotion policy/version. This does not make promotion itself a semantic entailment rule and never creates a host binding/capability. Ref #404A EPOCH.

nsaspy commented

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

Author

Owner

Machine Spirit #404C handoff — portable learned objects are meta-knowledge, not portable truth

PACT-EPOCH adds a versioned Learning Artifact Contract (LAC) / attestation layer above the semantic kernel. The IR/meta-knowledge surface should be able to represent a learned object's kind, payload ref, learner contract, applicability assumptions, source environment, evidence-use roles, source promotion attestation, drift/calibration scope and transfer provenance without converting any of those into an unqualified world assertion.

Hard boundary:

source_admitted(rule) != target_admitted(rule)
signed_attestation    != semantic truth
learned confidence    != epistemic warrant

Unknown/foreign learner predicates remain inert data. Cross-domain bridge logic may preserve/weaken/invalidate a guarantee but may not strengthen it without target evidence. Full design/fixtures are in #404C.

## Machine Spirit #404C handoff — portable learned objects are meta-knowledge, not portable truth PACT-EPOCH adds a versioned **Learning Artifact Contract (LAC)** / attestation layer above the semantic kernel. The IR/meta-knowledge surface should be able to represent a learned object's kind, payload ref, learner contract, applicability assumptions, source environment, evidence-use roles, source promotion attestation, drift/calibration scope and transfer provenance **without converting any of those into an unqualified world assertion**. Hard boundary: ```text source_admitted(rule) != target_admitted(rule) signed_attestation != semantic truth learned confidence != epistemic warrant ``` Unknown/foreign learner predicates remain inert data. Cross-domain bridge logic may preserve/weaken/invalidate a guarantee but may not strengthen it without target evidence. Full design/fixtures are in #404C.

nsaspy commented

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

Author

Owner

#405C CONCORDAT-MS handoff

Depth 8C confirms #392's existing context/profile/bridge model and adds one hard interoperability constraint for downstream implementation/conformance:

common semantic IR != common entailment
bridge(A,B) != bridge(B,A)
translation cannot silently strengthen guarantees

Semantic bridges should remain source/target-profile-qualified and expose a preservation class (preserved|translated|weakened|conditional|unknown|noncomposable) plus exact mapping/version provenance. A strong bridge may claim satisfaction/consequence preservation only when its declared formal/fixture contract establishes it; otherwise retain loss/unknown.

Foreign identity mappings remain semantic hypotheses and never substitute for authenticated host principal/resource binding.

Canonical research: #405C issue comment. #405D must turn the relevant bridge classes into executable conformance ownership.

## #405C CONCORDAT-MS handoff Depth 8C confirms #392's existing context/profile/bridge model and adds one hard interoperability constraint for downstream implementation/conformance: ```text common semantic IR != common entailment bridge(A,B) != bridge(B,A) translation cannot silently strengthen guarantees ``` Semantic bridges should remain source/target-profile-qualified and expose a preservation class (`preserved|translated|weakened|conditional|unknown|noncomposable`) plus exact mapping/version provenance. A strong bridge may claim satisfaction/consequence preservation only when its declared formal/fixture contract establishes it; otherwise retain loss/unknown. Foreign identity mappings remain semantic hypotheses and never substitute for authenticated host principal/resource binding. Canonical research: #405C issue comment. #405D must turn the relevant bridge classes into executable conformance ownership.

No labels

No milestone

No project

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#406

No description provided.

Rows
Columns

[semantic-ir] General semantic knowledge algebra v1: domain-neutral kernel, typing, modality, provenance, and extensions #406

Goal

Architecture

Kernel coverage

Semantic distinctions that MUST survive encoding

Ground IR

Extension mechanism

Quantification / variables

Context and scope

Provenance fields

Immutability and fingerprints

MACHINE-SPIRIT pass #398 research decision: proposition/assertion split + semantic profiles

MACHINE-SPIRIT #398B depth decision: contextual theories + scoped witnesses + justifications

1. Context and theory are first-class semantic objects

2. Context/theory imports and bridge rules are explicit

3. Existential witnesses are distinct from globally identified entities

4. Justification/derivation structure is first-class

5. Preserve support and refutation independently

6. Separate five provenance classes

7. Canonical semantic state and derived/materialized state are different layers

8. Profile capability contracts become explicit

9. Validation schema is separate from inference semantics

10. Revised preferred architecture

Acceptance

Non-goals

MACHINE-SPIRIT #398C/#398D canonical delta — theory composition + deductive plan plane

C: theory composition is typed, not generic imports

D: add explicit three-plane separation

Additional v1 acceptance implications

MACHINE-SPIRIT #400C bridge-layer clarification

Machine Spirit #401A procedural-IR handoff

Machine Spirit #401B procedural-profile refinement

Machine Spirit #401C handoff — procedural interoperability IR

MACHINE-SPIRIT #402C handoff — federation metadata remains inert semantic data

MACHINE-SPIRIT #404A handoff — learning meta-semantics

Machine Spirit #404C handoff — portable learned objects are meta-knowledge, not portable truth

#405C CONCORDAT-MS handoff

C: theory composition is typed, not generic `imports`