The engine, precisely

In brief

A small, deterministic Python kernel (about 7,400 lines, no runtime dependencies) for a Prolog dialect aimed at story worlds:

• Two execution paths. Non-recursive predicates run by ordinary SLD resolution with backtracking. Recursive predicates are detected and tabled automatically, then evaluated by naive fixpoint iteration. On that path cut is rejected, and answers are sets.
• Stratified negation, checked per predicate before any query runs.
• A native Event Calculus (holds_at/2) with explanations produced by the same procedure that answers the query. It finds calculated effect times, and stops on circular rules and on timeline rules that read story state.
• Query results carry completion status: COMPLETE, EXHAUSTED, or CANCELLED. Game decisions and temporal explanations keep that information: unfinished reasoning gives a disabled, indeterminate decision or an explanation of unknown truth, never a permission or a definite cause (details).

It deliberately isn't a general-purpose Prolog. By default, undefined and unsupported predicates fail quietly, with status COMPLETE. Game models should use strict checking. Known gaps lists the places where it can be wrong without saying so.

Facts, rules and story events

Facts record relationships; rules infer new ones:

parent(alice, bob).    parent(alice, carol).    parent(bob, dave).
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

Ask grandparent(alice, Who). The engine finds bob among alice's children, then dave among bob's children. It backs up to try carol, who has no recorded children. The answer is dave, a relationship nobody explicitly wrote down. Backtracking explores those alternatives; tabling remembers answers for recursive rules, subject to the finiteness and budget limits below.

The Event Calculus adds changes over time. An event such as Harriet's hack switches a property such as the vending machine being offline on or off. The engine follows that property's persistence through the named story moments. Its explanation identifies the initiating event and, when recorded in the model, a supporting sentence. The timed-rule example below explains the limits of this interpretation.

Quick reference

For a feature-by-feature table with SWI references and recorded executable probes, see Prolog compatibility. The summary below describes the broader design; that page identifies exactly which examples were verified.

Negation and stratification

\+ G succeeds if G has no solution. As in ISO, it binds nothing and doesn't check for floundering. The engine also doesn't reorder goals around negation. The earlier engine did, which sometimes gave the declaratively right answer, but not Prolog's.

Before any query runs, the program is checked for stratification: no predicate may depend on its own negation through any non-monotone construct. Those constructs are \+, forall, aggregates, if-then-else and soft-cut with an else branch, and ignore/1. The check looks through ^/2 and statically known call/N goals.

The check works at the level of predicates, not ground atoms. So programs that are safe only because of their data are rejected (in the literature, programs that are modularly but not predicate-stratified):

move(a, b).  move(b, c).
win(X) :- move(X, Y), \+ win(Y).
% SemanticConflict: negation is not stratified: {win/1} depends on its own negation

SWI answers this program (win(b)), and with tabling it would use the well-founded semantics. This engine refuses it rather than guess. A dependency hidden behind a runtime call/1 can slip past the static check. It's caught at run time and reported as EXHAUSTED, which overloads a status that usually means "a budget ran out."

Tabling

Recursive strongly connected components are tabled automatically (auto_table=True); :- table also works. Tables are keyed by call variant and filled by naive iteration. All the tables in a stratum iterate together until nothing changes, which makes left and mutual recursion complete:

road(a, b). road(b, c). road(c, a). road(c, d).
reach(X, Y) :- reach(X, Z), road(Z, Y).
reach(X, Y) :- road(X, Y).
% ?- reach(a, W).   W = b ; c ; a ; d      (terminates despite the cycle)

The conditions and costs:

• Termination needs finiteness. Recursion terminates and is complete when there are finitely many call variants and answers. An infinite answer set, such as nat(z). nat(s(X)) :- nat(X)., runs until the budget, as it would under tabling in SWI.
• Answers from tabled predicates are sets. Their order and multiplicity differ from plain SLD resolution.
• Tables are query-local. Nothing is reused across queries.
• There's no semi-naive evaluation, so later passes can repeat work on answers already found. The cost depends on the rules, call variants and term sizes; answer count alone does not determine it. The algorithm is closer to iterated (linear) tabling than to SLG.
• No answer subsumption and no incremental tabling.
• Cut is rejected in tabled predicates, and the rejection is global. Loading succeeds, but from then on every query on that knowledge base raises SemanticConflict, even 1 =:= 1, until the clause is removed. A predicate that fails the stratification check does the same. Set auto_table=False to allow cut; left recursion then runs until the budget.
• Tabling everything recursive has a price. Ordinary recursive list code pays for it:

