eyeling

Inside Eyeling

A compact Notation3 reasoner in JavaScript — a handbook

This handbook is written for a computer science student who wants to understand Eyeling as code and as a reasoning machine.
It’s meant to be read linearly, but each chapter stands on its own.

Contents

Preface: what Eyeling is (and what it is not)

Eyeling is a small Notation3 (N3) reasoner implemented in JavaScript. Its job is to take:

  1. Facts (RDF-like triples), and
  2. Rules written in N3’s implication style (=> and <=),

and compute consequences until nothing new follows.

If you’ve seen Datalog or Prolog, the shape will feel familiar. Eyeling blends both:

That last point is the heart of Eyeling’s design: forward rules are executed by proving their bodies using a backward engine. This lets forward rules depend on computations and “virtual predicates” without explicitly materializing everything as facts.

Eyeling deliberately keeps the implementation small and dependency-free:

This handbook is a tour of that miniature system.

Chapter 1 — The execution model in one picture

Let’s name the pieces:

Eyeling runs like this:

  1. Parse the document into:
    • an initial fact set F
    • forward rules R_f
    • backward rules R_b
  2. Repeat until fixpoint:
    • for each forward rule r ∈ R_f:
      • use the backward prover to find substitutions that satisfy r.body using:
        • the current facts
        • backward rules
        • built-ins
      • for each solution, instantiate and add r.head

A good mental model is:

Forward chaining is “outer control”. Backward chaining is the “query engine” used inside each rule firing.

A sketch:


FORWARD LOOP (saturation)
for each forward rule r:
solutions = PROVE(r.body)   <-- backward reasoning + builtins
for each s in solutions:
emit instantiate(r.head, s)

Because PROVE can call built-ins (math, string, list, crypto, dereferencing…), forward rules can compute fresh bindings as part of their condition.

Chapter 2 — The repository, as a guided reading path

If you want to follow the code in the same order Eyeling “thinks”, read:

  1. lib/prelude.js — the AST (terms, triples, rules), namespaces, prefix handling.
  2. lib/lexer.js — N3/Turtle-ish tokenization.
  3. lib/parser.js — parsing tokens into triples, formulas, and rules.
  4. lib/rules.js — small rule helpers (rule-local blank lifting and rule utilities).
  5. lib/engine.js — the core inference engine:
    • equality + alpha equivalence for formulas
    • unification + substitutions
    • indexing facts and backward rules
    • backward goal proving (proveGoals) and forward saturation (forwardChain)
    • scoped-closure machinery (for log:*In and includes tests)
    • tracing hooks (lib/trace.js, log:trace)
    • time helpers for time:* built-ins (lib/time.js)
    • deterministic Skolem IDs (head existentials + log:skolem) (lib/skolem.js)
  6. lib/builtins.js — builtin predicate evaluation plus shared literal/number/string/list helpers:
    • makeBuiltins(deps) dependency-injects engine hooks (unification, proving, deref, …)
    • and returns { evalBuiltin, isBuiltinPred } back to the engine
    • includes materializeRdfLists(...), a small pre-pass that rewrites anonymous rdf:first/rdf:rest linked lists into concrete N3 list terms so list:* builtins can work uniformly
  7. lib/explain.js — proof comments + log:outputString aggregation (fact ordering and pretty output).
  8. lib/deref.js — synchronous dereferencing for log:content / log:semantics (used by builtins and engine).
  9. lib/printing.js — conversion back to N3 text.
  10. lib/cli.js + lib/entry.js — command-line wiring and bundle entry exports.
  11. index.js — the npm API wrapper (spawns the bundled CLI synchronously).

This is almost literally a tiny compiler pipeline:


text → tokens → AST (facts + rules) → engine → derived facts → printer

Chapter 3 — The data model: terms, triples, formulas, rules (lib/prelude.js)

Eyeling uses a small AST. You can think of it as the “instruction set” for the rest of the reasoner.

3.1 Terms

A Term is one of:

That last one is special: N3 allows formulas as terms, so Eyeling must treat graphs as matchable data.

3.2 Triples and rules

A triple is:

A rule is:

Two details matter later:

  1. Inference fuse: a forward rule whose conclusion is the literal false acts as a hard failure. (More in Chapter 10.)
  2. headBlankLabels records which blank node labels occur explicitly in the head of a rule. Those blanks are treated as existentials and get skolemized per firing. (Chapter 9.)

3.3 Interning

Eyeling interns IRIs and Literals by string value. Interning is a quiet performance trick with big consequences:

In addition, interned Iri/Literal terms (and generated Blank terms) get a small, non-enumerable integer id .__tid that is stable for the lifetime of the process. This __tid is used as the engine’s “fast key”:

For blanks, the id is derived from the blank label (so different blank labels remain different existentials).

Terms are treated as immutable: once interned/created, the code assumes you won’t mutate .value (or .label for blanks).

3.4 Prefix environment

PrefixEnv holds prefix mappings and a base IRI. It provides:

Chapter 4 — From characters to AST: lexing and parsing (lib/lexer.js, lib/parser.js)

Eyeling’s parser is intentionally pragmatic: it aims to accept “the stuff people actually write” in N3/Turtle, including common shorthand.

4.1 Lexing: tokens, not magic

The lexer turns the input into tokens like:

Parsing becomes dramatically simpler because tokenization already decided where strings end, where numbers are, and so on.

4.2 Parsing triples, with Turtle-style convenience

The parser supports:

A nice detail: the parser maintains a pendingTriples list used when certain syntactic forms expand into helper triples (for example, some path/property-list expansions). It ensures the “surface statement” still emits all required triples even if the subject itself was syntactic sugar.

4.3 Parsing rules: =>, <=, and log idioms

At the top level, the parser recognizes:

It also normalizes top-level triples of the form:

into the same internal Rule objects. That means you can write rules either as operators (=>, <=) or as explicit log: predicates.

4.4 true and false as rule endpoints

Eyeling treats two literals specially in rule positions:

So these are valid patterns:

true => { :Program :loaded true }.
{ ?x :p :q } => false.

Internally:

Chapter 5 — Rule normalization: “compile-time” semantics (lib/rules.js)

Before rules hit the engine, Eyeling performs one lightweight transformation. A second “make it work” trick—deferring built-ins that can’t run yet—happens later inside the goal prover.

5.1 Lifting blank nodes in rule bodies into variables

In N3 practice, blanks in rule premises behave like universally-quantified placeholders. Eyeling implements this by converting Blank(label) to Var(_bN) in the premise only.

So a premise like:

{ _:x :p ?y. } => { ... }.

acts like:

{ ?_b1 :p ?y. } => { ... }.

This avoids the “existential in the body” trap and matches how most rule authors expect N3 to behave.

