Logic Cells: A Persistent Prolog Substrate for Governed Agents
Certified Rule Admission, Engine Tiers, and Suspended Inference with Governed Re-Entry
Abstract
Agent memory systems store; they do not reason. A vector store retrieves what is similar, a key-value store retrieves what is named, but neither can answer a question whose answer is entailed by what the agent knows and was never written down. The missing layer is inference over persistent facts, and the technology has existed for fifty years. What has not existed is a way to run it as multi-tenant infrastructure for agents: logic programs written by untrusted authors, persisting across sessions, and needing controlled access to the outside world mid-proof.
Logic Cells are persistent, namespaced Prolog environments provided as a platform primitive. Each is a world of typed facts and rules, backed by durable storage, that sleeps when idle and rehydrates on demand. Three mechanisms make them safe as shared infrastructure. Certified admission: every rule an agent asserts is statically analyzed (termination class, predicate surface, sandbox conformance) and receives a signed certificate before it may execute; queries chain their certificates to those of the rules they exercised, forming a provenance graph over reasoning itself. Engine tiers: a namespace runs on one of two Prolog engines, a full-featured default and a strictly ISO-conformant engine whose sandbox is stronger by construction, with a monotonic pinning discipline that rejects violations rather than degrading. Governed re-entry: the call_tool predicate family lets a proof suspend mid-inference, dispatch a platform tool through the full governance pipeline (credits, policy, audit), and resume with the result bound, so a proof can pull live data without leaving the governed path.
The result is symbolic memory with the properties agents need: zero-token queries over accumulated knowledge, rules as durable behavior, and a certificate or receipt for every step of admission and execution. And because an admitted rule can be served, its head parsed into an HTTP contract and its fact base rendered as an interface, a namespace is one object seen four ways: memory, reasoning, API, and interface.
Problem Landscape
Retrieval Is Not Reasoning
An agent that has recorded supplies(atlas, meridian) and depends_on(meridian, quartz) should be able to answer “who is exposed if quartz fails?” No retrieval system can, because the answer is not stored; it is derivable. Agents compensate by loading the facts into context and asking the model for the inference, at token cost and with sampling variance, every time. Logic programming derives deterministically, exhaustively, and at no token cost, provided the facts live somewhere an engine can reach.
Untrusted Authors
Once agents can write rules, the platform is executing tenant-authored programs. A rule can recurse without a base case, generate unboundedly, or reach predicates that touch the process, the file system, or other tenants. Prompt-level discipline does not help; admission must be decided by analysis of the rule itself, and the decision must be legible afterward: what was checked, what was found, why the rule was allowed to run.
Conformance Is a Security Boundary
Prolog implementations differ enormously in the built-in surface they expose. A full-featured engine’s sandbox must be maintained by enumeration, every dangerous built-in denied explicitly; a strictly ISO-conformant subset contains no shell, file, or process primitives, so the boundary holds by construction. For Logic Cells that back public-facing surfaces, that is the difference between a policy and a property.
Pure Logic Cannot Fetch
Reasoning over already-asserted facts hits a wall the moment a proof needs something live: a record from an integration, a numeric result, a search hit. Having the agent fetch first, assert, then query works but forfeits composition: the rule cannot decide what it needs. Letting inference call out re-raises every governance question the platform exists to answer: who pays, what policy applies, what gets audited, and what happens when the tool called is the engine executing the proof.
Design Principles
1. Facts Persist; Workers Are Cache
The durable representation is rows in encrypted storage, not a running process. Workers are ephemeral: a namespace wakes on first use, rehydrates, serves queries, and is reaped after idle timeout. Crash, deploy, and restart are non-events; the next query rehydrates.
2. Namespaces Are Worlds
Scope is user, gateway, and namespace, and each namespace resolves to its own worker process. Isolation is a process boundary, not a bookkeeping convention: compiled rules cannot leak between namespaces, and each chooses its engine independently. Namespaces are cheap enough to be organizational: one per project, per investigation, per application.
3. Rules Are Admitted, Not Accepted
Asserting a rule is a pipeline, not a write: validation, certificate minting, compilation into the live engine, verification that it loaded, and rollback if it did not. A rule that fails validation carries an explicitly untrusted certificate rather than a silently missing one.
4. Conformance Is Monotonic
A namespace pinned to the ISO engine stays pinned: unpinning, or asserting content that needs the richer engine, is rejected with reasons, never silently accommodated. The pin outranks every other engine-selection signal.
5. Tool Calls Go Through the Front Door
A tool call made from inside a proof traverses the same gateway pipeline as any agent-initiated call: credits, policy, audit, response shaping. There is no privileged side channel for internal calls. A rule is exactly as governed as its author.
The Logic Cell Model
A Logic Cell holds typed facts (entities, attributes, relations, metrics, with provenance and optional expiry) plus rules. The tool surface is plain: direct assertion (zero inference cost) and natural-language assertion (one translation call); querying by raw goal, by structured pattern, or by natural-language question; rule storage; reflection over contents; goal-directed context hydration under a token budget; export/import for portability; and tabulation of facts into flat records that the platform’s deterministic data tools consume directly.
The exposure query from the problem statement, answered by derivation:
% Two asserted facts, no stored answer.
supplies(atlas, meridian).
depends_on(meridian, quartz).
% One admitted rule.
exposed_to(Party, Input) :-
depends_on(Vendor, Input),
supplies(Party, Vendor).
?- exposed_to(Party, quartz).
Party = atlas.
The same knowledge is reachable by goal, by pattern, or by question:
# Structured pattern: name the relation, leave the rest unbound.
query_patterns(user, [%{"relation" => "depends_on", "object" => "quartz"}])
# Natural language, anchored to the cell's existing predicate vocabulary.
query(user, "who is exposed if quartz fails?")
Two details matter more than they look. Natural-language storing and querying are anchored to the same predicate vocabulary through embeddings over the existing facts, so the probabilistic bridge into and out of the symbolic store converges on one vocabulary instead of inventing synonyms on each side. And reflection is built for session starts: an agent’s first act can be to load a compact snapshot of everything its Logic Cell knows, at zero inference cost.
Certified Rule Admission
Every rule entering a Logic Cell is statically analyzed before compilation. The analysis produces:
- A termination class:
datalog(non-recursive over finite facts: termination guaranteed),well_founded(recursive, with a base case and a recognized decreasing pattern such as arithmetic on an argument, list decomposition, or a visited set),generator(may enumerate unboundedly; callers are advised to bound), orunbounded(no termination argument found; admitted with warnings, flagged for cycle-guard patterns). The classes are syntactic findings, not proofs, and the certificate labels them so:termination_basis: syntactic. Recursion is detected through the namespace’s other stored rules too, so a rule recursive only by way of a neighbor is classified as recursive - The predicate surface: every predicate the rule defines and every predicate its body can reach, found by walking the clause body’s full control structure
- A verified sandbox claim: the same walk asks, for each reachable goal, whether the query-time sandbox would permit it. Stored rules compile through a different path than ad-hoc queries, so without this check a certificate could assert conformance for a body the sandbox would never have allowed
The classifier reports what it found, and the certificate carries it:
rule: exposed_to/2
termination: datalog % non-recursive over finite facts
predicates: defines [exposed_to/2]
reaches [depends_on/2, supplies/2]
sandbox: conformant % every reachable goal permitted at query time
validated: true
The findings are minted into a signed certificate attached to the rule, the family described in Cognitive Trust Certificates: Verifiable Execution Proofs for Autonomous Systems, applied here to reasoning rather than workflow plans. Failed validation does not mint a weaker-looking success: the certificate states validated: false and warns against trust.
Queries close the loop. A query’s certificate records which stored rules the proof exercised (at runtime through predicate wrappers on the full engine; by static reachability over stored rules on the ISO engine, with the basis stated) and chains to their admission certificates. Any answer can be traced to the certified rules that produced it, and revoking a rule’s certificate identifies every conclusion built on it. Both certificates are persisted rows, not only fields in a response: a query certificate is kept for seven days like other per-run certificates, an admission certificate without expiry, so the viewer link on either resolves.
flowchart TB
subgraph A["admission of one rule"]
direction TB
r["rule text"] --> v["static validation<br/>termination class, predicate surface, sandbox conformance"]
v --> m["assertion certificate minted<br/>validated true or false"]
m --> c["compile into the live engine and persist"]
c --> k["verify the rule loaded"]
k -- "ok" --> s["stored rule<br/>carrying its certificate id"]
k -- "failed" --> b["rollback<br/>retract the persisted rule"]
end
subgraph Q["later, at query time"]
direction TB
q["query runs<br/>rules recorded at runtime on SWI,<br/>by static reachability on ISO"] --> qc["query certificate"]
end
qc -. "chains to the certificates<br/>of the rules the proof exercised" .-> s
Admission is a pipeline that ends in a certificate either way. A query certificate, minted later, chains back to the admission certificates of the stored rules the proof exercised, with the certificate stating whether that set was recorded or inferred.
Engine Tiers and the ISO Pin
A Logic Cell runs on one of two engines. SWI-Prolog is mature, fast, and feature-rich (dicts, aggregation, probabilistic extensions), with a sandbox maintained by explicit denial. Scryer Prolog executes a strictly ISO-conformant subset: no shell, no file system, no process control in the language, so the sandbox is structural. Both run as supervised operating-system processes, so a crash is a reaped worker and a rehydration, never a platform fault.
Selection is a small policy with a strict priority order. A namespace may be explicitly configured; otherwise, in automatic mode, it is placed by conformance analysis of its contents, and one that ever requires the richer engine is upgraded once, permanently, so placement cannot flap. Accounts with the ISO feature start fresh namespaces on the ISO engine in automatic mode. Above all of this sits the ISO pin: a pinned namespace is never upgraded and rejects any content that would need more, and the pin is checked before the stickiness signal, so an earlier upgrade cannot quietly bypass a later pin. Pinning is one-way, and the way out is not an unpin but a fork: a new namespace seeded from the pinned one’s facts and rules, choosing its own engine posture from the start. The pinned namespace keeps its guarantee for as long as it exists; the fork is where a different posture begins, and the two diverge from that point as separate worlds.
flowchart TB rule["rule arrives for a namespace"] --> pin["ISO pin set?"] pin -- "yes and the rule needs more than ISO" --> rej["rejected with reasons"] pin -- "yes and the rule is ISO" --> pinned["ISO engine<br/>the pin holds"] pin -- "no" --> cfg["engine explicitly configured?"] cfg -- "yes" --> use["use the configured engine"] cfg -- "no, automatic" --> sticky["already upgraded?"] sticky -- "yes" --> full["full engine, stays"] sticky -- "no" --> conf["conformance analysis<br/>of the rule text"] conf -- "ISO conformant" --> iso["ISO engine<br/>automatic, may upgrade later"] conf -- "needs the richer engine" --> up["upgrade once, permanently"]
Engine selection in priority order: the pin is consulted first and can only reject, so no later signal can route pinned content onto the richer engine.
The probabilistic case shows the posture. Probabilistic rule annotations natively require the richer engine, and the naive resolution would migrate the namespace and void the pin. Instead, annotated rules on pinned namespaces are rewritten into plain ISO form with a probabilistic inference battery installed alongside: notation, semantics, and the security property survive, at the cost of a specialized inference path. Guarantees are kept by doing more work, not by weakening the guarantee.
call_tool: Suspended Inference, Governed Re-Entry
The call_tool predicate family lets a proof invoke a platform tool mid-inference and continue with the result bound:
% The rule decides what it needs: a live rate the cell cannot derive, then
% ordinary Prolog arithmetic over the result.
smart_quote(Account, Weight, Quote) :-
contract_zone(Account, Zone),
call_tool('data-grout@1/store.get@1',
[collection-'rates', key-Zone], Record),
member(rate-Rate, Record),
Quote is Rate * Weight.
Note what is not delegated: the multiplication. Arithmetic, comparison, and
aggregation are native to the engine and cost nothing. call_tool exists for
what inference cannot reach on its own: live state and the platform’s
non-deterministic capabilities.
The two engines implement suspension differently (the richer engine yields from a first-class engine construct; the ISO engine round-trips through its host protocol), but both surface one dispatch policy and one result contract, so rules are portable across tiers.
Dispatch is a three-way decision. Inner queries against the same cell are inlined as sub-queries inside the running engine: no round-trip, no second worker, bounded depth. Calls that would need the worker executing the proof are refused with a structured, pattern-matchable term rather than a crash or a deadlock. Everything else goes through the full gateway pipeline, charged, policy-checked, and audited as if the agent had made the call directly. Recursion is depth-bounded; failures bind an error term the rule can handle; and the predicate is deterministic, so backtracking never re-fires a side effect.
flowchart TB p["proof reaches call_tool<br/>inside the running engine"] --> d["dispatch decision"] d -- "same cell, logic.query" --> i["inline sub-query<br/>no yield, depth bounded"] d -- "needs the worker running this proof" --> r["structured refusal<br/>bound as an error term"] d -- "anything else" --> y["suspend<br/>engine yields the tool call to the host"] y --> gw["gateway pipeline<br/>credits, policy, audit"] gw --> res["resume<br/>result bound as sorted Key-Value pairs"] i --> k["proof continues"] r --> k res --> k
The three-way dispatch: only the third branch suspends the engine, and it resumes with the result bound after the same governed path any agent call takes.
The Family
call_tool/3 is the primitive; four relatives cover the compositions that recur. All keep its contract: results arrive as sorted Key-Value pair lists that member/2 opens on either engine, failures bind a pattern-matchable marker rather than throwing across the engine boundary, and every dispatch is charged, policy-checked, and audited.
call_tool/4: the envelope as a second output. The four-argument form separates the payload from the platform’s response envelope (credits charged, cache reference, certificate) so a rule can read the cost and provenance of the call it just made: retry under a budget, or keep the certificate beside the conclusion it supports.
% Reasoning rules read Payload; cost and audit rules read Meta. This one reads
% both: take the quote only if the lookup stayed under budget, and keep the
% certificate beside the conclusion it supports.
quote_within_budget(Account, Weight, Quote, Cert) :-
contract_zone(Account, Zone),
call_tool('data-grout@1/store.get@1',
[collection-rates, key-Zone], Record, Meta),
memberchk(credits-Credits, Meta),
Credits =< 5,
memberchk(ctc-Cert, Meta),
member(rate-Rate, Record),
Quote is Rate * Weight.
call_ns/3,4: consult another world. A different namespace is a different worker, so a proof may hand a goal to one of the user’s other Logic Cells and await its solutions. Same-namespace calls are refused (they would wait on the worker running the proof) and chains are depth-bounded. Solutions come back as one binding list per answer, capped by the optional fourth argument:
% The supply-chain cell asks the incidents cell whether an exposed input is
% actually down. The error marker is not a list, so a non-empty match is
% also a successful one.
at_risk(Party, Input) :-
exposed_to(Party, Input),
call_ns(incidents, outage(Input, critical), Hits, 10),
Hits = [_|_].
call_tool_into/4: acquire and remember in one step. The factifying variant dispatches a tool, routes its result into a named namespace as typed facts (records become entities with scalar attributes), and returns a receipt rather than the data. Entity names are content-hashed, so repeating the call converges instead of duplicating, and the target must be a namespace other than the one running the proof.
% Pull a zone's current rates into the rates cell as facts. The receipt says
% what was written; the data now lives where later proofs derive from it at
% zero inference cost.
refresh_rates(Zone, Written) :-
call_tool_into('data-grout@1/store.list@1',
[collection-rates, filter-[zone-Zone]],
rates, Receipt),
memberchk(facts_written-Written, Receipt).
call_tool_cached/3,4: evidence under tabling. Tabled evaluation and mid-proof suspension do not compose, and the fix is not to table the tool call but to make it stop suspending. The cached variant memoizes tool results host-side for the life of the worker: the first identical call yields as usual; every repeat is a plain fact lookup, safe under backtracking and tabling on either engine. Keep :- table for pure predicates and put the cached call inside the evidence predicate.
% Pure, tabled recursion over an evidence predicate that fetches once per node.
:- table reachable/2.
reachable(A, B) :- link(A, B).
reachable(A, C) :- reachable(A, B), link(B, C).
link(A, B) :-
call_tool_cached('data-grout@1/store.get@1',
[collection-topology, key-A], Rec),
member(next-B, Rec).
Only ground arguments are cached; the cache is per worker, bounded, and not replayed on rehydration, because tool results describe external systems and a worker restart is the right moment to ask again.
Batteries: A Package System for Logic
Logic Cells gain capabilities the way software environments do: by installing packages. Logic Batteries is the package system, an open registry of versioned Prolog rule modules, each a battery, published at github.com/datagrout/logic-batteries. At time of writing there are forty-six batteries across six categories: a core of portable list and aggregate helpers (one Apache-licensed module, every predicate prefixed core_, loaded into every Logic Cell, added because batteries kept redefining the same helpers under their own prefixes); general reasoning (state machines, temporal ordering, taxonomies, provenance, fixpoint saturation, and assign, a budgeted constraint search); probabilistic inference; business rules (approval chains, pricing, compliance, scheduling, and the newest and largest pair: duty, sixteen predicates over rest limits and fitness for duty, and rostering, eighteen predicates that fill and audit rosters by depending on both duty and assign); sixteen simulation and game domains; and a tabletop rules layer implementing the SRD 5.1 mechanics (CC BY 4.0) as seven composing modules: core, conditions, combat, monsters, experience, grid, and spells. Dice stay client-side: the engine adjudicates, the caller rolls. Installing needs no schema or migration: the tenant asserts ordinary typed facts and the battery’s predicates reason over them. Batteries pass the same certified admission pipeline as hand-written rules (validated, certified, compiled per namespace, idempotent by version), so a package brings capability without an exception to the trust model.
A battery documents itself and is admitted twice. Each rule file opens with a manifest, battery_module/3 plus one battery_export/3 per public predicate, which batteries.describe and the command-line tool read as the authoritative documentation, and declares its input predicates dynamic so a standalone user can assert facts after loading. The first admission is at authoring time: a continuous-integration lint enforces the runtime’s predicate whitelist (no process execution, file I/O, networking, or global mutable state) and a portability ratchet flags any non-ISO call, so a module that would fail certified admission never reaches the registry. The same files run unchanged in bare swipl or scryer-prolog, and a battery command-line tool on crates.io vendors them into any Prolog project under a checksummed lockfile. Install state is an ordinary fact, attribute('_batteries', battery_id, version), so “what is installed here” is a plain query. A query names the batteries it needs with require/1 (consult/1 and use_battery/1 are synonyms), singly or as a list, and a bare require installs and succeeds, so it serves as a setup step in a flow.into plan; a goal that calls a predicate no installed battery defines auto-installs the battery that defines it, installing a battery installs its requires, and the registry cache expires on a schedule, with a failed refresh serving the last good copy.
Three batteries deepen the substrate rather than extend it:
- explain is a provenance meta-interpreter:
why/2returns the facts supporting any conclusion,explain/2full proof trees. With certificate chaining, a Logic Cell answers not only what follows but from what, exactly. - fixpoint provides bottom-up saturation: cyclic and left-recursive rule sets that would require tabling run verbatim, trading generality for the guaranteed termination the admission classifier can only warn about.
- prob-core-iso is the mechanism behind the engine-tier promise above: a ProbLog-style runtime written in pure ISO Prolog, over which weighted rules are reified, so that probabilistic queries (noisy-or success, expected value, decision-theoretic argmax via its companion battery) run identically on both engines.
Batteries share the fact vocabulary and declare dependencies on one another (probabilistic market dynamics on economy; probabilistic perception on combat), so the registry is a dependency graph, not a flat list of snippets.
A small set of built-in system modules (plan-execution state machines, FSM structural analysis, measurement rules for the platform’s benchmarking data) is present in every namespace and cannot be shadowed, since a tenant asserting under a system module’s name would silently rebind behavior the platform depends on.
This is the substrate the platform’s other systems stand on: Forensic Inference: Structured Agent Reasoning Over Accumulated Facts is a usage pattern over it; the Governor’s reflex triggers (see Governor: Neuro-Symbolic Runtime for Token-Efficient Agent Cognition) evaluate against stored facts; and the platform’s navigation and memory layers persist their outputs as facts.
The agent loops mine it most directly. The interstitial cycle described in Agentsmith: A Symbolically-Grounded Agent Architecture does a turn’s work outside the context window in typed sub-loops, several of them pure logic operations with no model involved: the memory-check interstitial queries the store before anything is generated; the execute interstitial dispatches planned assertions, queries, and rule admissions; every tool result is checkpointed back as compact facts the next turn’s hydration reads; and grounding verification tests a model’s relation claims against stored predicates, diagnosing each as grounded, inverted, or unsupported. The coding agent’s orient step and the memory layer’s hydration have the same shape: the Logic Cell is where the loop puts what it learned and where it looks before spending a model call. Interstitials are its most frequent client, and certified admission and governed re-entry are what make it safe to let an automated loop write rules as well as facts.
A Rulebook Under Query
The properties above are easiest to see in one small Logic Cell: a discount rulebook
(customer tiers from lifetime spend, seven summing discount components, a hard
40% cap), loaded and queried directly (namespace discount_demo, verified
2026-07-06):
tier(C, platinum) :- lifetime_spend(C, S), S >= 500000.
raw_discount(O, Pct) :- aggregate_all(sum(P), component(O, _, P), Pct).
capped_discount(O, Pct) :- raw_discount(O, Raw), Pct is min(Raw, 40).
final_price(O, Price) :- order_rec(O, _, Gross, _, _, _),
capped_discount(O, Pct),
Price is Gross * (1 - Pct / 100).
Three questions it answers that a store cannot, and that in-context reasoning answers unreliably:
Composition through a cap. final_price(o7, P) yields $48,000: seven
components sum to 68%, the cap clamps to 40%, and the arithmetic follows. The
answer is three rule applications deep and stored nowhere.
Provenance. With the explain battery installed, why(tier(acme, platinum), Facts)
returns the supporting fact lifetime_spend(acme, 620000) rather than a
plausible sentence about it. The tier is visibly derived, and the query
certificate chains to the rules that produced it.
Counterfactual interaction. Raising the strategic-volume threshold from
$50k to $70k changes exactly one order’s price: o4, from $37,950 to
$46,200. o1 does not change: it was already above the cap, so losing a 15%
component leaves it clamped at 40%. A cap absorbing a change is trivial for
resolution and easy for a language model to miss.
Re-run any of these and the answers are byte-identical, because nothing is sampled.
On measurement
The economic case for moving derivation off the token path has been measured at the platform level (a head-to-head over a production Salesforce and Jira org, matching figures for 2,840 tokens against 157,585 in the starkest case, with one in-context run failing after 440,655 tokens), but those numbers cover the whole offload path, not derivation alone. A head-to-head over the rulebook above is specified with verified ground truth; its comparison arm has not yet been run.
Living Applications
The substrate’s end state is worth naming: a Logic Cell whose rules are served is an application. The Reactor surface exposes an admitted rule as a live HTTP endpoint: the rule head is parsed into the input/output contract, so the head is the API; the namespace is the application’s identity; requests are evaluated by ephemeral fact assertion inside the same sandbox that governs every query; effect-capable rules are forced onto mutating verbs by inspection; and public exposure is bounded by a fixed-window request ration.
An agent that asserts facts, installs a battery, admits a rule through certification, and exposes it has built, verified, and shipped a working application without a line of conventional code. Served rules and the panels in front of them are the subject of the Reactor and Smart Panels paper, scheduled for October 2026.
The consumer that exists today is not an agent at all. Tether is a game-engine client for the platform: one Lua core shared by Roblox (Luau), LÖVE, Solar2D, and Defold adapters, plus a Godot addon exposing the same methods in GDScript, with Unity and Unreal planned. A game installs batteries into a namespace, asserts its state as facts, and asks the cell to adjudicate, which makes it the authoritative rules engine for software running a real-time loop. The economics are arranged for that loop: deterministic tools cost one credit, and batch runs up to twenty logic operations as one charged call, so a tick can afford one round-trip; watch polls a namespace for fact changes; every call carries an idempotency key, so a retried assert cannot write twice; and when credits run out the client fails locally for thirty seconds before probing again, so a loop cannot hammer the network. The game binary is the client, so no secret ships in the build: the first connect runs the onramp and stores a per-installation identity in the engine’s save location. The sixteen game batteries and the d20 layer exist because of this consumer.
Two arrangements are possible, and they differ in where the loop lives. In the first, the game owns the tick: the engine runs its frame, batches the facts that changed, and asks the namespace to adjudicate. In the second, the game engine itself lives in the Logic Cell: the world’s state and its rules are facts and admitted rules in one namespace, the platform drives the tick (the Governor’s reflex cycle evaluating triggers against the facts, or the scheduler firing a step on an interval), and the client is a renderer that learns of change by watching the namespace or by push over the WebSocket. The second arrangement is what makes a match a thing the platform can certify end to end, since every ruling is a fact with provenance, and it is the shape the session lease is being designed around.
-- The client rolls the dice; the cell adjudicates the rules.
local dg = Tether.connect()
dg:batteries().install("d20-combat", "arena", function(r) print(r.installed_count) end)
dg:batch("arena", {
{ op = "assert", facts = { "attribute(fighter, hp, 24)", "attribute(goblin, hp, 7)" } },
{ op = "query", prolog = "d20_damage(fighter, goblin, 8, Final)" },
}, function(results) applyDamage(results) end)
dg:query("arena", "hits_ac(fighter, goblin, 17)", function(hit) if #hit > 0 then swing() end end)
Operational Characteristics
Facts are encrypted at rest, with plaintext columns limited to indexable previews; full values rejoin results at read time. A reaper retracts expired facts from storage and any live engine. Workers sleep after minutes of inactivity, and rehydration is size-aware: small namespaces replay their facts; past a threshold, the facts are materialized to a file and bulk-consulted in one engine call, roughly half a second for two hundred thousand facts. The bulk path exists because replay-per-fact exhausted its database checkout as namespaces approached a million facts, taking the session down with it. Rehydration also re-derives dependent state: which stored rules need the streaming execution path, which predicates were tabled. Fact writes are embedded asynchronously, so every Logic Cell’s contents reach semantic retrieval without a separate indexing step.
The engineering record behind these properties is unglamorous and the substance of the contribution: multi-solution streams that re-enter suspension points; workers orphaned by hard-killed supervisors; workers that could not exit at all, because calling the engine’s own halt from an alarm handler deadlocked inside a cleanup routine’s mutex; compiled clauses leaking across tenants sharing a worker; scope threaded everywhere except the one dispatch path that mattered; sandboxes that made results uninspectable to the rules receiving them. Each appears only when a logic engine is run as long-lived, multi-tenant, tool-connected infrastructure, and each is now a regression test.
Comparison with Existing Approaches
| Vector memory | Embedded Prolog library | Datalog services | Logic Cells | |
|---|---|---|---|---|
| Retrieval | Similarity | Exact/derived | Derived | Exact, derived, and semantic |
| Derivation | None | Full | Stratified subset | Full, admission-certified |
| Rule authorship | — | Trusted code | Schema owners | Untrusted agents, certified |
| Persistence | Native | Caller’s problem | Native | Native, encrypted, TTL |
| External calls mid-inference | — | Unrestricted FFI | None | Governed re-entry |
| Execution guarantees | — | None | Termination by construction | Termination classes, certified |
| Marginal cost of a derivation | Embedding + tokens to reason | Compute | Compute | Compute; zero tokens |
The nearest relatives are Datalog-based services, which obtain termination by restricting the language. This design takes the opposite bet: keep full Prolog and make the safety story explicit: classify termination instead of guaranteeing it, certify what was checked, sandbox by engine construction where the deployment demands it, and govern the escape hatches rather than welding them shut.
Limitations and Trade-Offs
Termination classification is honest, not complete. unbounded means “no argument found,” not “diverges”; such rules are admitted with warnings and bounded execution rather than refused.
Two engines is a real cost. Every cross-cutting mechanism (suspension, error shapes, rehydration, result marshalling) is built and tested twice. The payoff is the conformance tier; deployments that never pin pay the complexity anyway.
The natural-language bridge is probabilistic. NL assertion and querying translate through a model; the embeddings-anchored vocabulary reduces drift but does not eliminate it. Precision-critical paths should use direct assertion and raw goals, which is why both are first-class.
Generation is bounded in time, not in space. The termination classifier
reasons about whether a proof ends, not how much it writes. A rule combining
unbounded enumeration with the factifying call_tool variant can grow a
namespace as fast as it can prove; the defenses there are quota and TTL rather
than analysis.
Suspension holds a worker. A proof waiting on a slow external tool occupies its namespace’s worker for the duration. Depth bounds and per-namespace isolation contain the blast radius; they do not make the wait free.
Wake-up coordination is shared. Running workers are isolated processes, but waking them is coordinated by a shared session manager, so one namespace’s slow rehydration can delay unrelated wake-ups. The bulk path shrinks that window by orders of magnitude; removing the serialization is queued work, and until then isolation applies to running workers, not cold starts.
Future Directions
Storage-Resident Facts
Workers currently rehydrate a namespace’s full fact set, cheaply but entirely. Resolving fact predicates directly against indexed storage, with the engine holding only compiled rules and working memory, would make workers nearly stateless, admit concurrent readers per namespace, and turn cold-start cost into a per-query concern. Prewarming exactly the predicates a goal touches is the intermediate step.
Read Replicas for Re-Entry
The structured refusal for same-namespace re-entrant reads exists because the proof holds its own worker. Ephemeral read-only workers, hydrated on demand, would convert that refusal into a served query without disturbing the write-side isolation model.
Certified Batteries as an Ecosystem
Batteries already pass certified admission per namespace at install time. Signing them at publication, so that termination and sandbox analysis travels with the module and is verifiable before installation, would extend the certificate chain from “this namespace’s rules” to “this ecosystem’s libraries.”
Labeled Facts and Mounted Namespaces
Isolation is currently the namespace, and there is nothing finer. Sharing a subset (a project’s facts but not the rest, at a bounded resolution, for a bounded time) requires labels on facts and a lattice over those labels: a derived fact inherits the most restrictive union of its sources, and a reader sees a conclusion only if their grant covers every fact beneath it. The same order answers mounting: one Logic Cell consulting a slice of another under an attenuated grant, where attenuation is the only derivation permitted and revocation needs no transitive chase. The certificate chain already knows which facts produced a conclusion; labels make that chain enforceable.
Proof-Gated Releases
Served applications currently evolve rule by admitted rule, live. The intended discipline adds a development/production fork, promotion gated on the full evidence set (certificates over every rule, agent-written test suites, termination and conformance checks), and an exported namespace snapshot as the release artifact. Deployment becomes a proof obligation rather than a process.
This document describes the conceptual architecture of Logic Cells. Sandbox predicate inventories, dispatch internals, engine protocol details, and storage schemas are part of the operational implementation and are not specified here.