[MACHINE-SPIRIT 1/8] Knowledge-representation foundations: logic, frames, DL/Datalog, events, typed open vocabularies #400
Labels
No labels
bug
documentation
duplicate
enhancement
good first issue
help wanted
invalid
question
wontfix
No milestone
No project
No assignees
1 participant
Notifications
Due date
No due date set.
Dependencies
No dependencies set.
Reference
nsaspy/prolog-rlm#400
Loading…
Add table
Add a link
Reference in a new issue
No description provided.
Delete branch "%!s()"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Parent: #397
Related: #388 #392
Downstream: lost-rob0t/symbolic-memory#4
Distinct research mandate
Study classical and modern knowledge-representation foundations as an independent design track: first-order/Horn/Datalog variants, frames/semantic networks, description logics/OWL-style modeling, conceptual graphs, event/state representations, typed feature structures, reification and provenance-aware knowledge graphs.
Required output
Do not optimize for NLP extraction in this pass; assume semantics are already available and ask how they should be represented.
Auto-Research pass 1/8 — knowledge-representation foundations
Scope / research questions
This pass intentionally ignores NLP extraction quality and asks a narrower question: assuming the semantics are already known, what symbolic substrate should Machine Spirit use so that arbitrary knowledge is representable, inspectable, efficiently reasoned over, safely lowered into Prolog, and extensible without one giant ontology?
Questions investigated:
Primary / authoritative sources inspected
What current #392 gets right
The existing design already makes several strong calls:
Those are correct and should survive.
Where #392 is currently too loose
The current conceptual forms (
sem_relation,sem_rule,sem_event,sem_modal, etc.) are semantic categories and storage constructors at the same time. That risks building an ever-growing list of special-case record types.The deeper issue is that the IR does not yet declare its logic profiles / entailment contracts. A record may contain universal variables, defaults, temporal qualification, modal attribution, or an OWL-like taxonomy, but a consumer cannot yet tell whether that package belongs to a tractable Horn fragment, a DL fragment, a temporal fragment, a constraint fragment, or a preservation-only fragment.
Without this, “general IR” can quietly become “arbitrary FOL plus Prolog implementation accidents.”
Candidate architecture A — proposition graph / RDF-1.2-inspired core
Everything important becomes a first-class proposition node plus assertion/context records.
Conceptually:
Rules/procedures are graphs over proposition nodes.
Strengths
Weaknesses
Decision: useful as persistence/interchange inspiration, insufficient as the whole semantic IR.
Candidate architecture B — Common-Logic-style universal formula AST
Represent arbitrary first-order formulas directly:
Context/provenance wraps formula IDs.
Strengths
Weaknesses
Decision: retain a formula AST as a preservation/interchange capability, but do not make unrestricted FOL the default execution semantics.
Candidate architecture C — layered semantic kernel + declared reasoning profiles (preferred)
Use a tiny common algebra, then attach an explicit semantic profile to each theory/package/record set. This follows the strongest lesson from RIF and OWL profiles: shared syntax/identity does not imply one universal reasoning semantics.
Layer 1 — terms and vocabulary
Open domain vocabulary is data. Signatures/typing are validated but never converted to host predicates by name.
Layer 2 — propositions as first-class values
N-ary relations are native. Proposition identity is separate from assertion. This directly adopts the useful RDF 1.2 distinction: a proposition can exist without being asserted, and multiple source/assertion objects may refer to the same proposition.
Layer 3 — sentence / logical structure
Use a closed ground AST:
Only closed constructors (
atom,and,or,explicit_not,implies,forall,exists, equality, comparison...) are allowed. Domain relation symbols insideatomremain inert.Layer 4 — assertion / stance / context envelope
Assertion identity is not proposition identity. This solves repeated sources, conflict, attribution, confidence and history cleanly.
Layer 5 — event/state/change vocabulary
Make events and fluents first-class semantic objects rather than only arbitrary relations:
Event-Calculus-style
occurs/initiates/terminatesshould be the canonical change vocabulary because it maps naturally onto append-only memory and supports late-arriving historical evidence. Allen interval relations can be an optional standard temporal vocabulary for interval reasoning.This does not require all world state to be recomputed through Event Calculus. Materialized
holds_at/current views may be caches downstream.Layer 6 — semantic profiles / dialects
Every theory/package declares what semantics it expects:
A package can compose several profiles only through explicit compatibility rules.
This gives
semantic_capability/2real teeth: the runtime can say represented != locally entailed != safely lowerable.Safe lowering boundary
Recommended contract:
Lower only if:
Example:
horn_safecan become internal generic indexed facts/rules;constraint_fdmay invoke validated CLP(FD);fol_preservemust not become arbitrarycall/1.Frames: projection, not primitive semantics
Minsky/F-logic-style frames are valuable for ergonomics:
But a frame should be a materialized/object-centered view over canonical proposition/assertion records. Defaults and procedural attachments inside frames should lower into explicit default/procedure records, never implicit callbacks. This preserves frame ergonomics without hidden execution semantics.
Capability matrix versus #392
sem_rulerepresented, notentailedComplexity / scaling implications
Epistemic / provenance implications
The most important change is proposition != assertion.
This structure makes contradiction, corroboration, supersession and model-vs-source provenance downstream operations over assertion objects instead of mutating the proposition itself.
PROV-O’s Entity/Activity/Agent model is a good interoperability vocabulary, but the internal provenance model should remain smaller and domain-neutral; map to PROV-O at export boundaries.
Safety / authority implications
shell,restart,delete, orcallremains a domain symbol.fol_preserveand unknown extension profiles are inert except for inspection/retrieval/export.Adversarial review
Attack: “One universal AST is cleaner”
It is cleaner syntactically but dangerously vague operationally. If everything can express everything, callers start assuming the Prolog runtime can reason soundly/terminatingly over everything. Profiles prevent that semantic lie.
Attack: “Just use RDF 1.2”
RDF 1.2 substantially improves statement-level metadata, but triple graphs still do not natively express the full scoped quantified/default/procedural semantics Machine Spirit needs. RDF should be an interchange projection, not the canonical internal model.
Attack: “Just use OWL”
OWL is excellent for ontology/class/property semantics, but procedures, event dynamics, defaults, arbitrary rules and attributed/conflicting claims are outside its core sweet spot. Even OWL itself uses profiles because expressiveness changes computational properties.
Attack: “Just use Prolog terms directly”
That collapses data and execution and makes persistence/versioning/security harder. The repo’s existing authority rules already reject this direction.
Attack: “Every record gets a unique proposition ID, easy”
Bad: semantically identical propositions from multiple sources would never corroborate. Proposition canonicalization needs deterministic structural fingerprints within a declared vocabulary/schema version, while assertion IDs remain source/run-specific. Cross-memory identity reconciliation must remain reversible downstream.
Attack: “Canonicalize everything globally”
Also bad: local symbols, time-varying names, hypothetical entities and versioned ontologies make global same-as unsafe. Canonicalization should be syntactic/structural; semantic identity links remain explicit knowledge.
Rejected alternatives
sem_record(Type, Payload, Meta)blob — easy persistence, terrible invariant enforcement and reasoning guarantees.Concrete recommendations to canonical issues
#392 — change required
Add these design invariants:
represented,validated,entailed/queryable, andsafely_lowerablesupport levels;#394 — later reasoning pass dependency
#394 should consume the profile/dialect declaration instead of implementing one global evaluator over every semantic constructor. Default/exception/paraconsistency semantics should be a distinct profile and not silently contaminate strict Horn inference.
symbolic-memory#4/#6
Persist proposition records and assertion/context/provenance records separately enough that many assertions may reference the same proposition. Current/history views operate over assertions, not by mutating proposition payloads. Materialized frame/current-state views remain rebuildable indexes.
symbolic-memory#10
Identity reconciliation should not rewrite proposition structural IDs. Entity same-as/likely-same-as/renaming remains explicit reversible semantic knowledge; proposition equivalence can be a separate derived relation.
Preferred design summary
Machine Spirit should not have one universal logic. It should have one universal symbolic interchange kernel with explicit, composable reasoning profiles.
The canonical substrate is:
That keeps arbitrary knowledge representable while making computational promises honest.
Unresolved questions to preserve for later passes
Pass conclusion
#398is design-complete from the KR-foundations perspective. It does not prove implementation or Machine Spirit acceptance. The next pass should be #399 semantic compilation and should treat this representation as a target contract to attack, not as unquestionable truth.Deepening pass #398B — contextual theories, existential knowledge, justification graphs, and reasoning contracts
This is an additional depth pass on completed Machine Spirit pass #398, not a new numbered pass. It does not consume #399. The first #398 pass established a strong base — proposition/assertion separation, a closed semantic kernel, open vocabularies, and explicit reasoning profiles — but it was still too representation-format centric. This pass asks the harder question:
Research questions
proposition + assertion + profileenough, or do contexts/theories/microtheories need to be first-class objects?Additional primary/authoritative research
Contexts and microtheories
McCarthy's key move is to make context itself a formal object and reason about propositions in a context rather than forcing all assertions into a single flat theory. Guha applied this direction to Cyc-style microtheories. This is directly relevant to Machine Spirit because source, time, scenario, speaker, ontology version and task frame are not cosmetic metadata — they change what a proposition means or whether it may be used.
Truth maintenance / assumptions / multiple contexts
A TMS records reasons for beliefs, not just conclusions. The ATMS goes further by associating conclusions with assumption sets; one important architectural consequence is that multiple mutually inconsistent solution/context sets can coexist rather than forcing destructive retraction/backtracking. Machine Spirit should not copy ATMS wholesale here — pass #400 owns epistemics/non-monotonic reasoning — but #398 must leave room for first-class justifications, assumptions and context-dependent support.
Four-valued/paraconsistent information states
Belnap's motivating problem is almost exactly the corpus-ingestion problem: a question-answering machine receives information from fallible sources and must not explode when both P and not-P are present. The useful information-state distinction is
true/support only,false/refutation only,both, andneither. I do not recommend making Belnap-Dunn logic the universal logic of Machine Spirit, but the canonical representation must make this information state computable without loss.Existential rules / unknown witnesses
Existential rules (
forall x: P(x) -> exists y: R(x,y)) are materially important for text-derived knowledge. A source may say “every project has a maintainer” without identifying one, or “an official said...” without identifying the official. Plain Datalog cannot express this faithfully. Datalog±/TGDs use labelled nulls/witnesses and syntactic restrictions such as guardedness/wardedness/acyclicity to regain decidability. Vadalog is important implementation evidence that this is not merely theoretical: Warded Datalog± targets tractable data complexity while allowing recursion and existentially introduced unknowns.Provenance as algebra / derivation structure
Semiring provenance demonstrates that derivation annotations can be composed algebraically: conjunction and alternative derivations can preserve how an answer depends on source tuples rather than reducing provenance to a string. Algebraic model counting/semiring programming show that similar algebraic abstraction can support probability, soft constraints and other inference tasks. This suggests Machine Spirit should preserve a generic derivation/support graph and leave quantitative interpretation to an explicit profile rather than hard-code one universal confidence arithmetic.
Non-monotonic logic-programming semantics and tabled execution
The representation must not silently identify Prolog negation-as-failure with semantic negation. Well-founded semantics is especially relevant because a tabled logic-programming engine can explicitly represent unknown rather than forcing two-valued answers. SWI's current incremental tabling can maintain dependencies across dynamic predicates by invalidating dependent tables after updates and lazily recomputing them. This is useful implementation evidence for making canonical knowledge immutable while treating derived tables as rebuildable state.
Current standards revisited
Two standards details strengthen this pass:
named graph = contextis not a sufficient canonical context semantics for Machine Spirit.Stress test against real Machine Spirit inputs
The architecture should survive all of these without special-case schema redesign.
A. LLM logs
Source:
There are several different semantic objects here:
possible_cause), not fact;The generalized rule must not masquerade as something explicitly stated by a trusted manual.
B. Wikipedia / encyclopedia text
Source:
Compiler output should initially mean:
not automatically:
A separate trusted source-promotion/context bridge policy may make P available in a general astronomy theory while preserving the original assertion/revision provenance.
C. News
Source:
Must preserve:
and must not assert
Pmerely because a sentence contains it.D. Manual / policy
Source:
Contains:
E. Scientific prose
Source:
The existential
some samplesmust not create a fake globally identified sample. The IR needs a scoped existential witness/variable and quantifier structure.These examples strongly argue that source context and semantic world context must be distinct first-class objects.
Candidate architecture D — flat global proposition graph + annotations
Extend the first pass's proposition graph and attach every qualifier as annotation.
Good
Fatal weakness
It conflates several fundamentally different things:
source_claims(P)andPbecome dangerously easy to mix. It also has no principled home for existential scope or bridge rules between theories.Reject as canonical architecture. Keep it only as an optimized projection.
Candidate architecture E — context/microtheory-first logic
Make every assertion belong to an explicit theory/context.
Conceptually:
Queries are evaluated against an explicit context closure, not an implicit union of the entire store.
Strengths
Weaknesses
Refinement
Do not create one context for every Cartesian combination of dimensions. Use an opaque context/theory ID plus normalized context facets and explicit parent/import/bridge links. Context composition is query-time/reasoner policy, not uncontrolled object multiplication.
Strongly adopt as part of preferred design.
Candidate architecture F — existential-rule / deductive-database core
Make the executable kernel primarily a Datalog±-style theory:
Reasoning creates scoped labelled nulls/witnesses rather than invented real-world IDs.
Strengths
Weaknesses
Recommendation
Add a guarded/warded existential semantic profile rather than make existential Datalog the universal IR.
Required invariant:
Witness IDs are scoped to a formula/assertion/derivation context and carry constraints/provenance. Identity reconciliation may later conclude that a witness equals a known entity, but that is new append-only knowledge, not mutation of the original existential statement.
Candidate architecture G — justification/support graph as canonical reasoning substrate
Represent not only facts and rules but the proof/support dependency graph:
Alternative justifications are separate hyperedges.
Strengths
Weaknesses
Recommendation
Make the justification schema canonical, but treat many derived justification instances/materializations as rebuildable/indexed derived state. Preserve durable derivation receipts for material promoted conclusions/actions and externally visible explanations; allow low-value intermediate derivations to remain cacheable.
Strongly adopt as part of preferred design.
Candidate architecture H — universal weighted/algebraic logic
Use a generic logic theory plus an annotation semiring so provenance, probability, cost, confidence and optimization are all instances of one algebra.
Strengths
Weaknesses
Recommendation
Preserve an optional versioned annotation-algebra interface, but do not make a universal semiring mandatory in IR v1. Provenance should have a structured derivation representation first; probabilistic/soft profiles may interpret annotations separately.
Preferred #398B architecture — Contextual Theory Graph + Formula Algebra + Justification Hypergraph
The first pass's layered-profile architecture survives, but needs two new first-class layers and one major quantifier refinement.
Proposed normalized kernel direction
Conceptual only; exact names remain a design/implementation decision.
Why a first-class
theoryin addition tocontext?A context says where/from whose viewpoint/under which assumptions a semantic statement lives. A theory says which assertions/rules/vocabulary/profile set are considered together for inference.
Often one maps closely to the other, but they are not identical. Example:
This separation prevents a source document from becoming an executable global theory merely because it was parsed successfully.
Bridge rules are security-sensitive semantic infrastructure
Context/theory lifting must be explicit:
A bridge can express policies such as:
Bridge rules themselves are trusted configuration / validated symbolic policy, not arbitrary model-generated active code. A model may propose a bridge candidate; activation requires the appropriate trusted boundary.
This is semantic trust management, not host execution authority.
Query semantics: evidence state should be computable without flattening
The core ledger need not adopt one universal paraconsistent logic, but a default query result should be able to distinguish support and refutation independently:
This is Belnap-inspired information status, not necessarily the final consequence relation for every profile.
Why this belongs in the representation pass: if positive and negative source assertions have already been collapsed or one overwrote the other, pass #400 cannot recover the information later.
The query result should additionally retain:
Existential semantics — important addition to #392
The current #392 mentions existential quantification but does not yet say enough about witness identity.
Required invariants:
Example:
may justify:
but not:
without additional identity evidence.
This matters constantly in news, reports and scientific prose.
Provenance design — separate five notions that are easy to conflate
Machine Spirit needs at least:
All five can point into a shared graph, but they must remain distinguishable.
For derivation provenance, use a hash-consed DAG/hypergraph representation rather than duplicating proof trees into every assertion. Provenance-semiring style annotations can be computed over that graph for supported profiles.
Avoid eagerly expanding polynomial provenance expressions for highly recursive derivations. Keep canonical dependency nodes and compute bounded human explanations on demand.
Materialization / truth maintenance architecture
Canonical durable knowledge should remain append-only; derived current truth should not.
Recommended separation:
When canonical inputs change, dependency metadata invalidates affected derived tables/materializations. SWI incremental tabling provides one available implementation primitive today, although its documented strategy may invalidate and lazily recompute entire dependent tables rather than perform perfect delta maintenance. Therefore the public architecture should not depend on one Prolog engine's exact cache behavior.
This reconciles append-only history with efficient mutable runtime state.
Reasoning-profile refinement
The first pass introduced profiles. This pass suggests a more precise profile capability contract.
A profile should declare:
Support status should be more explicit than
represented/queryable/lowerable:A package should never imply stronger guarantees than its declared profile proves.
Suggested standard profile family after #398B
contextual_theorymay ultimately be a kernel capability rather than a separate profile; implementation research should decide after #400/#402.Performance / scale implications
1. Do not query one universal union graph
At millions/billions of records, every task should compile to:
This naturally aligns with #381 retrieval/projection.
2. Ground + Horn remains the hot path
Function-free Horn/Datalog should be the principal zero-LLM reasoning workhorse. Semi-naive evaluation, tabling and specialized relational representations are mature. Soufflé demonstrates that Datalog can handle large real-world analyses with compiled/specialized execution, and XSB/SWI provide tabled logic-programming paths.
3. Existential reasoning must be opt-in
General Datalog with existential heads is undecidable. Use warded/guarded/acyclic fragments and bounded chase/query-directed methods. Vadalog is strong evidence for Warded Datalog± as a serious candidate profile, not necessarily a dependency.
4. Context closure must be bounded
Recursive imports/bridges need cycle detection, memoization and explicit selection. Do not automatically union all ancestor microtheories.
5. Provenance can dominate storage
A conclusion can have combinatorially many derivations. Persist compact shared dependency structure and bounded material explanations; do not persist a complete expanded proof tree for every answer.
6. Specialized reasoners should be legal
The semantic IR is an interchange/control plane. A query may dispatch to:
provided the profile mapping is trusted and semantics-preserving for the admitted subset.
Prolog-RLMowns the semantic contract, not necessarily every low-level solver algorithm.Adversarial review
Attack 1: contexts become an ontology-management nightmare
Correct risk. A system that creates a unique full context for every source × time × speaker × scenario × ontology version will explode.
Countermeasure: contexts have stable opaque identity plus facets; theory membership/imports/bridges are sparse explicit relations. Query context composition is computed, not eagerly cross-product materialized.
Attack 2: bridge rules are just hidden trust heuristics
They can be. Therefore bridge provenance/status must be explicit and inspectable, and compiler/model proposals cannot auto-activate trusted bridges.
Attack 3: proposition canonicalization breaks intensional meaning
Two syntactically similar formulas can differ by context, vocabulary version, quantifier binding or concept identity.
Countermeasure: proposition structural fingerprints are scoped to canonicalized formula + exact vocabulary/signature version. Assertion/context identity remains separate. Cross-vocabulary equivalence is explicit knowledge, never fingerprint magic.
Attack 4: existential witnesses pollute entity reconciliation
Very real. A labelled null is not an entity assertion.
Countermeasure: use a distinct
witnesssemantic kind with scope/origin; reconciliation may link it later but cannot silently rewrite it into a global entity.Attack 5: justification graph becomes larger than the KB
Likely for recursive rules.
Countermeasure: shared DAG/hyperedges, derivation-class retention policy, on-demand explanation, and derived-cache eviction. Durable source assertions remain enough to replay/rederive.
Attack 6: four-valued status conflicts with stable/well-founded/default semantics
It can if treated as the universal logic.
Countermeasure: use support/refutation pair as a query information summary over assertion evidence, while each reasoning profile defines its own consequence semantics. Pass #400 decides default/nonmonotonic semantics.
Attack 7: too many reasoning profiles fragment the system
Also real.
Countermeasure: profiles form a small versioned registry with explicit capability/compatibility declarations. Prefer a handful of standardized profiles; unknown domain vocabulary should not require a new profile. Profiles vary semantics, vocabularies vary domain concepts.
Attack 8: arbitrary web/LLM text can create rules that later execute
Still forbidden.
A model can generate candidate semantic data. Validation can admit it as knowledge. Only separately trusted expert/tool/capability mapping can cause host effects.
Concrete canonical changes recommended
Update #392 semantic IR
Add explicit requirements for:
contextandtheoryidentities;neither/supported/refuted/bothinformation states;Downstream symbolic-memory #4/#6
Storage must preserve
context/theory/witness/justificationrecords and must not flatten them into generic triples. Current views should be theory/context aware and derived materializations must be explicitly rebuildable.Pass #400 boundary
Do not prematurely settle:
#398B only ensures the representation does not destroy the information those later semantics need.
Revised north-star representation test
Compile a corpus containing all of:
With the original prose removed from reasoning context, the IR/world-model must be able to answer:
Every answer must return theory/context, profile, supporting/refuting assertion IDs and exact source/derivation provenance.
#398B conclusion
The original preferred design remains valid but is incomplete. Machine Spirit should be designed as a contextual theory system, not a flat knowledge graph.
The refined core is:
That combination is substantially better suited to the user's actual intended ingestion domain — arbitrary LLM logs, web/news/encyclopedia text, manuals and research — because it distinguishes meaning, who/what said it, under what assumptions/world/time it applies, what is still unknown, and why a derived conclusion follows.
The next numbered pass remains #399 semantic compilation from language. It should now target this richer context/theory/witness/justification IR and actively test whether language compilation can populate it without losing attribution, quantification, discourse scope or procedural semantics.
Deepening pass #398C — modular heterogeneous theories, conservative imports, logic composition, and ontology boundaries
This is subpass C of four for Machine Spirit depth 1 (#398). A/B established the semantic kernel, proposition/assertion split, first-class contexts/theories, scoped witnesses, justification hypergraphs, and explicit reasoning profiles. This pass attacks a remaining hidden assumption: that one world model can be safely treated as a single theory with a shared vocabulary and a single import operation.
For the intended inputs — LLM logs, Wikipedia revisions, news sources, scientific literature, manuals, policies, project-specific knowledge, historical schemas, and domain ontologies — that assumption is false. Machine Spirit must support many partially overlapping theories whose domains, identities, vocabularies, and consequence relations need not coincide.
Research questions
Primary / authoritative sources inspected
Core finding
importis too vague to be a primitive. Machine Spirit needs a typed theory composition algebra where every edge declares what semantic promise it makes.A source-context theory, an ontology module, a rule module, and a constraint solver profile should not all be connected by one
imports/2relation.Recommended canonical distinction:
These are semantic contracts, not filesystem-module mechanisms.
Candidate architecture A — global merged theory
Normalize all accepted records into one canonical vocabulary and let profile tags distinguish semantics.
Advantages: easiest querying; simple index; straightforward cross-source joins.
Failure: identity and ontology boundaries become accidental. Adding a new ontology/rule set can alter conclusions everywhere. Conflicting closed-world/open-world assumptions leak. Imported defaults interact globally. Version replay becomes fragile. This is acceptable only as a materialized query view, never canonical semantics.
Reject as canonical design.
Candidate architecture B — fully isolated microtheories with arbitrary bridges
Every source/domain/profile is a separate theory. Cross-theory reasoning occurs only through model/compiler-proposed bridge rules.
Advantages: strong isolation; easy provenance.
Failure: knowledge becomes fragmented; bridge explosion; model-generated mappings become hidden semantic authority; no contract that a bridge preserves meaning or queries.
Reject in this unrestricted form.
Candidate architecture C — typed theory graph + declared interfaces (preferred)
Represent theories/modules as first-class objects with explicit signatures, profile contracts and typed composition edges.
Conceptual API/data:
Where
Kindis closed/versioned and can represent the contracts above.Export signatures are first-class
A theory should declare an interface:
Internal symbols/rules need not be globally addressable. This makes a theory closer to a module with a semantic API.
Mappings are data, not predicate aliases
Do not rewrite source records. A mapping is reversible provenance-bearing knowledge.
Theory edges carry proof obligations
A composition edge can declare:
A model/compiler may propose an edge, but trusted admission determines whether it can participate in automatic inference. Unverified mappings remain searchable evidence.
Logic combination lesson from E-connections
Do not attempt unrestricted cross-profile formula nesting as the default composition mechanism.
Prefer link relations between theories/domains:
A temporal solver can reason about the lifespan object; a taxonomic reasoner can reason about the person; a declared bridge moves only the required result between them.
This avoids turning
Horn × temporal × spatial × modal × constraint × defeasibleinto one giant undecidable logic.Conservative change / ontology evolution
The append-only model needs more than schema version numbers. For each new theory/vocabulary version, allow a conformance test expressing the intended compatibility contract.
Conceptual forms:
If no proof/test exists, compatibility status is
unverified; never infer that a newer ontology is backwards-compatible merely because its version number increased.This directly supports historical LLM/web ingestion: old interpretations stay tied to the vocabulary/theory version under which they were compiled.
Query projections should be semantic modules
A bounded projection for an expert/model should itself declare:
Thus projection is not “top-K facts”; it is a replayable query-specific module.
Validation versus entailment
SHACL reinforces an important boundary: structural/schema validation must remain separate from semantic entailment.
For Machine Spirit:
are distinct gates.
A record may be structurally valid but belong to a theory that cannot legally import into the current query environment.
Complexity / scaling
Epistemic / provenance consequences
A conclusion derived across modules needs a justification path containing:
A result can therefore say not only “source A supports P,” but “P follows only if ontology mapping M and bridge B are accepted.”
That is essential when an LLM-derived ontology alignment is uncertain.
Safety consequences
permitted(delete_file)remains epistemic data.Adversarial cases / required fixtures
ownerdifferently; naive merge yields false equivalence. Typed mapping must preserve distinction.Canonical recommendations
semantic_projection/4should return a replayable query module/receipt, not an untyped list of relevant facts.equivalent,narrower,broader,overlap,different) with theory/signature scope rather than globalsame_asshortcuts.Rejected alternatives
Depth-1 delta
A/B gave Machine Spirit
proposition → assertion → context/theory → justification → profile.C makes the theory layer modular and compositional:
The world model is therefore a network of theories with explicit semantic contracts, not one enormous global Prolog database.
This subpass intentionally does not decide truth revision/default logic (#400) or long-term persistence engine details (#402).
Deepening pass #398D — deductive execution substrate: Datalog compilation, demand transformation, incremental tabling, CHR/constraints, and derived-state architecture
This is subpass D of four for Machine Spirit depth 1 (#398). A/B/C now define a rich semantic object model and modular theory graph. D asks the operational question that decides whether any of this can become useful intelligence rather than archival semantics:
This pass stays at the KR/execution boundary. It does not choose non-monotonic truth semantics (#400), durable storage technology (#402), or symbolic attention/retrieval policy (#403). It defines the execution architecture those later passes can rely on.
Research questions
Primary / authoritative sources inspected
Core finding
The preferred architecture is not “lower semantic IR to Prolog clauses and query them.”
It is a three-plane system:
Only the first plane is semantic source-of-truth. The other two are rebuildable.
Candidate architecture A — direct Prolog lowering
Translate every admitted relation/rule to generated Prolog predicates and rely on normal SLD execution.
Strengths: simple prototype; excellent interactive ergonomics.
Failures:
Reject as canonical execution architecture. Trusted generated helper predicates may exist inside a compiled reasoner module, but never as the semantic model itself.
Candidate architecture B — pure bottom-up materialization
Compile every admissible Horn theory to Datalog and materialize its complete least fixpoint.
Strengths: deterministic; database-friendly; excellent for repeated broad queries; simple provenance/materialization semantics.
Failure: large heterogeneous KBs will derive enormous irrelevant closure. Temporal/event/identity relations may explode. Updating one base assertion can force costly recomputation without incremental dependency tracking.
Keep as one execution strategy, not the universal strategy.
Candidate architecture C — pure top-down tabled Prolog
Use tabled evaluation for all rule queries, memoizing answers.
Strengths: demand-driven; avoids irrelevant global closure; handles many recursive definitions elegantly.
Failure: less natural for broad reusable materializations, database-style joins, distributed/streaming updates, and bulk rule application; requires careful mapping of semantic update invalidation into table dependencies.
Keep as another strategy.
Candidate architecture D — profile compiler + hybrid demand/materialization engine (preferred)
The runtime compiles each admitted theory/query into an explicit deductive plan.
Conceptually:
DeductivePlanis inspectable data containing at minimum:No model is needed to execute an already-compiled symbolic plan.
1. Horn/Datalog as the primary zero-LLM workhorse
For function-free/range-restricted monotonic rules, compile to a Datalog-like normalized form.
Example semantic rule:
becomes internal rule data, not source clauses:
The compiler can then map that closed representation into a trusted generic Datalog evaluator or generated private reasoner code.
2. Semi-naive materialization
For repeated/broad queries, use delta fixpoint semantics:
This avoids recomputing old consequences at each recursive iteration.
Materializations are indexed by:
They are caches, never historical truth.
3. Magic/demand transformation
For narrow queries over large rule sets, transform evaluation so bottom-up reasoning follows top-down demand.
Example:
should not materialize
responsible_for/2for every entity in years of ingested logs.The plan records the demand transformation and its query binding pattern, making it reproducible/explainable.
This is one of the most important scaling ideas for Machine Spirit: symbolic attention can begin at the deductive compiler, before later retrieval/model projection.
4. Tabled evaluation for recursive/demand-heavy components
Use tabling where query-directed recursion is natural. On SWI, tabling already provides a mature primitive and incremental tabling provides dependency-driven invalidation.
Crucial abstraction:
Do not expose SWI's table identifiers as canonical knowledge IDs. They are an implementation detail of one backend.
5. Incremental invalidation
Every derived answer/materialization should depend on canonical semantic generations/edges.
When an assertion, theory mapping, bridge, rule, or lifecycle status changes:
SWI's Incremental Dependency Graph is direct evidence that this pattern is practical for tabled logic programming: updated dynamic predicates mark dependent tables invalid and re-evaluation occurs on demand.
The public contract should remain backend-neutral:
6. Constraint profiles are solver calls, not ordinary predicates
CLP(FD),CLP(Q/R), temporal interval constraints, unit/dimension constraints, etc. should compile into explicit trusted solver nodes.Example plan node:
Never turn an arbitrary semantic expression into a Prolog callable term.
7. CHR as a trusted extension profile, not the universal rule language
CHR is attractive for:
But CHR has operational semantics (simplification/propagation/simpagation) distinct from Horn entailment.
Therefore define an optional trusted
chr_constraintprofile whose programs/extensions are host-admitted/versioned. Do not compile arbitrary natural-language rules directly into unrestricted CHR.8. Validation compiles separately
Schema/shape checking should have its own validation plan:
Validation failures are evidence; they do not mutate the candidate or silently repair it.
A later repair/compiler pass may propose corrected IR.
9. Explanations piggyback on evaluation
Every successful derived result should optionally emit a compact derivation receipt:
Do not duplicate full proof trees when common subderivations exist. Store/reference a justification DAG/hypergraph.
For hot ephemeral queries the proof structure may remain transient; promoted conclusions and action-relevant VERIFY evidence should retain replayable receipts.
10. Derived state has typed freshness
A materialized fact needs status equivalent to:
No stale cached inference may silently masquerade as current truth.
Execution strategy selector
The compiler can use deterministic heuristics/profile metadata rather than an LLM:
The choice and reason are included in the plan receipt.
Query planning and cross-theory composition
Subpass C's theory graph is used before rule execution:
The runtime never unions the entire durable KB first.
Performance model / complexity honesty
Each semantic profile declares known complexity/termination properties where possible. The plan may reject or bound a query whose requested composition escapes supported guarantees.
Examples:
Do not turn a timeout into
unknown=false; reportresource_exhausted/unsupportedseparately from logical unknown.Machine Spirit scaling consequences
For millions of semantic records:
Safety / authority consequences
restart(service)can be reasoned about as data but cannot invoke a tool.Adversarial fixtures
shell/1; validator keeps it inert/unsupported.resource_exhausted, not semantic false/unknown.Canonical recommendations
semantic_projectionshould be able to consume/query a prepared symbolic plan and expose its bounded dependency/theory slice rather than selecting context only by heuristic relevance.successlabel.Rejected alternatives
Depth-1 final architecture after A/B/C/D
This completes the four-subpass KR-foundations depth. It is still design/research evidence, not Machine Spirit acceptance. #399 should now attack whether language can be compiled into this architecture with acceptable semantic fidelity.