Blanks in the conclusion are not lifted — they remain blanks and later become existentials (Chapter 9).

5.2 Builtin deferral in forward-rule bodies

In a depth-first proof, the order of goals matters. Many built-ins only become informative once parts of the triple are already instantiated (for example comparisons, pattern tests, and other built-ins that don’t normally create bindings).

If such a builtin runs while its subject/object still contain variables or blanks, it may return no solutions (because it can’t decide yet) or only the empty delta ({}), even though it would succeed (or fail) once other goals have bound the needed values.

Eyeling supports a runtime deferral mechanism inside proveGoals(...), enabled only when proving the bodies of forward rules.

What happens when proveGoals(..., { deferBuiltins: true }) sees a builtin goal:

A small counter (deferCount) caps how many rotations can happen (at most the length of the current goal list), so the prover can’t loop forever by endlessly “trying later”.

There is one extra guard for a small whitelist of built-ins that are considered satisfiable even when both subject and object are completely unbound (see __builtinIsSatisfiableWhenFullyUnbound). For these, if evaluation yields no deltas and there is nothing left to bind (either it is the last goal, or deferral has already been exhausted), Eyeling treats the builtin as a vacuous success ([{}]) so it doesn’t block the proof.

This is intentionally enabled for forward-chaining rule bodies only. Backward rules keep their normal left-to-right goal order, which can be important for termination on some programs.

5.3 Materializing anonymous RDF collections into N3 list terms

Many N3 documents encode lists using RDF’s linked-list vocabulary:

_:c rdf:first :a.
_:c rdf:rest _:d.
_:d rdf:first :b.
_:d rdf:rest rdf:nil.

Eyeling supports both representations:

To make list handling simpler and faster, Eyeling runs a small pre-pass called materializeRdfLists(...) (implemented in lib/builtins.js and invoked by the CLI/entry code). It:

Why only blank nodes? Named list nodes (IRIs) must keep their identity, because some programs treat them as addressable resources; Eyeling leaves those as rdf:first/rdf:rest graphs so list builtins can still walk them when needed.

Chapter 6 — Equality, alpha-equivalence, and unification (lib/engine.js)

Once you enter engine.js, you enter the “physics layer.” Everything else depends on the correctness of:

6.1 Two equalities: structural vs alpha-equivalent

Eyeling has ordinary structural equality (term-by-term) for most terms.

But quoted formulas (GraphTerm) demand something stronger. Two formulas should match even if their internal blank/variable names differ, as long as the structure is the same.

That’s alpha-equivalence:

Eyeling implements alpha-equivalence by checking whether there exists a consistent renaming mapping between the two formulas’ variables/blanks that makes the triples match.

6.2 Groundness: “variables inside formulas don’t leak”

Eyeling makes a deliberate choice about groundness:

This is encoded in functions like isGroundTermInGraph. It’s what makes it possible to assert and store triples that mention formulas with variables as data.

6.3 Substitutions: chaining and application

A substitution is a plain JS object:

{ X: Term, Y: Term, ... }

When applying substitutions, Eyeling follows chains:

Chains arise naturally during unification (e.g. when variables unify with other variables) and during rule firing.

At the API boundary, a substitution is still just a plain object, and unification still produces delta objects (small { varName: Term } maps).
But inside the hot backward-chaining loop (proveGoals), Eyeling uses a Prolog-style trail to avoid cloning substitutions at every step:

This keeps the search semantics identical, but removes the “copy a growing object per step” cost that dominates deep/branchy proofs. Returned solutions are emitted as compact plain objects, so callers never observe mutation.

Implementation details (and why they matter):

These “no-op returns” are one of the biggest practical performance wins in the engine: backward chaining and forward rule instantiation apply substitutions constantly, so avoiding allocations reduces GC pressure without changing semantics.

6.4 Unification: the core operation

Unification is implemented in unifyTerm / unifyTriple, with support for:

There are two key traits of Eyeling’s graph unification:

  1. It’s set-like: order doesn’t matter.
  2. It’s substitution-threaded: choices made while matching one triple restrict the remaining matches, just like Prolog.

6.5 Literals: lexical vs semantic equality

Eyeling keeps literal values as raw strings, but it parses and normalizes where needed:

This lets built-ins and fast-key indexing treat some different lexical spellings as the same value (for example, normalizing "abc" and "abc"^^xsd:string in the fast-key path).

Chapter 7 — Facts as a database: indexing and fast duplicate checks

Reasoning is mostly “join-like” operations: match a goal triple against known facts. Doing this naively is too slow, so Eyeling builds indexes on top of a plain array.

7.1 The fact store

Facts live in an array facts: Triple[].

Eyeling attaches hidden (non-enumerable) index fields:

termFastKey(term) returns a termId (term.__tid) for Iri, Literal, and Blank terms, and null for structured terms (lists, quoted graphs) and variables.

The “fast key” only exists when termFastKey succeeds for all three terms.

7.2 Candidate selection: pick the smallest bucket

When proving a goal with IRI predicate, Eyeling computes candidate facts by:

  1. restricting to predicate bucket
  2. optionally narrowing further by subject or object fast key
  3. choosing the smaller of (p,s) vs (p,o) when both exist

This is a cheap selectivity heuristic. In type-heavy RDF, (p,o) is often extremely selective (e.g., rdf:type + a class IRI), so the PO index can be a major speed win.

7.3 Duplicate detection with fast keys

When adding derived facts, Eyeling uses a fast-path duplicate check when possible:

This still treats blanks correctly: blanks are not interchangeable; the blank label (and thus its __tid) is part of the key.

Chapter 8 — Backward chaining: the proof engine (proveGoals)

Eyeling’s backward prover is an iterative depth-first search (DFS) that looks a lot like Prolog’s SLD resolution, but written explicitly with a stack to avoid JS recursion limits.

8.1 Proof states

A proof state contains:

8.2 The proving loop

At each step:

  1. If no goals remain: emit the current substitution as a solution.
  2. Otherwise:
    • take the first goal
    • apply the current substitution to it
    • attempt to satisfy it in three ways:
      1. built-ins
      2. backward rules
      3. facts

Eyeling’s order is intentional: built-ins often bind variables cheaply; backward rules expand the search tree (and enable recursion); facts are tried last as cheap terminal matches.

8.3 Built-ins: return deltas, not full substitutions

A built-in is evaluated by the engine via the builtin library in lib/builtins.js:

deltas = evalBuiltin(goal0, {}, facts, backRules, ...)
for delta in deltas:
  mark = trail.length
  if applyDeltaToSubst(delta):
    dfs(restGoals)
  undoTo(mark)