A left-recursive all-pairs "reaches" rule over a 160-link chain (12,880 answers) exhausts the default budget at 11,169 answers, correctly marked EXHAUSTED. The same rule written right-recursively finishes in 0.3 seconds, and the left-recursive form over 80 links completes in 1.6.

Result status

Every query result carries a status (the code calls it Completion; it has nothing to do with Clark's completion):

• COMPLETE: the search ran to the end.
• EXHAUSTED: a budget ran out, or the engine stopped because it couldn't establish the answer, as with a circular story-time question, a timeline that depends on story state, or a negation cycle caught at run time (see Negation). The defaults are 2,000,000 resolution steps and a depth of 1,200. The answers found so far are returned; anything else is unknown.
• CANCELLED: the host's cancellation callback stopped the query; any answers are partial.

kb.query() raises IncompleteResult rather than return an EXHAUSTED result, so an empty list never means "gave up." It can still mean "no such predicate," because of the quiet default for unknown predicates. kb.ask() returns partial answers with the status attached.

What a request's budget covers. Besides solving, a request's Limits and cancellation callback cover preparing the story timeline (source enumeration, ground effect-time collection, graph construction and ordering diagnostics) and discovering calculated effect times. The first request after a load or change pays for preparation, even a non-temporal one such as ask("true"). ask and explain include preparation's work and depth in their accounting. Cancellation is checked at request entry, after uncached static analysis, and every 512 charged steps. These are cooperative work controls, not wall-clock deadlines. A game menu runs several internal queries, and each has its own budget. Outer answer limits never truncate the timeline's source search.

Weak spots:

• The default budget is generous. nat(z). nat(s(X)) :- nat(X). reports EXHAUSTED after 198 answers in about 5 seconds with a 20,000-step budget. With the default budget it would take, by extrapolation, around an hour.
• Converting partial answers can be slow. gen(L) :- member(_, L). reports EXHAUSTED in about 6 seconds, but converting its 1,498 partial lists to Python values takes about 100 more.
• Integer arithmetic isn't budgeted. X is 10^5000000 counts as one step.
• Parsing and static analysis aren't charged per operation.
• Large worlds may need a larger budget. Ordering the timeline has a quadratic cost, and it counts against the request's budget.
• Inspection properties use the default limits. Public inspection properties raise IncompleteResult if timeline preparation stops.

Story time: the Event Calculus

time(t1). time(t2). time(t3). time(t4).
before(t1, t2). before(t2, t3). before(t3, t4).
happens(switch_on, t1).    initiates(switch_on, light_on).
happens(switch_off, t3).   terminates(switch_off, light_on).
% ?- holds_at(light_on, T).    T = t2 ; t3

The engine implements a simplified Event Calculus in the style of the 1990s formulations (Shanahan's among them), evaluated natively rather than by Prolog axioms.

• Vocabulary. happens/2, initiates/2,3, terminates/2,3 (facts or rules), initially/1, holds_at/2.
• Time. Time points are named by time/1, by before/2, by happens/2, or by the ground time in an initiates/3/terminates/3 clause. Plain numbers work too. T1 ≺ T2 means reachability in before/2, or numeric order. Points on unconnected chains are incomparable, and a cycle in before/2 is reported. A time that an effect rule calculates is found too, within the limits in Calculated effect times.
• When effects are visible. A fluent initiated at T1 and terminated at T2 holds on (T1, T2]: strictly after it starts, up to and including the moment it ends. This is the standard reading. A rule body that asks holds_at(G, T) therefore sees the state before anything that happens at T.
• Simultaneity. tie_break="init_wins" (the default) or "term_wins" decides a tick where the same fluent is both initiated and terminated.
• Exclusive fluents. Only by declaration. exclusive_fluent(f) means f holds at most one value per slot, where a slot is the functor plus every argument except the last. Initiating f(a, v2) ends f(a, v1). On a contested tick the first-authored initiation wins.

Where it departs from the classical Event Calculus. In the textbook axioms, the third argument of initiates/3 and terminates/3 is the occurrence time of an event that must also appear in happens/2. Here it's the time the effect lands, and happens/2 isn't required. That lets a model be written entirely in the /3 form. But conditional effect rules written the classical way mean something different:

happens(flip, 1).  happens(flip, 3).  time(1). time(2). time(3). time(4). time(5).
initiates(flip, on, T)  :- \+ holds_at(on, T).     % a toggle
terminates(flip, on, T) :- holds_at(on, T).
% Classical reading (SWI with the textbook axioms):  on holds at 2, 3
% This engine:                                       on holds at 2, 4, explained by a
%                                                    termination at 2, when flip didn't happen

The answer comes back COMPLETE, with no warning. The same applies to any conditional timed rule. terminates(check, on, T) :- holds_at(g, T). fires at every moment g holds, not only when check happens. Even terminates(check, on, _) misfires.

Here, a timed effect rule has to say when its event happens:

terminates(check, on, T) :- happens(check, T), holds_at(g, T).

The rewrite's own docs describe the 3-argument forms but never flag this departure from the classical reading.

Calculated effect times

An initiates/3 or terminates/3 rule may calculate when its effect lands, for example terminates(timer, unlocked, T2) :- happens(timer, T), T2 is T + 1. The engine finds that time without a time/1 declaration. If a badge scan unlocks a door and the timer happens at minute 3, the door is still unlocked at minute 4 itself (the usual delayed effect) and locked afterwards; at minute 9, explain names the timer's termination at minute 4. Discovery runs inside the temporal query, using the ordinary solver and the request's budget and cancellation, with isolated bindings and tables. It doesn't change the authored time/1 facts or the cached base timeline.

The supported case is a finite rule that generates its time without reading temporal state. A generator that calls holds_at, directly or indirectly, is reported as uncertain; so are discovery errors and clause-level cuts that could make per-clause enumeration misleading. The discovered times are shared by every story-time question in a query, so one such generator can make otherwise unrelated story-time questions uncertain; non-temporal queries are unaffected. Rules constrained to named output times keep the ordinary state-dependent evaluation. A rule that yields an additional time only when that time is already supplied (for example, one that tests nonvar(T)) must have that time named, for example with time/1; otherwise its effect is missed without warning. Discovery is bounded; it doesn't resolve circular temporal rules.

Reproduction and verification: repair history.

Circular temporal rules

When a story-time question depends on its own answer, the engine stops rather than guess. Take a door that starts unlocked, with terminates(auto_lock, unlocked, 1) :- holds_at(unlocked, 9). and an entry guard on holds_at(unlocked, 9): the state at minute 9 depends on whether the lock fired at minute 1, which depends on the state at minute 9. The query stops as EXHAUSTED with no assumed answer and a note naming the circular call. Its explanation has holds=None and no asserted cause, and entry is disabled and indeterminate. Under the default tie_break="init_wins", changing the lock rule's condition to holds_at(unlocked, 1) gives the ordinary completed denial, and explain names the locking effect.

The stop crosses negation, control flow, aggregates and tables. A tabled helper can't bypass it: story-time calculations entered from an active table session use their own table store, and the caller's store is restored afterwards. Ordinary recursive helpers complete their own fixed point. This is a conservative runtime boundary, not a three-valued well-founded solver. It keeps independent proofs already obtained and leaves unrelated queries usable, but it doesn't explore later alternatives after reaching a cycle, so some answerable circular questions stay open. Current-tick checks under term_wins can reach cycles that init_wins avoids.

Listing what holds at a time. For holds_at(F, T) with F unbound and T named, candidates come from initial fluents and from initiations at strictly earlier ticks, and each candidate is checked with the ordinary evaluator. Future and incomparable /3 heads that can't match those ticks are skipped, so a listing of the present completes even when a /3 rule tied to a later time is circular, while a question that actually reaches the cycle stays uncertain. In this museum, an alarm check at minute 10 depends on its own outcome at minute 11:

time(1). time(2). time(10). time(11).
initially(light_on).
initiates(alarm_check, alarm_on, 10) :- \+ holds_at(alarm_on, 11).
% ?- holds_at(F, 2).            F = light_on, COMPLETE
% ?- holds_at(alarm_on, 11).    no answers, EXHAUSTED

Queries over all times keep time order and may return sound earlier answers before reaching a later incomplete point. Because discovery supplies named ticks to /3 rules, universal-time and nonvar(T) rules can appear in listings where the ground evaluator proves them; no new times are invented. Rule bodies keep their authored order, so a /2 effect body, which runs before its happens/2 join, can reach future reasoning; so can a variable-time /3 body whose time filter follows its temporal call. A state-reading time generator can still make a listing uncertain (see Calculated effect times). Current-tick clipping and both tie policies behave normally.

Effect on the engine's testworld model. It has an alarm/secret post-state cycle, so affected alarm and secret queries report uncertainty. A broad listing at its first point, t0, completes (empty); broad listings at t1 through t6 stay uncertain through its /2 alarm cycle. Normal trust progression and the ordinary story and affordance models are usable.

Reproduction and verification: circular temporal reasoning and time-scoped listings in the repair history.

Building the timeline

The timeline (its points, their order and the events) comes from time/1, before/2 and happens/2, solved as ordinary goals, plus the ground times in /3 effect clauses. Those three predicates must not depend on story state. If they do, as in before(lock_check, arrival) :- holds_at(locked, arrival)., temporal queries and explanations return no answers, with status EXHAUSTED and notes explaining the dependency. Here that status means the reasoning couldn't be established, not that a budget ran out. Explanations have holds=None, and dependent actions are disabled and indeterminate. Ordinary non-temporal queries, unrelated actions and independent earlier proofs remain usable. Replacing the rule with the fact before(lock_check, arrival). restores normal answers.

The check combines known dependencies from before/2, time/1 and happens/2 to holds_at/2 with a runtime stop for temporal calls reached through computed meta-calls during construction. Both temporal queries and explanations reject an affected timeline before calculating effects. The static policy is conservative: a known dependency blocks temporal evaluation even in an unreachable branch, and opaque calls in branches that construction never reaches can't be validated. Each timeline source discards its bindings and tables before the next one runs, so an interrupted table can't leak provisional facts into the timeline. The engine doesn't compute a joint fixed point of time and state; ordinary state-dependent effect rules are unaffected.

Preparing the timeline counts against the initiating request's budget and cancellation (see Result status). Completed preparation is reused until the program changes; a mutation or restore forces preparation for the new revision. Interrupted preparation is discarded, a tabled source's buffered partial answers can't become a completed timeline, and a later request retries normally.

Reproduction and verification: circular timeline construction and timeline preparation limits in the repair history.

Explanations and provenance

• kb.explain(fluent, time) says why a fluent does or doesn't hold. It comes from the same decision procedure as holds_at, not reconstructed afterwards. The reasons are initially, initiated (by which event, when), clipped (by which event, when), never_initiated, and unexplained (the reasoning didn't finish). An unexplained result has holds=None in Python (null in JSON), carries the status and notes, and asserts no initiating or terminating cause: hosts must treat it as unknown, not false. A completed false explanation has holds=False.
• kb.spans_for(fact) returns the source-text spans the model records as supporting a fact, through authored fact_id/2 and supports/2 facts.
• There are no rule-level derivations. The engine doesn't record which clauses and bindings produced an answer. It has no why/1, derivation/1 or evidence_chain/1, which is why it fails the three explanation probes in the comparison. And explain() on a fact that isn't a fluent reports never_initiated, even when the fact is true.

Known gaps

The host API

from cyclops import KnowledgeBase
from cyclops.api import decide, affordances

kb = KnowledgeBase()                     # options: occurs_check, tie_break, unknown_fails, auto_table, ...
kb.load(text) / kb.consult(path)         # add clauses
kb.query(goal)                           # answers as Python values; raises if the search didn't finish
kb.ask(goal, limits=..., distinct=...)   # Solutions: answers + status + notes
kb.holds(goal)                           # bool; raises if it gave up before finding an answer
kb.explain(fluent, time)                 # see above
kb.assert_(clause) / kb.retract(clause); kb.snapshot() / kb.restore(s)
decide(kb, action, site)                 # Decision: kind, allowed, message, status, notes
affordances(kb, site)                    # a site's menu: Affordance entries with label, enabled, kind

• Answer order is part of the contract and is tested across processes and hash seeds.
• JSON output tags atoms and compounds and includes the status.
• Game hooks. affords(Action, Site), guard(Action, Order, Condition, Message) and action_label/2 let a host ask "may I do this here, and if not, what do I say?" Guards are checked in the author's order, and the first unmet one supplies the message. An action the site doesn't offer abstains, which is different from being denied.

Decisions when reasoning can't finish

A game decision is only as definite as the reasoning behind it:

An indeterminate decision has kind == "indeterminate", allowed=False, the neutral message "Action availability could not be determined." and a status: EXHAUSTED, CANCELLED, or JSON status "error" when a typed engine error occurred during decide. For example, with KnowledgeBase(auto_table=False), a guard list whose second row loops (guard(open_gate, 2, true, 'Unused') :- loop.) makes decide(kb, "open_gate", "gate") indeterminate with EXHAUSTED, although the first guard was found. Decision and menu JSON (as_json()) include status and notes, and menu entries include their decision kind. affordances raises IncompleteResult if action discovery or label lookup is incomplete; an action whose decision can't finish is listed as a disabled, indeterminate entry. decide and affordances take the same limits and cancel arguments as ask. Limits apply to each internal query, not as one budget for a whole menu. A cancelled decision is indeterminate too, never a permission or an authored refusal; retrying with enough budget and cancellation cleared gives the ordinary decision.

Reproduction and verification: repair history.

Strict checking for game models

KnowledgeBase(unknown_fails=False) turns a reached undefined predicate into an error instead of a quiet failure. It's recommended for game models; the engine's default is permissive. In a decision, that error disables only the affected action: a misspelled guard such as guard(enter, 1, \+ lokced(laboratory), 'The door is locked') makes enter indeterminate with lokced/1 named in its notes, while other actions at the site stay available. The host's optional lookups tolerate absence: if guard/4 or action_label/2 isn't defined at all, actions are unguarded and get a fallback label (read_notice is labelled read notice). To declare a relation that is intentionally empty, write :- dynamic locked/1.

The exception covers only wholly absent guard/4 and action_label/2. A definition with only the wrong arity is still an error, and defined rules, actual conditions and the required affords/2 inventory are checked normally. The fallback runs an ordinary checked query, keeping analysis, resource handling and diagnostics. Strict mode checks the calls that are actually reached. It can't recognize gaurd/4 as a misspelled optional head, detect a misspelled fluent argument inside a valid holds_at/2 call, or inspect alternatives skipped by a first proof. It is not a static authoring validator.

Reproduction and verification: repair history.

Performance

Revised full-binding timings on one Windows machine, September 25, 2026. Both engines materialize every requested variable; the rewrite uses native answer terms, with Python value conversion measured separately. See the method, exact-answer checks, batch ranges and raw timings.

These measurements include query setup and result construction, and do not isolate interpreter overhead. SWI executes compiled goals; the rewrite parses each query. The list-split SWI and Python-conversion measurements varied substantially. The original placeholder-answer SWI ratios are superseded.

The earlier story-model audit measured about 20 ms to load 748 facts and 1–16 ms for example queries/explanations; those particular observations were not retimed in this benchmark run. There is no cross-query answer cache. The old engine's cache was fast and had a separate result-aliasing bug: fixing that bug would not eliminate the caching advantage.

Design in one paragraph

There is one term representation, one reader, and one clause list per predicate holding facts and rules together. One solver serves top-level queries and rule bodies, and there is one holds_at. All long-lived state belongs to the program and is versioned by a single revision counter. Everything query-local lives in a context created per query and thrown away. Derived data (static analysis, the timeline, diagnostics) is tagged with the revision it came from, so staleness is detected by comparing one integer. Line and test counts below are at 9be7804.

What changed from the earlier engine

The migration drill-down supplies the measured comparison, test dispositions and capability gaps; the revised 21-case run separates observed correctness from timeout uncertainty. Architecture compares how the two engines are organized at their latest revisions: request routing, where state lives, and what a host sees when a query can't finish.

Semantics the rewrite chose differently:

• ISO \+ with no goal reordering;
• ISO precedence for ,, ; and \+;
• 1 and 1.0 kept distinct;
• // truncates;
• exclusivity only by declaration;
• no why/derivation/evidence_chain predicates.

Removed:

• two-evaluator routing;
• a seven-stage query pipeline;
• a handler registry;
• a six-level cache hierarchy;
• five parsers.

Left out: the text parser, the command-line game, the narrative tools and the analysis tools.

Deferred: semi-naive tabling, cross-query caching, rule-level explanation and concurrency.

HISTORY.md runs the same programs on both.

Compared with SWI-Prolog

SWI-Prolog is a complete, fast, largely ISO-conformant system with nearly 40 years of engineering behind it. For almost anything, use SWI; for Python, its janus bridge works well.

This engine is for one job: reasoning about authored story worlds, with answers you can explain. For that job it offers:

• a native Event Calculus whose explanations come from the decision procedure itself;
• source-sentence provenance;
• a result status on every answer by default;
• a small, dependency-free Python package.