Implementation note (performance): in the core DFS, Eyeling applies builtin (and unification) deltas into a single mutable substitution and uses a trail to undo bindings on backtracking. This preserves the meaning of “threading substitutions through a proof”, but avoids allocating and copying full substitution objects on every branch. Empty deltas ({}) are genuinely cheap: they don’t touch the trail and only incur the control-flow overhead of exploring a branch.

Implementation note (performance): as of this version, Eyeling also avoids allocating short-lived substitution objects when matching goals against facts and when unifying a backward-rule head with the current goal. Instead of calling the pure unifyTriple(..., subst) (which clones the substitution on each variable bind), the prover performs an in-place unification directly into the mutable substMut store and records only the newly-bound variable names on the trail. This typically reduces GC pressure significantly on reachability / path-search workloads, where unification is executed extremely frequently.

So built-ins behave like relations that can generate zero, one, or many possible bindings. A list generator might yield many deltas; a numeric test yields zero or one.

8.3.1 Builtin deferral and “vacuous” solutions

Conjunction in N3 is order-insensitive, but many builtins are only useful once some variables are bound by other goals in the same body. When proveGoals is called from forward chaining, Eyeling enables builtin deferral: if a builtin goal can’t make progress yet, it is rotated to the end of the goal list and retried later (with a small cycle guard to avoid infinite rotation).

“Can’t make progress” includes both cases:

That second case matters for “satisfiable but non-enumerating” builtins (e.g., some log: helpers) where early vacuous success would otherwise prevent later goals from ever binding the variables the builtin needs.

8.4 Loop prevention: visited multiset with backtracking

Eyeling avoids obvious infinite recursion by recording each (substituted) goal it is currently trying in a per-branch visited structure. If the same goal is encountered again on the same proof branch, Eyeling skips it.

Implementation notes:

8.5 Backward rules: indexed by head predicate

Backward rules are indexed in backRules.__byHeadPred. When proving a goal with IRI predicate p, Eyeling retrieves:

For each candidate rule:

  1. standardize it apart (fresh variables)
  2. unify the rule head with the goal
  3. append the rule body goals in front of the remaining goals

That “standardize apart” step is essential. Without it, reusing a rule multiple times would accidentally share variables across invocations, producing incorrect bindings.

Implementation note (performance): standardizeRule is called for every backward-rule candidate during proof search.
To reduce allocation pressure, Eyeling reuses a single fresh Var(...) object per original variable name within one standardization pass (all occurrences of ?x in the rule become the same fresh ?x__N object). This is semantics-preserving — it still “separates” invocations — but it avoids creating many duplicate Var objects when a variable appears repeatedly in a rule body.

8.6 Substitution size on deep proofs

The trail-based substitution store removes the biggest accidental quadratic cost (copying a growing substitution object at every step).
In deep and branchy searches, the substitution trail still grows, and long variable-to-variable chains increase the work done by applySubstTerm.

Eyeling currently keeps the full trail as-is during search. When emitting a solution, it runs a lightweight compaction pass (via gcCollectVarsInGoals(...) / gcCompactForGoals(...)) so only bindings reachable from the answer variables and remaining goals are kept. It still does not perform general substitution composition/normalization during search.

Chapter 9 — Forward chaining: saturation, skolemization, and meta-rules (forwardChain)

Forward chaining is Eyeling’s outer control loop. It is where facts get added and the closure grows.

9.1 The shape of saturation

Eyeling loops until no new facts are added. Inside that loop, it scans every forward rule and tries to fire it.

A simplified view:

repeat
  changed = false
  for each forward rule r:
    sols = proveGoals(r.premise, facts, backRules)
    for each solution s:
      for each head triple h in r.conclusion:
        inst = applySubst(h, s)
        inst = skolemizeHeadBlanks(inst)
        if inst is ground and new:
          add inst to facts
          changed = true
until not changed

9.2 Strict-ground head optimization

There is a nice micro-compiler optimization in runFixpoint():

If a rule’s head is strictly ground (no vars, no blanks, no open lists, even inside formulas), and it contains no head blanks, then the head does not depend on which body solution you choose.

In that case:

This is a surprisingly effective optimization for “axiom-like” rules with constant heads.

9.3 Existentials: skolemizing head blanks

Blank nodes in the rule head represent existentials: “there exists something such that…”

Eyeling handles this by replacing head blank labels with fresh blank labels of the form:

But it does something subtle and important: it caches skolemization per (rule firing, head blank label), so that the same firing instance doesn’t keep generating new blanks across outer iterations.

The “firing instance” is keyed by a deterministic string derived from the instantiated body (“firingKey”). This stabilizes the closure and prevents “existential churn.”

Implementation note (performance): the firing-instance key is computed in a hot loop, so firingKey(...) builds a compact string via concatenation rather than JSON.stringify. If you change what counts as a distinct “firing instance”, update the key format and the skolem cache together.

Implementation: deterministic Skolem IDs live in lib/skolem.js; the per-firing cache and head-blank rewriting are implemented in lib/engine.js.

9.4 Inference fuses: { ... } => false

A rule whose conclusion is false is treated as a hard failure. During forward chaining:

This is Eyeling’s way to express hard consistency checks and detect inconsistencies.

9.5 Rule-producing rules (meta-rules)

Eyeling treats certain derived triples as new rules:

So these are “rule triples”:

{ ... } log:implies { ... }.
true log:implies { ... }.
{ ... } log:impliedBy true.

When such a triple is derived in a forward rule head:

  1. Eyeling adds it as a fact (so you can inspect it), and
  2. it promotes it into a live rule by constructing a new Rule object and inserting it into the forward or backward rule list.

This is meta-programming: your rules can generate new rules during reasoning.

Implementation note (performance): rule triples are often derived repeatedly (especially inside loops).
To keep promotion cheap, Eyeling maintains a Set of canonical rule keys for both the forward-rule list and the backward-rule list. Promotion checks membership in O(1) time instead of scanning the rule arrays and doing structural comparisons each time.

Chapter 10 — Scoped closure, priorities, and log:conclusion

Some log: built-ins talk about “what is included in the closure” or “collect all solutions.” These are tricky in a forward-chaining engine because the closure is evolving.

Eyeling addresses this with a disciplined two-phase strategy and an optional priority mechanism.

10.1 The two-phase outer loop (Phase A / Phase B)

Forward chaining runs inside an outer loop that alternates:

This produces deterministic behavior for scoped operations: they observe a stable snapshot, not a moving target.

Implementation note (performance): the two-phase scheme is only needed when the program actually uses scoped built-ins. If no rule contains log:collectAllIn, log:forAllIn, log:includes, or log:notIncludes, Eyeling now skips Phase B entirely and runs only a single saturation. This avoids re-running the forward fixpoint and can prevent a “query-like” forward rule (one whose body contains an expensive backward proof search) from being executed twice.

Implementation note (performance): in Phase A there is no snapshot, so scoped built-ins (and priority-gated scoped queries) are guaranteed to “delay” by failing.
Instead of proving the entire forward-rule body only to fail at the end, Eyeling precomputes whether a forward rule depends on scoped built-ins and skips it until a snapshot exists and the requested closure level is reached. This can avoid very expensive proof searches in programs that combine recursion with log:*In built-ins.

10.2 Priority-gated closure levels

Eyeling introduces a scopedClosureLevel counter:

Some built-ins interpret a positive integer literal as a requested priority:

If a rule requests priority N, Eyeling delays that builtin until scopedClosureLevel >= N.

In practice this allows rule authors to write “don’t run this scoped query until the closure is stable enough” and is what lets Eyeling iterate safely when rule-producing rules introduce new needs.

10.3 log:conclusion: local deductive closure of a formula

log:conclusion is handled in a particularly elegant way:

Notably, log:impliedBy inside the formula is treated as forward implication too for closure computation (and also indexed as backward to help proving).

This makes formulas a little world you can reason about as data.

Chapter 11 — Built-ins as a standard library (lib/builtins.js)

Built-ins are where Eyeling stops being “just a Datalog engine” and becomes a practical N3 tool.

Implementation note: builtin code lives in lib/builtins.js and is wired into the prover by the engine via makeBuiltins(deps) (dependency injection keeps the modules loosely coupled).

11.1 How Eyeling recognizes built-ins

A predicate is treated as builtin if:

Super restricted mode exists to let you treat all other predicates as ordinary facts/rules without any built-in evaluation.

Note on log:query: Eyeling also recognizes a special top-level directive of the form {...} log:query {...}. to select which results to print. This is not a builtin predicate (it is not evaluated as part of goal solving); it is handled by the parser/CLI/output layer. See §11.3.5 below and Chapter 13 for details.

11.2 Built-ins return multiple solutions

Every builtin returns a list of substitution deltas.

That means built-ins can be:

List operations are a common source of generators; numeric comparisons are tests.

Below is a drop-in replacement for §11.3 “A tour of builtin families” that aims to be fully self-contained and to cover every builtin currently implemented in lib/builtins.js (including the rdf:first / rdf:rest aliases).

11.3 A tour of builtin families

Eyeling’s builtins are best thought of as foreign predicates: they look like ordinary N3 predicates in your rules, but when the engine tries to satisfy a goal whose predicate is a builtin, it does not search the fact store. Instead, it calls a piece of JavaScript that implements the predicate’s semantics.

That one sentence explains a lot of “why does it behave like that?”:

11.3.0 Reading builtin “signatures” in this handbook

The N3 Builtins tradition often describes builtins using “schema” annotations like:

Eyeling is a little more pragmatic: it implements the spirit of these schemas, but it also has several “engineering” conventions that appear across many builtins:

  1. Variables (?X) may be bound by a builtin if the builtin is written to do so.
  2. Blank nodes ([] / _:) are frequently treated as “don’t care” placeholders. Many builtins accept a blank node in an output position and simply succeed without binding.
  3. Fully unbound relations are usually not enumerated. If both sides are unbound and enumerating solutions would be infinite (or huge), a number of builtins treat that situation as “satisfiable” and succeed once without binding anything. (This is mainly to keep meta-tests and some N3 conformance cases happy.)

With that, we can tour the builtin families as Eyeling actually implements them.

11.3.1 crypto: — digest functions (Node-only)

These builtins hash a string and return a lowercase hex digest as a plain string literal.

crypto:sha, crypto:md5, crypto:sha256, crypto:sha512

Shape: $literal crypto:sha256 $digest

Semantics (Eyeling):

Important runtime note: Eyeling uses Node’s crypto module. If crypto is not available (e.g., in some browser builds), these builtins simply fail (return no solutions).

Example:

"hello" crypto:sha256 ?d.
# ?d becomes "2cf24dba5...<snip>...9824"

11.3.2 math: — numeric and numeric-like relations

Eyeling’s math: builtins fall into three broad categories:

  1. Comparisons: test-style predicates (>, <, =, …).
  2. Arithmetic on numbers: sums, products, division, rounding, etc.
  3. Unary analytic functions: trig/hyperbolic functions and a few helpers.

A key design choice: Eyeling parses numeric terms fairly strictly, but comparisons accept a wider “numeric-like” domain including durations and date/time values in some cases.

11.3.2.1 Numeric comparisons

These builtins succeed or fail; they do not introduce new bindings.

Shapes:

$a math:greaterThan $b.
$a math:equalTo $b.

Eyeling also accepts an older cwm-ish variant where the subject is a 2-element list:

( $a $b ) math:greaterThan true.   # (supported as a convenience)

Accepted term types (Eyeling):

Edge cases:

These are pure tests. In forward rules, if a test builtin is encountered before its inputs are bound and it fails, Eyeling may defer it and try other goals first; once variables become bound, the test is retried.

11.3.2.2 Arithmetic on lists of numbers

These are “function-like” relations where the subject is usually a list and the object is the result.

math:sum

Shape: ( $x1 $x2 ... ) math:sum $total

Eyeling also supports a small, EYE-style convenience for timestamp arithmetic:

math:product

Shape: ( $x1 $x2 ... ) math:product $total

math:difference

This one is more interesting because Eyeling supports a couple of mixed “numeric-like” cases.

Shape: ( $a $b ) math:difference $c

Eyeling supports:

  1. Numeric subtraction: c = a - b.
  2. DateTime difference: (dateTime1 dateTime2) math:difference duration
    • Produces an xsd:duration in a seconds-only lexical form such as "PT900S"^^xsd:duration.
    • This avoids ambiguity around month/year day-length and still plays well with math:lessThan, math:greaterThan, etc. because Eyeling’s numeric comparison builtins treat xsd:duration as seconds.
  3. DateTime minus duration: (dateTime durationOrSeconds) math:difference dateTime
    • Subtracts a duration from a dateTime and yields a new dateTime.

If the types don’t fit any supported case, the builtin fails.

math:quotient

Shape: ( $a $b ) math:quotient $q

math:integerQuotient

Shape: ( $a $b ) math:integerQuotient $q

math:remainder

Shape: ( $a $b ) math:remainder $r

math:rounded

Shape: $x math:rounded $n

11.3.2.3 Exponentiation and unary numeric relations

math:exponentiation

Shape: ( $base $exp ) math:exponentiation $result

This is a pragmatic inversion, not a full algebra system.

Unary “math relations” (often invertible)

Eyeling implements these as a shared pattern: if the subject is numeric, compute object; else if the object is numeric, compute subject via an inverse function; if both sides are unbound, succeed once (don’t enumerate).

Example:

"0"^^xsd:double math:cos ?c.      # forward
?x math:cos "1"^^xsd:double.      # reverse (principal acos)

Inversion uses principal values (e.g., asin, acos, atan) and does not attempt to enumerate periodic families of solutions.

11.3.3 time: — dateTime inspection and “now”

Eyeling’s time builtins work over xsd:dateTime lexical forms. They are deliberately simple: they extract components from the lexical form rather than implementing a full time zone database.

Implementation: these helpers live in lib/time.js and are called from lib/engine.js’s builtin evaluator.

Component extractors

Shape: $dt time:month $m

Semantics:

time:timeZone

Shape: $dt time:timeZone $tz

Returns the trailing zone designator:

It yields a plain string literal (and also accepts typed xsd:string literals).

time:localTime

Shape: "" time:localTime ?now

Binds ?now to the current local time as an xsd:dateTime literal.

Two subtle but important engineering choices:

  1. Eyeling memoizes “now” per reasoning run so that repeated uses in one run don’t drift.
  2. Eyeling supports a fixed “now” override (used for deterministic tests).

11.3.4 list: — list structure, iteration, and higher-order helpers

Eyeling has a real internal list term (ListTerm) that corresponds to N3’s (a b c) surface syntax.

RDF collections (rdf:first / rdf:rest) are materialized

N3 and RDF can also express lists as linked blank nodes using rdf:first / rdf:rest and rdf:nil. Eyeling materializes such structures into internal list terms before reasoning so that list:* builtins can operate uniformly.

For convenience and compatibility, Eyeling treats:

Core list destructuring

list:first (and rdf:first)

Shape: (a b c) list:first a

list:rest (and rdf:rest)

Shape: (a b c) list:rest (b c)

Eyeling supports both:

For open lists, “rest” preserves openness:

list:firstRest

This is a very useful “paired” view of a list.

Forward shape: (a b c) list:firstRest (a (b c))

Backward shapes (construction):

This is the closest thing to Prolog’s [H|T] in Eyeling.

Implementation note (performance): list:firstRest is a hot builtin in many recursive list-building programs (including path finding). Eyeling constructs the new prefix using pre-sized arrays and simple loops (instead of spread syntax) to reduce transient allocations.

Membership and iteration (multi-solution builtins)

These builtins can yield multiple solutions.

list:member

Shape: (a b c) list:member ?x

Generates one solution per element, unifying the object with each member.

list:in

Shape: ?x list:in (a b c)

Same idea, but the list is in the object position and the subject is unified with each element.

list:iterate

Shape: (a b c) list:iterate ?pair

Generates (index value) pairs with 0-based indices:

A nice ergonomic detail: the object may be a pattern such as:

(a b c) list:iterate ( ?i "b" ).

In that case Eyeling unifies ?i with 1 and checks the value part appropriately.

list:memberAt

Shape: ( (a b c) 1 ) list:memberAt b

The subject must be a 2-element list: (listTerm indexTerm).

Eyeling can use this relationally:

Indices are 0-based.

Transformations and queries

list:length

Shape: (a b c) list:length 3

Returns the length as an integer token literal.

A small but intentional strictness: if the object is already ground, Eyeling does not accept “integer vs decimal equivalences” here; it wants the exact integer notion.

list:last

Shape: (a b c) list:last c

Returns the last element of a non-empty list.

list:reverse

Reversible in the sense that either side may be the list:

It does not enumerate arbitrary reversals; it’s a deterministic transform once one side is known.

list:remove

Shape: ( (a b a c) a ) list:remove (b c)

Removes all occurrences of an item from a list.

Important requirement: the item to remove must be ground (fully known) before the builtin will run.

list:notMember (test)

Shape: (a b c) list:notMember x

Succeeds iff the object cannot be unified with any element of the subject list. As a test, it typically works best once its inputs are bound; in forward rules Eyeling may defer it if it is reached before bindings are available.

list:append

This is list concatenation, but Eyeling implements it in a pleasantly relational way.

Forward shape: ( (a b) (c) (d e) ) list:append (a b c d e)

Subject is a list of lists; object is their concatenation.

Splitting (reverse-ish) mode: If the object is a concrete list, Eyeling tries all ways of splitting it into the given number of parts and unifying each part with the corresponding subject element. This can yield multiple solutions and is handy for logic programming patterns.

list:sort

Sorts a list into a deterministic order.

Like reverse, this is “reversible” only in the sense that if one side is a list, the other side can be unified with its sorted form.

list:map (higher-order)

This is one of Eyeling’s most powerful list builtins because it calls back into the reasoner.

Shape: ( (x1 x2 x3) ex:pred ) list:map ?outList

Semantics:

  1. The subject is a 2-element list: (inputList predicateIri).
  2. inputList must be ground.

  3. For each element el in the input list, Eyeling proves the goal:

    el predicateIri ?y.

    using the full engine (facts, backward rules, and builtins).

  4. All resulting ?y values are collected in proof order and concatenated into the output list.
  5. If an element produces no solutions, it contributes nothing.

This makes list:map a compact “query over a list” operator.

11.3.5 log: — unification, formulas, scoping, and meta-level control

The log: family is where N3 stops being “RDF with rules” and becomes a meta-logic. Eyeling supports the core operators you need to treat formulas as terms, reason inside quoted graphs, and compute closures.

Equality and inequality

log:equalTo

Shape: $x log:equalTo $y

This is simply term unification: it succeeds if the two terms can be unified and returns any bindings that result.

log:notEqualTo (test)

Succeeds iff the terms cannot be unified. No new bindings.

Working with formulas as terms

In Eyeling, a quoted formula { ... } is represented as a GraphTerm whose content is a list of triples (and, when parsed from documents, rule terms can also appear as log:implies / log:impliedBy triples inside formulas).

log:conjunction

Shape: ( F1 F2 ... ) log:conjunction F

log:conclusion

Shape: F log:conclusion C

Computes the deductive closure of the formula F using only the information inside F:

Eyeling caches log:conclusion results per formula object, so repeated calls with the same formula term are cheap.

Dereferencing and parsing (I/O flavored)

These builtins reach outside the current fact set. They are synchronous by design.

log:content

Shape: <doc> log:content ?txt

log:semantics

Shape: <doc> log:semantics ?formula

Dereferences and parses the remote/local resource as N3/Turtle-like syntax, returning a formula.

A nice detail: top-level rules in the parsed document are represented as data inside the returned formula using log:implies / log:impliedBy triples between formula terms. This means you can treat “a document plus its rules” as a single first-class formula object.

log:semanticsOrError

Like log:semantics, but on failure it returns a string literal such as:

This is convenient in robust pipelines where you want logic that can react to failures.

log:parsedAsN3

Shape: " ...n3 text... " log:parsedAsN3 ?formula

Parses an in-memory string as N3 and returns the corresponding formula.

Type inspection

log:rawType

Returns one of four IRIs:

Literal constructors

These two are classic N3 “bridge” operators between structured data and concrete RDF literal forms.

log:dtlit

Relates a datatype literal to a pair (lex datatypeIri).

Language-tagged strings are normalized: they are treated as having datatype rdf:langString.

log:langlit

Relates a language-tagged literal to a pair (lex langTag).

Rules as data: introspection

log:implies and log:impliedBy

As syntax, Eyeling parses {A} => {B} and {A} <= {B} into internal forward/backward rules.

As builtins, log:implies and log:impliedBy let you inspect the currently loaded rule set:

Each enumerated rule is standardized apart (fresh variable names) before unification so you can safely query over it.

Top-level directive: log:query (output selection)

Shape (top level only):

{ ...premise... } log:query { ...conclusion... }.

log:query is best understood as an output projection, not as a rule and not as a normal builtin:

This is “forward-rule-like” in spirit (premise ⇒ conclusion), but the instantiated conclusion triples are not added back into the fact store; they are just what Eyeling prints.

Important details:

Example (project a result set):

@prefix : <urn:ex:>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

{ :a :p ?x } => { :a :q ?x }.
:a :p :b.

{ :a :q ?x } log:query { :result :x ?x }.

Output (only):

:result :x :b .

Scoped proof inside formulas: log:includes and friends

log:includes

Shape: Scope log:includes GoalFormula

This proves all triples in GoalFormula as goals, returning the substitutions that make them provable.

Eyeling has two modes:

  1. Explicit scope graph: if Scope is a formula {...}
    • Eyeling reasons only inside that formula (its triples are the fact store).
    • External rules are not used.
  2. Priority-gated global scope: otherwise
    • Eyeling uses a frozen snapshot of the current global closure.
    • The “priority” is read from the subject if it’s a positive integer literal N.
    • If the closure level is below N, the builtin “delays” by failing at that point in the search.

This priority mechanism exists because Eyeling’s forward chaining runs in outer iterations with a “freeze snapshot then evaluate scoped builtins” phase. The goal is to make scoped meta-builtins stable and deterministic: they query a fixed snapshot rather than chasing a fact store that is being mutated mid-iteration.

Also supported:

log:notIncludes (test)

Negation-as-failure version: it succeeds iff log:includes would yield no solutions (under the same scoping rules).

log:collectAllIn

Shape: ( ValueTemplate WhereFormula OutList ) log:collectAllIn Scope

This is essentially a list-producing “findall”.

log:forAllIn (test)

Shape: ( WhereFormula ThenFormula ) log:forAllIn Scope

For every solution of WhereFormula, ThenFormula must be provable under the bindings of that solution. If any witness fails, the builtin fails. No bindings are returned.

As a pure test (no returned bindings), this typically works best once its inputs are bound; in forward rules Eyeling may defer it if it is reached too early.

Skolemization and URI casting

log:skolem

Shape: $groundTerm log:skolem ?iri

Deterministically maps a ground term to a Skolem IRI in Eyeling’s well-known namespace. This is extremely useful when you want a repeatable identifier derived from structured content.

log:uri

Bidirectional conversion between IRIs and their string form:

Side effects and output directives

log:trace

Always succeeds once and prints a debug line to stderr:

<s> TRACE <o>

using the current prefix environment for pretty printing.

Implementation: this is implemented by lib/trace.js and called from lib/engine.js.

log:outputString

As a goal, this builtin simply checks that the terms are sufficiently bound/usable and then succeeds. The actual “printing” behavior is handled by the CLI:

This is a pure test/side-effect marker (it shouldn’t drive search; it should merely validate that strings exist once other reasoning has produced them). In forward rules Eyeling may defer it if it is reached before the terms are usable.

11.3.6 string: — string casting, tests, and regexes

Eyeling implements string builtins with a deliberate interpretation of “domain is xsd:string”:

Construction and concatenation

string:concatenation

Shape: ( s1 s2 ... ) string:concatenation s

Casts each element to a string and concatenates.

string:format

Shape: ( fmt a1 a2 ... ) string:format out

A tiny sprintf subset:

Containment and prefix/suffix tests

All are pure tests: they succeed or fail.

Case-insensitive equality tests

Lexicographic comparisons

These compare JavaScript strings directly, i.e., Unicode code unit order (practically “lexicographic” for many uses, but not locale-aware collation).

Regex-based tests and extraction

Eyeling compiles patterns using JavaScript RegExp, with a small compatibility layer:

string:matches / string:notMatches (tests)

Shape: data string:matches pattern

Tests whether pattern matches data.

string:replace

Shape: ( data pattern replacement ) string:replace out

string:scrape

Shape: ( data pattern ) string:scrape out

Matches the regex once and returns the first capturing group (group 1). If there is no match or no group, it fails.

11.4 log:outputString as a controlled side effect

From a logic-programming point of view, printing is awkward: if you print during proof search, you risk producing output along branches that later backtrack, or producing the same line multiple times in different derivations. Eyeling avoids that whole class of problems by treating “output” as data.

The predicate log:outputString is the only officially supported “side-effect channel”, and even it is handled in two phases:

  1. During reasoning (declarative phase):
    log:outputString behaves like a pure test builtin (implemented in lib/builtins.js): it succeeds when its arguments are well-formed and sufficiently bound (notably, when the object is a string literal that can be emitted). Importantly, it does not print anything at this time. If a rule derives a triple like:

    :k log:outputString "Hello\n".

then that triple simply becomes part of the fact base like any other fact.

  1. After reasoning (rendering phase): Once saturation finishes, Eyeling scans the final closure for log:outputString facts and renders them deterministically (this post-pass lives in lib/explain.js). Concretely, the CLI collects all such triples, orders them in a stable way (using the subject as a key so output order is reproducible), and concatenates their string objects into the final emitted text.

This separation is not just an aesthetic choice; it preserves the meaning of logic search:

In short: Eyeling makes log:outputString safe by refusing to treat it as an immediate effect. It is a declarative output fact whose concrete rendering is a final, deterministic post-processing step.

Chapter 12 — Dereferencing and web-like semantics (lib/deref.js)

Some N3 workflows treat IRIs as pointers to more knowledge. Eyeling supports this with:

deref.js is deliberately synchronous so the engine can remain synchronous.

12.1 Two environments: Node vs browser/worker

12.2 Caching

Dereferencing is cached by IRI-without-fragment (fragments are stripped). There are separate caches for:

This is both a performance and a stability feature: repeated log:semantics calls in backward proofs won’t keep refetching.

12.3 HTTPS enforcement

Eyeling can optionally rewrite http://… to https://… before dereferencing (CLI --enforce-https, or API option). This is a pragmatic “make more things work in modern environments” knob.

Chapter 13 — Printing, proofs, and the user-facing output

Once reasoning is done (or as it happens in streaming mode), Eyeling converts derived facts back to N3.

13.1 Printing terms and triples (lib/printing.js)

Printing handles:

The printer is intentionally simple; it prints what Eyeling can parse.

13.2 Proof comments: local justifications, not full proof trees

When enabled, Eyeling prints a compact comment block per derived triple:

It’s a “why this triple holds” explanation, not a globally exported proof graph.

Implementation note: the engine records lightweight DerivedFact objects during forward chaining, and lib/explain.js (via makeExplain(...)) is responsible for turning those objects into the human-readable proof comment blocks.

13.3 Streaming derived facts

The engine’s reasonStream API can accept an onDerived callback. Each time a new forward fact is derived, Eyeling can report it immediately.

This is especially useful in interactive demos (and is the basis of the playground streaming tab).

Chapter 14 — Entry points: CLI, bundle exports, and npm API

Eyeling exposes itself in three layers.

14.1 The bundled CLI (eyeling.js)

The bundle contains the whole engine. The CLI path is the “canonical behavior”:

14.1.1 CLI options at a glance

The current CLI supports a small set of flags (see lib/cli.js):

14.2 lib/entry.js: bundler-friendly exports

lib/entry.js exports:

14.3 index.js: the npm API wrapper

The npm reason(...) function does something intentionally simple and robust:

This ensures the API matches the CLI perfectly and keeps the public surface small.

One practical implication:

Chapter 15 — A worked example: Socrates, step by step

Consider:

@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix : <http://example.org/socrates#>.

:Socrates a :Human.
:Human rdfs:subClassOf :Mortal.

{ ?S a ?A. ?A rdfs:subClassOf ?B } => { ?S a ?B }.

What Eyeling does:

  1. Parsing yields two facts:
    • (:Socrates rdf:type :Human)
    • (:Human rdfs:subClassOf :Mortal) and one forward rule:
    • premise goals: ?S a ?A, ?A rdfs:subClassOf ?B
    • head: ?S a ?B

  2. Forward chaining scans the rule and calls proveGoals on the body.

  3. Proving ?S a ?A matches the first fact, producing { S = :Socrates, A = :Human }.

  4. With that substitution, the second goal becomes :Human rdfs:subClassOf ?B. It matches the second fact, extending to { B = :Mortal }.

  5. Eyeling instantiates the head ?S a ?B → :Socrates a :Mortal.

  6. The triple is ground and not already present, so it is added and (optionally) printed.

That’s the whole engine in miniature: unify, compose substitutions, emit head triples.

Chapter 16 — Extending Eyeling (without breaking it)

Eyeling is small, which makes it pleasant to extend — but there are a few invariants worth respecting.

16.1 Adding a builtin

Most extensions belong in lib/builtins.js (inside evalBuiltin):

A small architectural note: lib/builtins.js is initialized by the engine via makeBuiltins(deps). It receives hooks (unification, proving, deref, scoped-closure helpers, …) instead of importing the engine directly, which keeps the module graph acyclic and makes browser bundling easier.

If your builtin needs a stable view of the scoped closure, follow the scoped-builtin pattern:

And if your builtin is “forward-only” (needs inputs bound), it’s fine to fail early until inputs are available — forward rule proving enables builtin deferral, so the goal can be retried later in the same conjunction.

16.2 Adding new term shapes

If you add a new Term subclass, you’ll likely need to touch:

16.3 Parser extensions

If you extend parsing, preserve the Rule invariants:

Epilogue: the philosophy of this engine

Eyeling’s codebase is compact because it chooses one powerful idea and leans into it:

Use backward proving as the “executor” for forward rule bodies.

That design makes built-ins and backward rules feel like a standard library of relations, while forward chaining still gives you the determinism and “materialized closure” feel of Datalog.

If you remember only one sentence from this handbook, make it this:

Eyeling is a forward-chaining engine whose rule bodies are solved by a Prolog-like backward prover with built-ins.

Everything else is engineering detail — interesting, careful, sometimes subtle — but always in service of that core shape.

Appendix A — Eyeling user notes

This appendix is a compact, user-facing reference for running Eyeling and writing inputs that work well. For deeper explanations and implementation details, follow the chapter links in each section.

A.1 Install and run

Eyeling is distributed as an npm package.

See also: Chapter 14 — Entry points: CLI, bundle exports, and npm API.

A.2 What Eyeling prints

By default, Eyeling prints newly derived forward facts (the heads of fired => rules), serialized as N3. It does not reprint your input facts.

If the input contains one or more top-level log:query directives:

{ ...premise... } log:query { ...conclusion... }.

Eyeling still computes the saturated forward closure, but it prints only the unique instantiated conclusion triples of those log:query directives (instead of all newly derived facts). This is useful when you want a forward-rule-like projection of results.

For proof/explanation output and output modes, see:

A.3 CLI quick reference

The authoritative list is always:

eyeling --help

Options:

  -a, --ast                    Print parsed AST as JSON and exit.
  -d, --deterministic-skolem   Make log:skolem stable across reasoning runs.
  -e, --enforce-https          Rewrite http:// IRIs to https:// for log dereferencing builtins.
  -h, --help                   Show this help and exit.
  -p, --proof-comments         Enable proof explanations.
  -r, --strings                Print log:outputString strings (ordered by key) instead of N3 output.
  -s, --super-restricted       Disable all builtins except => and <=.
  -t, --stream                 Stream derived triples as soon as they are derived.
  -v, --version                Print version and exit.

Note: when log:query directives are present, Eyeling cannot stream output (the selected results depend on the saturated closure), so --stream has no effect in that mode.

See also:

A.4 N3 syntax notes that matter in practice

Eyeling implements a practical N3 subset centered around facts and rules.

Quoted graphs/formulas use { ... }. Inside a quoted formula, directive scope matters:

For the formal grammar, see the N3 spec grammar:

See also:

A.5 Builtins

Eyeling supports a built-in “standard library” across namespaces like log:, math:, string:, list:, time:, crypto:.

References:

If you are running untrusted inputs, consider --super-restricted to disable all builtins except implication.

A.6 Skolemization and log:skolem

When forward rule heads contain blank nodes (existentials), Eyeling replaces them with generated Skolem IRIs so derived facts are ground.

See:

A.7 Networking and log:semantics

log:content, log:semantics, and related builtins dereference IRIs and parse retrieved content. This is powerful, but it is also I/O.

See:

Safety tip:

A.8 Embedding Eyeling in JavaScript

If you depend on Eyeling as a library, the package exposes:

See:

A.9 Further reading

If you want to go deeper into N3 itself and the logic/programming ideas behind Eyeling, these are good starting points:

N3 / Semantic Web specs and reports:

Logic & reasoning background (Wikipedia):

Appendix B — Notation3: when facts can carry their own logic

RDF succeeded by making a radical design choice feel natural: reduce meaning to small, uniform statements—triples—that can be published, merged, and queried across boundaries. A triple does not presume a database schema, a programming language, or a particular application. It presumes only that names (IRIs) can be shared, and that graphs can be combined.

That strength also marks RDF’s limit. The moment a graph is expected to do something—normalize values, reconcile vocabularies, derive implied relationships, enforce a policy, compute a small transformation—logic tends to migrate into code. The graph becomes an inert substrate while the decisive semantics hide in scripts, services, ETL pipelines, or bespoke rule engines. What remains portable is the data; what often becomes non-portable is the meaning.

Notation3 (N3) sits precisely at that seam. It remains a readable way to write RDF, but it also treats graphs themselves as objects that can be described, matched, and related. The N3 Community Group’s specification presents N3 as an assertion and logic language that extends RDF rather than replacing it: https://w3c.github.io/N3/spec/.

The essential move is quotation: writing a graph inside braces as a thing that can be discussed. Once graphs can be quoted, rules become graph-to-graph transformations. The familiar implication form, { … } => { … } ., reads as a piece of prose: whenever the antecedent pattern holds, the consequent pattern follows. Tim Berners-Lee’s design note frames this as a web-friendly logic with variables and nested graphs: https://www.w3.org/DesignIssues/Notation3.html.

This style of rule-writing makes rules first-class, publishable artifacts. It keeps the unit of exchange stable. Inputs are RDF graphs; outputs are RDF graphs. Inference produces new triples rather than hidden internal state. Rule sets can be versioned alongside data, reviewed as text, and executed by different engines that implement the same semantics. That portability theme runs back to the original W3C Team Submission: https://www.w3.org/TeamSubmission/n3/.

Practical reasoning also depends on computation: lists, strings, math, comparisons, and the other “small operations” that integration work demands. N3 addresses this by standardizing built-ins—predicates with predefined behavior that can be used inside rule bodies while preserving the declarative, graph-shaped idiom. The built-ins report is here: https://w3c.github.io/N3/reports/20230703/builtins.html.

Testing is where rule languages either converge or fragment. Different implementations can drift on scoping, blank nodes, quantification, and built-in behavior. N3’s recent direction has been toward explicit, testable semantics, documented separately as model-theoretic foundations: https://w3c.github.io/N3/reports/20230703/semantics.html.

In that context, public conformance suites become more than scoreboards: they are the mechanism by which interoperability becomes measurable. The community test suite lives at https://codeberg.org/phochste/notation3tests/, with comparative results published in its report: https://codeberg.org/phochste/notation3tests/src/branch/main/reports/report.md.

The comparison with older tools is historically instructive. Cwm (Closed World Machine) was an early, influential RDF data processor and forward-chaining reasoner—part of the lineage that treated RDF (often written in N3) as something executable: https://www.w3.org/2000/10/swap/doc/cwm.

What motivates Notation3, in the end, is architectural restraint. It refuses to let “logic” become merely a private feature of an application stack. It keeps meaning close to the graph: rules are expressed as graph patterns; results are expressed as triples; computation is pulled in through well-defined built-ins rather than arbitrary code. This produces a style of working where integration and inference are not sidecar scripts, but publishable artifacts—documents that can be inspected, shared, tested, and reused.

In that sense, N3 is less a bid to make the web “smarter” than a bid to make meaning portable: not only facts that travel, but also the explicit steps by which facts can be connected, extended, and made actionable—without abandoning the simplicity that made triples travel in the first place.

Appendix C — N3 beyond Prolog: logic for RDF-style graphs

Notation3 (N3) rule sets often look similar to Prolog at the surface: they use variables, unification, and implication-style rules (“if these patterns match, then these patterns follow”). N3 is typically used in a different setting: instead of a single program operating over a single local database, N3 rules and data are commonly written as documents that can be published, shared, merged, and referenced across systems.

In practice, that setting is reflected in several common features of N3-style rule writing:

Engines can combine execution styles in different ways. One common pattern is to use a Prolog-like backward-chaining prover to satisfy rule bodies, while still using forward chaining to add the instantiated conclusions to the fact set until no new facts are produced.

Appendix D — LLM + Eyeling: A Repeatable Logic Toolchain

Eyeling is a deterministic N3 engine: given facts and rules, it derives consequences to a fixpoint using forward rules proved by a backward engine. That makes it a good “meaning boundary” for LLM-assisted workflows: the LLM can draft and refactor N3, but Eyeling is what decides what follows.

A practical pattern is to treat the LLM as a syntax-and-structure generator and Eyeling as the semantic validator.

1) Constrain the LLM to output compilable N3

If the LLM is allowed to emit prose or “almost N3”, you’ll spend your time cleaning up. Instead, require:

This is less about prompt craft and more about creating a stable interface between a text generator and a compiler-like consumer.

2) Use Eyeling as the compile check and the semantic check

Run Eyeling immediately after generation:

Eyeling explicitly supports inference fuses: a forward rule with head false is a hard failure. This is extremely useful as a guardrail when you want “never allow X” constraints to stop the run.

Example fuse:

@prefix : <http://example/> .

{ ?u :role :Admin.
  ?u :disabled true.
} => false.

If you don’t want “stop the world”, derive a :Violation fact instead, and keep going.

3) Make the workflow test-driven (golden closures)

The most robust way to keep LLM-generated logic plausible is to make it live under tests:

This turns rule edits into a normal change-management loop: diffs are explicit, reviewable, and reproducible.

4) Use proofs/traces as the input to the LLM, not the other way around

If you want a natural-language explanation, don’t ask the model to “explain the rules from memory”. Instead:

  1. Run Eyeling with proof/trace enabled (Eyeling has explicit tracing hooks and proof-comment support in its output pipeline).
  2. Give the LLM the derived triples + proof comments and ask it to summarize:
    • what was derived,
    • which rule(s) fired,
    • which premises mattered.

This keeps explanations anchored to what Eyeling actually derived.

5) The refinement loop: edits are N3 diffs, not “better prompting”

When output looks wrong, the fix should be a change in the artifact:

Then regenerate/rewrite only the N3, rerun Eyeling, and review the diff.

A prompt shape that tends to behave well

A simple structure that keeps the LLM honest:

The point isn’t that the LLM is “right”; it’s that Eyeling makes the result checkable, and the artifact becomes a maintainable program rather than a one-off generation.

This site is open source. Improve this page.