Logic and Computation¶
This video walks through the concepts on this page with live terminal demonstrations and auto-generated graph diagrams. Section links (🎬) throughout the page jump to the corresponding part of the video.
zelph is a logic programming system, but not in the traditional sense. Where Prolog operates on terms and Datalog on flat relations, zelph stores everything — facts, rules, predicates, even numbers — as structures in a single semantic network. Computation does not happen outside the graph; it emerges from the graph, through rule-driven inference over its topology.
This page introduces zelph's reasoning capabilities from a logic programming perspective. For the basic syntax of facts, sets, and lists, see Core Concepts. For a hands-on quick start, see the Quick Start Guide.
Positioning: Forward Chaining over Graphs¶
zelph's inference engine performs forward chaining (bottom-up evaluation), similar to Datalog or production rule systems. When a new fact is asserted or a rule is defined, the engine immediately checks whether any rule conditions are newly satisfied and derives all possible consequences. This process repeats until a fixed point is reached — no further facts can be derived.
This is fundamentally different from Prolog's approach of top-down, goal-driven search relying on backtracking. zelph does not seek proofs; instead, it materializes every fact that can be derived within the graph. Formally, this constitutes a least-fixed-point computation on the graph's Herbrand base: start with the facts that are asserted, apply all rules to derive new facts, continue iteratively until no further additions emerge. The compromise is deliberate: forward chaining aligns seamlessly with knowledge graphs (where facts are added over time, for instance, via Wikidata imports). The fixpoint remains finite provided no rule introduces new nodes: a rule whose consequence includes neither a fresh variable, a nested term, nor a collection literal only relates nodes that already exist. zelph does not check this constraint. A nested term in a consequence – (s of X), or the arithmetic's (D cons T) – acts as a function symbol: the mathematical modules intentionally construct such terms and bound them via gating (refer to the header of symbolic-core.zph), whereas a rule that constructs a term from its own condition runs away. A collection literal in a consequence also functions as a function symbol: a firing generates a collection per binding, and a rule whose collection flows back into its own binding never terminates either.
What sets zelph apart from both Prolog and Datalog is the representation: rules, predicates, and even the concept of conjunction are themselves nodes in the graph. This homoiconicity enables meta-reasoning, self-referential structures, and a seamless boundary between knowledge and computation.
The Executable Graph¶
A defining characteristic of zelph is its homoiconicity: logic (code) and facts (data) share the exact same representation.
In many traditional semantic web stacks (like OWL/RDF), the ontology is descriptive. For example, an OWL "cardinality restriction" describes a constraint, but the actual logic to enforce that constraint resides hidden in the external reasoner's codebase (e.g., HermiT or Pellet). The operational semantics are external to the data.
In zelph, the logic is intrinsic to the data.
- Rules are Data: Inference rules are not separate scripts; they are specific topological structures within the graph itself. The implication operator
=>is a standard relation node; the conditions form a set tagged as a conjunction — all represented by ordinary subject–predicate–object triples. - Predicates are Nodes: Every relation type (including user-defined ones) is a first-class node in the graph, not an edge label. This means you can write rules about predicates — declaring symmetry, transitivity, or functional constraints as graph-level properties.
- Math is Data: Numbers are not opaque literals but Lisp-style cons-lists of digit nodes that interact with semantic entities through the same rule mechanism.
This means the graph doesn't just describe knowledge; it structures the execution of logic. The boundary between "data storage" and "processing engine" is effectively removed. Consequently, importing data (e.g., from Wikidata) can immediately alter the computational behavior of the system.
Relation Nodes and Self-Reference¶
Every fact in zelph — every subject–predicate–object triple — is represented by a dedicated relation node. This node can immediately serve as the subject, the object or the predicate of further facts, enabling statements about statements without any special mechanism.
A rule qualifies as a fact as well, so it can be talked about – yet discussing it does not claim it. Only the rule that was stated on its own fires; the one that is simply quoted is a part of the sentence containing the quotation:
zelph> (X p Y) => (X q Y)
zelph> ((X buys Y) => (X owns Y)) "was proposed by" alice
zelph> a buys car
zelph> a p b
(a q b) ⇐ (a p b)
a buys car derives nothing: alice's proposal is on record, not in force.
Nothing has to be remembered for this — an asserted rule is a part of no
other fact, a quoted one is the subject, the predicate or an object of the
sentence that quotes it — so it survives .save and .load unchanged.
Being on record does not make it findable: a condition matches solely facts that lack variables, and since alice’s rule includes variables, neither a query like R "was proposed by" alice nor a rule can access the statement (refer to Mentioning a Rule Is Not Asserting It).
The engine’s bookkeeping regarding a rule is likewise not to be found: the mark that records a ground part as the rule’s pattern does not respond to any query and fails to satisfy any condition, nor does the record of a contradiction (refer to Contradiction Detection). Only the engine is permitted to write this mark: (a p b) ~ "rule pattern" is rejected in any context where it would be written by anyone else – whether on a standalone line, embedded within a statement, written by a program, derived by a firing, or included in a rule – since a load would reconstruct the patterns from every such mark and subsequently read a claimed a p b as a rule’s pattern. A rule’s text, however, is treated as data: the tag ~ conjunction that makes a set the rule’s conditions and the memberships within that set answer like any fact, and a rule over rules reads the conditions of a rule via them (see Mentioning a Rule Is Not Asserting It).
Predicate position is the least obvious of the three, and it works like the others:
zelph> a p b
zelph> x (a p b) y
zelph> X (a p b) Y
Answer: x (a p b) y
Anything used as a predicate becomes a relation type, so the composite predicate appears among them and the fact is found by a rule quantifying over predicates just like any other:
zelph> X Y Z
Answer: (a p b) ~ ->
Answer: p ~ ->
...
Answer: a p b
Answer: x (a p b) y
(abridged — the query also lists the core relation types). This holds independently of how the network came to be: a graph read back from a .bin answers exactly as the one that was typed.
A composite predicate may itself carry variables, and then it is a pattern like any other — it unifies structurally rather than being looked up by identity, so it reaches inside the predicate. In a query:
zelph> a p b
zelph> x (a p b) y
zelph> S (a P b) O
Answer: x (a p b) y
and in a rule, where the variables it binds are available to the consequence:
zelph> a p b
zelph> x (a p b) y
zelph> (S (a P b) O) => (P links S)
(p links x) ⇐ (x (a p b) y)
zelph> S links O
Answer: p links x
The same holds in a consequence: (X p Y) => (X (Y r s) c) derives a (b r s) c, and the instantiated predicate is declared a relation type like every other.
This is in contrast to RDF, where a triple is an edge with no inherent identity. To make a statement about a triple in classic RDF, you need reification: four additional triples that decompose and name the original one. The RDF-star extension was introduced specifically to address this limitation.
In zelph, this problem does not exist. Every statement is already a node. The relation node serves a purpose analogous to Gödel numbering — it makes the system self-referential by giving every statement a first-class identity within the system. But where Gödel had to route through arithmetic encoding (prime factorization), zelph's reification is structural: the node is the statement, with no encoding or decoding step.
Comparisons with Other Systems¶
zelph's design can be understood through comparisons with several established systems. These comparisons highlight both shared principles and fundamental differences.
Prolog and Datalog¶
Prolog performs top-down, goal-driven search with backtracking. zelph performs bottom-up forward chaining, like Datalog: it materializes all derivable facts until a fixed point is reached.
However, in contrast to standard Datalog, zelph treats predicates as first-class nodes. This allows for meta-rules – rules that quantify over relations themselves. Standard Datalog lacks variables in predicate position, thus requiring an encoding to express such constructs: each fact is stored as a tuple within a single generic relation, for instance holds(p, s, o), and rules are formulated using this relation. Prolog supports variable predicates via the call/N construct. In zelph, no encoding is needed: a predicate functions as a node just like any other, and whether a relation is transitive is simply an ordinary fact that can be provided by the data itself.
Lean and Curry-Howard¶
Lean 4 is a powerful theorem prover based on dependent type theory. Through the Curry-Howard correspondence, proofs in Lean are programs — propositions are types, and proofs are terms. This is a beautiful unification of logic and computation, but it is a different kind of unification than what zelph provides.
In Lean, the inference machinery — tactics, the elaboration pipeline, the MetaM monad — lives in a metaprogramming layer that operates on terms but is not itself expressed as terms in the same way. To reason about a proof as data, you step up to a meta-level (the Expr API).
In zelph, there is no meta-level. Rules, facts, predicates, and numbers all coexist within the same graph. A rule concerning a predicate is expressed using identical syntax, stored in the same structure, and processed by the same processing engine as any ordinary fact. In terms of representation, the boundary between "data" and "logic" dissolves, with one deliberate exception: a pattern containing a variable constitutes graph structure, not data. Rules live in the same graph as data and can be created by it (Rules That Write Rules), yet a condition matches only facts that lack variables, meaning a rule involving variables cannot be discovered by a condition (refer to Claimed or Merely Written Down).
Lean unifies through type theory. zelph unifies through graph topology. These are philosophically very different approaches to the same goal: erasing the boundary between code and data.
Gödel Numbering¶
In 1931, Gödel showed that formal systems can reason about themselves by encoding formulas as numbers via prime factorization. Arithmetic statements about those numbers become, implicitly, statements about formulas.
zelph's relation nodes serve the exact same purpose: they make the system self-referential. Every statement gets a node, and that node can immediately participate in further statements. But where Gödel's encoding is arithmetic — requiring encoding and decoding via prime factorization — zelph's reification is structural. The node is the statement. No encoding, no decoding. It is a more direct path to the same goal: self-reference within a formal system.
Lisp and S-Expressions¶
Lisp's famous "code is data" principle — homoiconicity via S-expressions — is a direct ancestor of what zelph does. But where Lisp applies this idea to programs via cons-cell lists, zelph applies it to knowledge via subject–predicate–object triples.
The connection goes deeper than analogy: zelph's lists are actual Lisp-style cons-lists built from cons and nil nodes, and a cons cell is a relation node (a triple with cons as the predicate). The S-P-O triple is zelph's equivalent of Lisp's S-expression — the universal data structure from which everything else is composed.
Rules Over Graphs¶
Basic Rules and Conjunction¶
A rule in zelph connects a set of conditions to a consequence via the => operator.
The conditions form a conjunction: all must match simultaneously under a shared variable binding.
The idiomatic syntax uses commas to separate conditions:
(cond1, cond2, cond3) => consequence
Variables are single uppercase letters (A–Z) or identifiers starting with _ (e.g. _Var).
They are scoped to the current rule and universally quantified: the rule fires for all bindings that satisfy the conditions.
Everything else is a name, and that includes multi-letter uppercase tokens
such as DA or SUM. A rule that uses one as if it were a variable asks for
that one specific node instead of binding anything, so it never fires — and it
does so silently, which looks exactly like an engine that refuses to match.
Write _DA when a longer variable name reads better.
A classic example — transitive closure:
zelph> (R is transitive, A R B, B R C) => (A R C)
((A R B), (R is transitive), (B R C)) => (A R C)
zelph> > is transitive
zelph> 6 > 5
zelph> 5 > 4
(6 > 4) ⇐ {(6 > 5) (> is transitive) (5 > 4)}
After entering 5 > 4, the engine finds that the three conditions are jointly satisfiable with R = >, A = 6, B = 5, C = 4, and derives 6 > 4.
Several Consequences¶
A rule may conclude more than one thing at once. The consequences are written as several objects of the same rule. The comma is the conjunction of conditions; on the right-hand side it is refused with a message naming this form, rather than guessed at:
zelph> .deductions all
Deduction printing mode: all
Every derivation is printed.
zelph> (A is human) => (A has consciousness) (A has mortality)
(A is human) => (A has mortality) (A has consciousness)
zelph> tim is human
(tim has mortality) ⇐ (tim is human)
(tim has consciousness) ⇐ (tim is human)
The objects of a fact are an unordered set, so which of the two is announced first is not defined.
This is not the same as writing two rules with the same conditions.
One rule fires once, so its consequences share their fresh variables: (X p Y) => (X q N) (N r Y) links X to a generated node and that same node to Y, while two separate rules would generate one node each.
Meta-Rules: Predicates as First-Class Nodes¶
Notice that R in the transitive rule is a variable ranging over predicates.
This is possible because predicates in zelph are nodes, not edge labels.
Any relation declared is transitive automatically benefits from this single rule — no separate rule per predicate is needed.
This allows for a class of rules that standard Datalog can only represent via an encoding (see Prolog and Datalog): rules that reason about relations themselves.
Example — Symmetric relations:
zelph> (R is symmetric, X R Y) => (Y R X)
((X R Y), (R is symmetric)) => (Y R X)
zelph> friend is symmetric
zelph> alice friend bob
(bob friend alice) ⇐ {(alice friend bob) (friend is symmetric)}
A single rule declares the semantics of symmetry for any relation.
Declaring friend is symmetric is a fact about the predicate friend; the rule matches it and closes over all instances.
Example — Opposite relations:
zelph> (R "is opposite of" S, X R Y) => (Y S X)
((R "is opposite of" S), (X R Y)) => (Y S X)
zelph> "has part" "is opposite of" "is part of"
zelph> chimpanzee "has part" hand
(hand "is part of" chimpanzee) ⇐ {("has part" "is opposite of" "is part of") (chimpanzee "has part" hand)}
Declaring that "has part" is opposite of "is part of" causes every has part fact to automatically generate its inverse.
The rule is generic: it works for any pair of opposite relations without modification.
The two examples differ in a single aspect that becomes significant when a rule performs negation.
The symmetric rule creates an R fact exclusively for an R it has just matched as a predicate; the opposite rule creates an S fact based on an S discovered within the object of a declaration, meaning the rule does not specify which predicates are involved.
Regarding negation levels, such a rule is considered to create every predicate; Rules over predicates clarifies the consequences and how the rule-derived form circumvents this issue.
Rules That Derive Rules¶
A consequence does not have to be a fact. It can be a rule — and then the outer rule is a rule schema: firing it writes a new rule into the graph, which the engine picks up and applies within the same run.
The inner rule's variables belong to the inner rule. Only what the outer rule's conditions bind is substituted; everything else comes through as a variable, so what arrives is a rule and not one instance of one.
Example — transitivity as a schema:
zelph> (R is transitive) => ((X R Y, Y R Z) => (X R Z))
(R is transitive) => (((X R Y), (Y R Z)) => (X R Z))
zelph> before is transitive
(((Y before Z), (X before Y)) => (X before Z)) ⇐ (before is transitive)
zelph> a before b
zelph> b before c
(a before c) ⇐ {(b before c) (a before b)}
zelph> c before d
(b before d) ⇐ {(c before d) (b before c)}
(a before d) ⇐ {(c before d) (a before c)}
R was bound to before and is gone; X, Y and Z were bound by nothing and stayed variables.
What the second line derives is the transitivity rule for before, and one such rule appears for every relation declared transitive.
Compare this with the meta-rule (R is transitive, X R Y, Y R Z) => (X R Z), which expresses the same closure by quantifying over the predicate at match time.
The schema instead pays that quantification once, when the relation is declared, and leaves a specialised rule behind.
Both are available; the schema is the one that can make the shape of a rule depend on data.
It is also the form that leaves the negation levels intact when a rule takes the predicate it creates from the subject or object of a declaration, as occurs in an inverse or sub-property axiom: every rule it derives explicitly names its predicates.
Example — a rule under a switch:
zelph> (K is on) => ((X p Y) => (X q Y))
zelph> a p b
zelph> A q B
zelph> k is on
((X p Y) => (X q Y)) ⇐ (k is on)
(a q b) ⇐ (a p b)
zelph> A q B
Answer: a q b
The inner rule is written out from the start and a p b is there before the switch, yet the query answers nothing until k is on arrives.
That is not a scheduling accident, it is the next section.
Example — an ontology's property axioms as data:
Sub-property, domain and sub-class are the axioms an ontology is normally described with. Written once as schemas, every declaration a modeller makes afterwards is ordinary data — and produces its own rule:
zelph> .deductions all
Deduction printing mode: all
Every derivation is printed.
zelph> (P is transitive) => ((X P Y, Y P Z) => (X P Z))
(P is transitive) => (((X P Y), (Y P Z)) => (X P Z))
zelph> (P subpropertyof Q) => ((X P Y) => (X Q Y))
zelph> (C subclassof D) => ((X isa C) => (X isa D))
zelph> (P domain C) => ((X P Y) => (X isa C))
zelph> mother subpropertyof parent
((X mother Y) => (X parent Y)) ⇐ (mother subpropertyof parent)
zelph> parent domain person
((X parent Y) => (X isa person)) ⇐ (parent domain person)
zelph> person subclassof agent
((X isa person) => (X isa agent)) ⇐ (person subclassof agent)
zelph> m mother n
(m parent n) ⇐ (m mother n)
(m isa person) ⇐ (m parent n)
(m isa agent) ⇐ (m isa person)
One statement of data, m mother n, walked three rules that nobody wrote — and each step carries its own justification, so .explain (m isa agent) reconstructs the chain back to it.
Rules that write rules have a page of their own: Rules That Write Rules covers where the idea comes from (it is the axiom schema of logic, with the instances made real), what happens when a generator matches many times, generators that generate generators, and the edges of the construct.
Mentioning a Rule Is Not Asserting It¶
Writing a rule down inside another statement talks about it; it does not claim it.
zelph> ((X p Y) => (X q Y)) is questionable
zelph> a p b
zelph> A q B
zelph>
Nothing fires — which is the only defensible reading, since the alternative is that doubting a rule puts it to work.
What the rule says is not claimed either. A mention writes the rule’s parts as patterns, exactly as a typed rule does, so a proposal on record leaves its ground consequence unanswered:
zelph> ((X is bad) => (alarm is on)) "was proposed by" alice
zelph> rust is bad
zelph> A is B
Answer: rust is bad
zelph> .explain (alarm is on)
alarm is on [rule pattern; not asserted]
Only what the mention has brought into existence qualifies as a pattern, and a claim undoes it: a statement claims itself and every fact nested in it outside a =>, while nothing situated within a => is claimed by writing it. A statement asserted before the mention therefore remains asserted, and one written afterwards that holds the identical fact outside the rule, either independently or as a part, claims it, even though neither puts the mentioned rule in force. The order of writing within a single statement does not matter either. In the example below, the mention comes first and creates rust is bad as its condition, yet the statement still claims it, while the consequence that only the mentioned rule states remains a pattern:
zelph> ((rust is bad) => (alarm is on)) "was proposed because of" (rust is bad)
zelph> A is B
Answer: rust is bad
zelph> .explain (alarm is on)
alarm is on [rule pattern; not asserted]
The mentioned rule itself remains stored as data, accessible for reading by a rule over rules, unless it is contained within another mentioned rule, in which case it is a part of that rule, or it is written as a mention in its own right (see below); a statement that holds it outside a rule claims it as a node, yet not what it says. A query that names a mention does not mark anything. The same principle applies to a Janet program that writes a mention using zelph/rule-text (see Claimed or Merely Written Down), and to a mention written by a firing. What a firing derives claims the facts its consequence writes outside the mentioned rule, just as any statement does, yet it does not assert a value that a variable within the rule represents: a value the rule binds is claimed solely by the statement that asserted it. A rule over rules therefore asserts no part of the rules it reads, and the proposal stays a proposal:
zelph> (G => H) => (G seen H)
zelph> alice says ((rust is bad) => (alarm is on))
((rust is bad) seen (alarm is on)) ⇐ ((rust is bad) => (alarm is on))
zelph> A is B
zelph> .explain (alarm is on)
alarm is on [rule pattern; not asserted]
When the user types the identical (rust is bad) seen (alarm is on), it writes both parts and claims them.
A rule may also function as a mention in its own right: one authored by zelph/mention or zelph_mention, and one that stands in an argument of an opaque predicate, regardless of whether it is typed or written by a firing. This kind of rule carries the same mark as any mention, meaning it remains out of force, even after no statement holds it any longer, and a rule over rules does not read it, just as neither a query nor a rule condition takes a mention as data. A claim of the same rule puts it in force: a typed rule, zelph/fact inside a Janet block, zelph_fact, zelph/dedup-rule, or zelph/build-rule. A rule that a plain statement holds, like alice’s proposal above, remains accessible for reading:
zelph> believes ~ opaque
zelph> (G => H) => (G seen H)
zelph> alice says ((rust is bad) => (alarm is on))
((rust is bad) seen (alarm is on)) ⇐ ((rust is bad) => (alarm is on))
zelph> john believes ((tea is cold) => (kettle is on))
zelph> .prune-facts john believes ((tea is cold) => (kettle is on))
Pruned 1 matching facts.
Consider running .cleanup.
zelph> tea is cold
zelph> A is B
Answer: tea is cold
zelph> S seen O
Answer: (rust is bad) seen (alarm is on)
zelph> .explain ((tea is cold) => (kettle is on))
(tea is cold) => (kettle is on) [rule mentioned; not in force]
A rule over rules reads the conditions of a rule, regardless of how numerous they may be, by means of the memberships within its condition set: G => H binds G to the set, and M in G binds M to every condition sequentially. This mechanism applies equally to a rule that a statement holds as to one that is currently in force, and the tag ~ conjunction answers just like any fact, here for the rule over rules as well:
zelph> alice says ((a p b, c q d) => (alarm is on))
zelph> (G => H, M in G) => (M cond-of H)
((a p b) cond-of (alarm is on)) ⇐ {((a p b) in {(c q d) (a p b)}) (((c q d), (a p b)) => (alarm is on))}
((c q d) cond-of (alarm is on)) ⇐ {((c q d) in {(c q d) (a p b)}) (((c q d), (a p b)) => (alarm is on))}
zelph> S ~ conjunction
Answer: {(M in G) (G => H)} ~ conjunction
Answer: {(c q d) (a p b)} ~ conjunction
A rule over rules may additionally specify the rule it seeks. A rule held as an argument within a condition matches every rule sharing identical conditions and the same consequence, regardless of which statement wrote it. A comma list of conditions is compared as a set, irrespective of sequence, and a rule that differs in any single condition, in the number of its conditions, or in its consequence constitutes a distinct rule:
zelph> (P proposed ((a p b, c q d) => (alarm is on))) => (P flagged k)
zelph> x proposed ((c q d, a p b) => (alarm is on))
(x flagged k) ⇐ (x proposed (((c q d), (a p b)) => (alarm is on)))
zelph> y proposed ((a p b, c r d) => (alarm is on))
zelph> S flagged O
Answer: x flagged k
A variable of the outer rule inside the held rule binds the corresponding part of the stored rule, and when conditions can pair up in multiple ways, every possible pairing is tried. What the held rule matches is a rule lacking variables of its own. A rule that a statement mentions with variables constitutes rule text, which no condition can match (refer to Relation Nodes and Self-Reference), and attempting to locate it via naming in the outer rule also fails to retrieve it:
zelph> bob says ((X p Y) => (X r Y))
zelph> (Z says ((X p Y) => (X r Y))) => (Z ok k)
zelph> S ok O
zelph>
Matching such a mention up to a renaming of its variables remains an open direction. A variable in the outer rule that binds an entire rule refers to that node, just as it does for any other value: two statements that each write (a p b, c q d) => (alarm is on) hold two distinct rules, which (bob says V, carl says V) does not join, whereas two mentions of a ground rule with a single condition constitute one node.
A mentioned rule features the same slots as any other rule: a condition operator must reside at the top of one of its conditions, just as in a typed rule, and is disallowed elsewhere, particularly within the consequence. What follows beneath the operator, as written in the mention, constitutes a pattern, as the other components of the rule do, whether in a statement or in a query:
zelph> ((X is bad, ¬(rust is fixed)) => (alarm is on)) "was proposed by" bob
zelph> rust is bad
zelph> A is B
Answer: rust is bad
zelph> .explain (rust is fixed)
rust is fixed [rule pattern; not asserted]
A firing does not derive a statement whose instance would keep a variable from a rule it mentions. It writes the conditions of such a rule exactly as they are, meaning that (X p Y) => (X about ((A r B, A s B) => (c q d))) would write rule text that no query answers, and the first rule below would produce half of a rule that was never written, with b and k appearing in its consequence while X and Y remain in its conditions. Neither is derived: nothing is written, claimed, or printed, and no witness is made for a fresh variable that exists solely in that context. The same applies within a collection of the rule’s text, for which the firing builds a value, as seen in the second rule below. There, the firing also keeps a variable it does not bind, such as B in the third rule, whereas a rule that the firing makes ground, as in the fourth, is derived:
zelph> .deductions all
Deduction printing mode: all
Every derivation is printed.
zelph> (X p Y) => (((X q Y, X r Y) => (X s Y)) is noted)
zelph> b p k
zelph> S is noted
zelph> (X p Y) => (X about {((X r B, X s B) => (c q d))})
zelph> (X p Y) => (X near {((X r B) => (c q d))})
zelph> (X p Y) => (X like {((X r Y) => (X q Y))})
(b like {((b r k) => (b q k))}) ⇐ (b p k)
zelph> S about O
zelph> S near O
zelph>
A mentioned rule that features a single condition has a distinct structure: its condition takes the form of a fact instead of a set, and a firing substitutes within it just as it does in any other part of the consequence. A variable appearing exclusively within the mentioned rule is therefore a fresh variable relative to the outer rule, and the firing makes a witness for it. What it writes is a rule concerning the witnesses, not a rule involving variables:
zelph> (A p B) => (y about ((X p Y) => (X r Y)))
zelph> a p b
zelph+> S about O
Answer: y about ((?? p ??) => (?? r ??))
Writing a mention that incorporates its own variables constitutes an open direction as well.
The distinction is decidable from the graph alone, and cheaply.
Building a rule in order to talk about it creates the same nodes and the same edges as asserting it, so the rule node itself cannot say which happened — but its surroundings can: an asserted rule is a part of nothing, while a mentioned one is the subject, the predicate or an object of the statement that mentions it.
Nothing is remembered, so a .save/.load round trip cannot lose the difference, and a graph without rules never pays for the test.
This is what makes the switch above work.
Until k is on fires, (X p Y) => (X q Y) is an object of the outer rule and therefore a mention; firing the outer rule asserts a copy of it, which is a part of nothing and consequently live.
The one shape this cannot separate is a fully ground rule — no variables anywhere — that is asserted and mentioned at once: hash-consing makes those a single node. A rule with variables is two nodes, because every statement names its own variables.
Mentioning a Statement: Opaque Predicates¶
A rule is not the sole entity that can be written down without being claimed. The sentence "John believes that Mary waits" conveys information regarding John and nothing about Mary: the statement john believes (mary waits nil) must not make mary waits nil a fact. => serves as the built-in instance of such a predicate – the parts of a rule are discussed, not asserted – and the fact P ~ opaque makes any predicate P behave in the same way; opaque is a node within the language zelph, akin to refuted. In every argument position of an opaque fact, whether subject or object, whatever the statement newly creates is a mention: it carries the same mark as a rule’s ground pattern, no query and no rule condition takes it as data, and .explain labels it by the position it stands in:
zelph> believes ~ opaque
zelph> john believes (mary waits nil)
zelph> X waits nil
zelph> S believes O
Answer: john believes (mary waits nil)
zelph> .explain mary waits nil
mary waits nil [mentioned; not asserted]
What existed before keeps its status, meaning that a belief in a statement previously asserted leaves that statement asserted, and a subsequent claim of the identical statement makes the mention data. A rule condition examines the interior of an opaque argument based on its structure, just as it examines the interior of a rule that a statement holds, and a firing whose consequence involves an opaque predicate writes its arguments as mentions too:
zelph> believes ~ opaque
zelph> john believes (mary waits nil)
zelph> (Z believes (Y waits nil)) => (Z ~ credulous)
(john ~ credulous) ⇐ (john believes (mary waits nil))
zelph> (X ~ woman) => (X believes (bob waits nil))
zelph> ann ~ woman
(ann believes (bob waits nil)) ⇐ (ann ~ woman)
(ann ~ credulous) ⇐ (ann believes (bob waits nil))
zelph> X waits nil
zelph> mary waits nil
zelph> X waits nil
Answer: mary waits nil
The same applies to a statement constructed using zelph/fact from Janet and created via the C API with zelph_fact: neither claims the arguments of an opaque fact. Every invocation is a statement of its own, meaning that an argument established by a distinct zelph/fact call is claimed by that call; zelph/mention and zelph_mention write it as a mention instead (refer to Claimed or Merely Written Down). The negation levels read nothing within an opaque argument, and .prune-facts on a claimed statement that an opaque fact also holds withdraws the claim while preserving the statement as a mention that the fact holds.
In an opaque argument, a rule constitutes a mention in its own right: it is not in force, even after the fact that holds it is removed, and a rule over rules does not read it (refer to Mentioning a Rule Is Not Asserting It).
A query asserts what it creates within an opaque argument, just as it asserts what it creates beneath a => that it mentions outside every condition operator. A program that asks without writing runs its question within a cluster that it drops afterwards:
zelph> believes ~ opaque
zelph> S believes (sue sleeps nil)
zelph> X sleeps nil
Answer: sue sleeps nil
The declaration is refused when any of the predicate’s facts holds a statement in an argument position, since the claims such a fact made can no longer be distinguished from what it would merely mention; facts whose arguments are atoms do not prevent this. Removing the declaration is likewise refused under the same condition, and the same applies to declaring a core predicate. A name merge (.name) that would make a predicate opaque while one of its facts holds a statement is refused in the same way and with the same error message, before any modification: this constitutes a merge involving a declared predicate and one that is not declared, in either direction. The node opaque retains its name within the language zelph and does not merge with any other node, just as every node in the engine’s vocabulary does, meaning that neither a rename nor a merge makes or ends a declaration. Everything preceding -- in the message remains constant, allowing a program to recognize the refusal by this prefix:
zelph> sue knows (tom sleeps nil)
zelph> knows ~ opaque
Error in line "knows ~ opaque": fact(): a predicate cannot be declared opaque while one of its facts holds a statement -- knows: sue knows (tom sleeps nil)
Deep Unification¶
zelph's unification engine matches patterns against arbitrarily nested structures. This is essential for reasoning about statements-about-statements — a natural consequence of zelph's graph topology where fact nodes can themselves appear as subjects or objects of other facts.
zelph> .deductions all
Deduction printing mode: all
Every derivation is printed.
zelph> ((A + B) = C) => (test A B)
zelph> (4 + 5) = 9
(test 4 5) ⇐ ((4 + 5) = 9)
The rule's condition pattern ((A + B) = C) requires a fact whose subject is itself a fact matching (A + B).
The engine recursively walks the graph topology, binding A = 4, B = 5, C = 9.
The presence of .deductions all is required here since the derived fact is
associated with test, a node that is not referenced in the typed statement,
causing the default quiet mode to suppress it and merely annotate the next
prompt with + – refer to
Deduction Output Modes. (In test A B the
variables occupy predicate and object position: the derived statement is
test, related to 5 through the predicate 4.)
This extends to arbitrary depth:
zelph> .deductions all
Deduction printing mode: all
Every derivation is printed.
zelph> (subj pred (obj is (subj2 A (b test C)))) => (success A C)
zelph> subj pred (obj is (subj2 a_val (b test c_val)))
(success a_val c_val) ⇐ (subj pred (obj is (subj2 a_val (b test c_val))))
Deep unification also works within conjunction conditions, enabling rules that combine structural decomposition with multi-condition reasoning:
zelph> ((A + B) = C) => (test A B)
zelph> (4 + 5) = 9
zelph+> (*{ ((A + B) = C) (B followed-by D) (C followed-by E) } ~ conjunction) => ((A + D) = E)
(((A + B) = C), (B followed-by D), (C followed-by E)) => ((A + D) = E)
zelph> 5 followed-by 42
zelph> 9 followed-by 43
((4 + 42) = 43) ⇐ {((4 + 5) = 9) (5 followed-by 42) (9 followed-by 43)}
This rule decomposes the nested equation (A + B) = C, uses the bound values to look up successor relationships, and assembles a new equation — all in a single inference step.
What the conjunction tag decides, and what it does not¶
The tag says how the members of a condition container combine; it is not what makes the node a container. With more than one member it is the only thing that says so, and other combinations are conceivable — so an untagged container of several conditions is left alone rather than read as a conjunction.
A container of exactly one member is different: no combination of one thing can differ from any other, so the tag cannot change what the rule means. All four spellings below are therefore the same rule, and all four fire:
(X p Y) => (X q Y) # one condition, no container
{(X p Y)} => (X q Y) # written out in set notation
*{(X p Y)} => (X q Y) # ... with the focus operator
(*{(X p Y)} ~ conjunction) => (X q Y) # ... and tagged explicitly
Facts with Multiple Objects¶
A fact in zelph connects a subject to an object via a predicate.
When a fact has multiple objects (e.g. f maps 1 2), these objects form an unordered set — there is no defined ordering among them.
The statement f maps 1 2 means: f is related via maps to both 1 and 2, but it does not encode which is "first" and which is "second".
This is a deliberate design choice: zelph's internal topology represents objects as a set of incoming connections to the fact node, not as a sequence.
When order matters — for example, to represent a mapping from a domain element to a codomain element — you must use lists (cons-lists via angle brackets <...>), which provide an explicit structural ordering.
See Angle Brackets: Lists for details on the list syntax.
Example — unordered objects in rules:
zelph> alice parent_of bob charlie
zelph> (A parent_of B) => (B child_of A)
(bob child_of alice) ⇐ (alice parent_of bob)
(charlie child_of alice) ⇐ (alice parent_of charlie)
The rule matches each object independently. Whether bob or charlie was written first is irrelevant — both are equally "objects of" the parent_of fact.
The same applies when a fact is embedded within another. A statement contained within a pattern is stated by a fact that includes additional objects as well, meaning (a p b c) states both (a p b) and (a p c), a variable among the objects takes each of them in turn, and a rule over such a statement fires whichever of its conditions the engine evaluates first, with anchoring on or off (.anchors):
zelph> a p b c
zelph> (a p b c) bad k
zelph> a q c
zelph> (a p c) bad Z
Answer: (a p c) bad k
zelph> (a p Y) bad k
Answer: (a p b) bad k
Answer: (a p c) bad k
zelph> (X q Y, (X p Y) bad Z) => (X ok Z)
(a ok k) ⇐ {((a p c) bad k) (a q c)}
An answer names the statement the pattern requested, (a p c) bad k, whereas the fact stating it is (a p b c) bad k. A consequence is read exactly: a rule whose consequence is (a p b) bad k writes that fact beside the wider one. A statement functioning as a predicate is interpreted identically: next to x (a p b c) y, the query x (a p c) Z answers x (a p c) y, and a rule applying to it fires.
.explain names the fact that states a condition as its premise, across every level of the condition and where a statement is its predicate, even when the narrower statement appears solely as a rule’s pattern. A query answers each binding exactly once, even if a narrower fact, alongside the wider one, states it a second time:
zelph> ((a p c) bad k) => (x ok y)
zelph+> .explain x ok y
x ok y
└─ (a p b c) bad k [axiom]
zelph+> x (a p b c) y
zelph> (x (a p c) Z) => (Z ok c)
(y ok c) ⇐ (x (a p c) y)
zelph> .explain y ok c
y ok c
└─ x (a p b c) y [axiom]
zelph> a p c
zelph> a p Y
Answer: a p b
Answer: a p c
This distinction becomes critical in more complex rules. Consider a naïve attempt at function composition using multiple objects:
(F maps A B, G maps B C) => ((G compose F) maps A C)
f maps 1 2
g maps 2 3
The engine cannot distinguish "domain" from "codomain" here, because both are
unordered objects of the same fact: f maps 1 2 matches F maps A B with
A = 1, B = 2 and equally with A = 2, B = 1. So the rule derives not only
(g compose f) maps 1 3 but also (f compose g) maps 1 3, and each of those
is itself a maps fact whose subject is a composite the rule has just built –
which feeds the rule again, with ((f compose g) compose g), then
(((f compose g) compose g) compose (g compose f)), and so on. The terms grow
without bound and there is no fixed point to reach.
Do not type this one in. It is here as the mistake to recognize, not as an example to run: three lines are enough to make the engine derive until the session is ended from outside, since a run in progress cannot be stopped from the prompt.
Example — Function composition with lists:
The correct approach uses ordered lists to encode the domain–codomain relationship:
zelph> (F maps <A B>, G maps <B C>) => ((G compose F) maps <A C>)
((G maps <B C>), (F maps <A B>)) => ((G compose F) maps <A C>)
zelph> f maps <item1 item2>
zelph> g maps <item2 item3>
((g compose f) maps <item1 item3>) ⇐ {(g maps <item2 item3>) (f maps <item1 item2>)}
The list <A B> is a cons-list with a defined structure: A is the first element (car) and B is the rest (cdr).
Deep unification matches this structure precisely, so A unambiguously binds to the domain element and B to the codomain element.
The consequence (G compose F) creates a new fact node representing the composition, which then becomes the subject of maps.
This is higher-order reasoning expressed as first-order graph topology — with the structural ordering provided by cons-lists rather than by positional assumptions about objects.
Negation as Failure¶
Negation in zelph follows negation-as-failure (NAF) semantics, familiar from Datalog with stratified negation and Prolog's \+.
A negated condition succeeds when no fact in the graph matches the pattern under the current variable bindings.
The idiomatic syntax uses ¬:
zelph> (A is yellow, ¬(A is green)) => (A "is not" green)
(¬(A is green), (A is yellow)) => (A "is not" green)
zelph> plant is green
zelph> plant is yellow
zelph> plant2 is yellow
(plant2 "is not" green) ⇐ {(¬(plant2 is green)) (plant2 is yellow)}
plant is both yellow and green, so ¬(plant is green) fails and the rule does not fire for plant.
plant2 is yellow but not green, so the rule fires.
Negation is particularly powerful for structural queries — finding elements that lack a specific connection:
zelph> elem1 --> elem2
zelph> elem2 --> elem3
zelph> elem3 --> elem4
zelph> elem4 --> elem5
zelph> elem1 partoflist mylist
zelph> elem2 partoflist mylist
zelph> elem3 partoflist mylist
zelph> elem4 partoflist mylist
zelph> elem5 partoflist mylist
zelph> (A partoflist L, ¬(A --> X)) => (A "is last of" L)
(¬(A --> X), (A partoflist L)) => (A "is last of" L)
(elem5 "is last of" mylist) ⇐ {(¬(elem5 --> X)) (elem5 partoflist mylist)}
The negated condition ¬(A --> X) succeeds only when A has no outgoing --> link — identifying the last element purely declaratively.
A free variable inside ¬ is quantified inside it. Whichever position it
stands in, the condition succeeds exactly when no fact matches — the free
variable produces no binding that leaves the rule. So the same graph answers
both directions the way their names suggest:
zelph> a ~ interval
zelph> b ~ interval
zelph> c ~ interval
zelph> a before b
zelph> b before c
zelph> (A ~ interval, ¬(A before B)) => (A is latest)
((A ~ interval), ¬(A before B)) => (A is latest)
(c is latest) ⇐ {(c ~ interval) (¬(c before B))}
zelph> (A ~ interval, ¬(B before A)) => (A is earliest)
((A ~ interval), ¬(B before A)) => (A is earliest)
(a is earliest) ⇐ {(a ~ interval) (¬(B before a))}
Textbook Datalog would refuse both rules: its safety condition (range
restriction) mandates that every variable appearing within negation must be
bound by a positive condition, and B fails this requirement. Certain
engines loosen this rule when dealing with an anonymous variable: for
example, Soufflé permits _ under negation and reads it as quantified
inside the negation. zelph extends this allowance to named variables as
well, granting both rules the interpretation implied by their notation.
Ranging over a domain is a positive condition, not a negation. To conclude something for each member of a set that lacks a property, name the set:
(X flagged S, ¬(X flagged bad)) => (X unflagged ok)
X flagged S is what makes an entity a candidate, and it says which
candidates — the negation then only filters. The justification of each
derived fact names both, so a result can be traced back to why the entity was
considered at all.
As with a path condition, ¬ serves as input syntax over an ordinary fact: ¬(F) represents the condition ((F) ~ negation), just as (C P279⁺ T) denotes the condition ((C P279 T) closure one-or-more). A rule names that fact as its condition rather than the pattern F directly, meaning a pattern that one rule negates stays positive in every other rule that employs it. Expressed in full, the fact corresponds to the explicit (ASCII-only) spelling of ¬(F): within a condition, it is the identical condition, and it prints as ¬(F):
zelph> (X go Y, ((X p b) ~ negation)) => (X ok Y)
(¬(X p b), (X go Y)) => (X ok Y)
zelph> t go k
(t ok k) ⇐ {(¬(t p b)) (t go k)}
What ¬ applies to. A single fact pattern, not a group of them —
¬(A is y, A is z) is rejected rather than guessed at. Use De Morgan:
¬(A ∧ B) is (¬A) ∨ (¬B), and a
disjunction is written as several rules with the same
consequence:
(A is x, ¬(A is y)) => (A r s)
(A is x, ¬(A is z)) => (A r s)
Negating a group directly is an open direction, not a decision against it — see Where the logic goes next.
Where ¬ may stand, and what it means there. Within a condition, it functions as the negation-as-failure operator above – in a rule, and in a query, which constitutes a condition list evaluated once. Positioned alone on a line and lacking a variable, it expresses a claim: the fact does not hold.
zelph> ¬(a p b)
zelph> c p d
zelph> S p O
Answer: c p d
The refuted fact answers nothing, no rule fires on it, and zelph/exists reports it as absent – but it is not absent, it is denied. Asserting it afterwards is refused rather than silently overwritten, and so is refuting something the graph already claims:
zelph> ¬(a p b)
zelph> a p b
Error in line "a p b": fact(): this fact is known to be wrong
This is the mechanism zelph uses for a negative claim: a fact carries a probability, and one below 0.5 makes it known-wrong. The claim survives .save and .load, and it prints as what it is – the echo of ¬(a p b) is ¬(a p b), not a p b.
When a variable appears within it, the line asks instead: ¬(X q d) constitutes a query featuring a single negated condition. It establishes no bindings, thus yields a single response – displaying the condition as written – whenever no fact satisfies it, and produces nothing otherwise; in the first session above, c p d matches X p d:
zelph> ¬(X q d)
Answer: ¬(X q d)
zelph> ¬(X p d)
Both readings are part of the line, not of the prefix, thus neither reaches a statement that only includes a pattern. There, the symbol ¬ is refused:
zelph> x mentions (¬(a p b))
Error in line "x mentions (¬(a p b))": "¬" is a condition operator and has no
meaning in a statement that asserts: it succeeds when a pattern is ABSENT, which
only a condition can ask -- in a rule, or in a query (a line with a variable).
On its own line "¬(a p b)" says that the fact does not hold.
The marking a refutation writes is printed without the prefix for the same reason – (a p b) ~ refuted – since the predicate is already saying it, and a ¬ inside the subject would be interpreted as the condition operator when the line is re-entered.
What the graph claims is a fact that has been asserted, derived, or written as a part of a claimed statement. A statement that a rule or query merely writes down as its pattern does not constitute a claim, and thus may be refuted; a rule that concludes it then reports a contradiction when it fires:
zelph> (mary waits nil) => (john sleeps nil)
zelph> ¬(john sleeps nil)
zelph> mary waits nil
! ⇐ (mary waits nil)
Found one or more contradictions!
The alternative ordering functions equally: a rule can name a fact that had been previously refuted, whether within its conditions or in its consequence. A condition referencing the refuted fact never succeeds in matching, and a consequence attempting to derive it is reported as a contradiction.
The marking also serves as a second spelling for the refutation. On a separate line, (a p b) ~ refuted conveys the same meaning as ¬(a p b): it is refused for a fact the graph claims, and accepted again, changing nothing, for a fact that is already refuted – thus, the printed marking re-enters. A fact that the line names by reference – a Janet variable within ,f ~ refuted, or the node yielded by an inline keyword – is refuted and refused in identical fashion. When containing a variable, (X p b) ~ refuted functions as a query seeking refutations. Within a rule, the parenthesized marking acts as a condition checking whether a fact is refuted, or as a consequence that derives a refutation. A refutation that is derived and meets a fact somebody claimed is reported as a contradiction, and the fact keeps answering:
zelph> (X ~ person) => ((X sleeps nil) ~ refuted)
zelph> mary sleeps nil
zelph> mary ~ person
! ⇐ (mary ~ person)
Found one or more contradictions!
zelph> S sleeps O
Answer: mary sleeps nil
The contradiction is recorded with the claimed fact among its members, thus it is reported only once. The focus spelling *(P) ~ refuted is rejected by both a rule and a query: the focus transforms it into the pattern P, which the rule would otherwise read or derive positively. From Janet, the refutation of a ground fact is expressed via zelph/refute; zelph/fact refuses to write its marking.
A condition can read the refutation directly. A rule whose condition matches the marking and whose consequence is the refuted fact reports the same contradiction, recorded with the facts its conditions matched, including the marking, and thus reported once:
zelph> ¬(t p b)
zelph> t go k
zelph> ((X p b) ~ refuted, X go Y) => (X p b)
! ⇐ {(t go k) ((t p b) ~ refuted)}
Found one or more contradictions!
zelph> X ~ refuted
Answer: (t p b) ~ refuted
A marking that a claimed statement writes is itself claimed alongside it, meaning the refutation remains the same regardless of position. If embedded within another statement, or present as a member in a comma-separated list devoid of variables, it is refused for a fact the graph claims, and a rule whose consequence writes it within a statement reports a contradiction rather than deriving it:
zelph> a p b
zelph> x says ((a p b) ~ refuted)
Error in line "x says ((a p b) ~ refuted)": fact(): this fact is known to be true
zelph> (X go Y) => (k says ((a p b) ~ refuted))
zelph> t go k
! ⇐ (t go k)
Found one or more contradictions!
zelph> S p O
Answer: a p b
Regardless of which spelling builds the marking, the refutation is the same. A refuted or a ~ provided by a binding produces the same marking: a derived marking of a claimed fact constitutes a contradiction, recorded identically, and nothing is written. A derived marking of a fact that is already refuted is accepted and changes nothing, whether it appears independently or within a statement, just like the typed line does. Within an argument of an opaque predicate, a derived marking functions as a mention, just as a typed one does, and does not refute anything:
zelph> a p b
zelph> t go refuted
zelph> (X go Y) => ((a p b) ~ Y)
! ⇐ (t go refuted)
Found one or more contradictions!
zelph> S p O
Answer: a p b
zelph> ¬(c p d)
zelph> (X go Y) => (X says ((c p d) ~ Y))
(t says ((c p d) ~ refuted)) ⇐ (t go refuted)
The same applies in any context where the consequence writes a marking or a refuted fact: whether as a member within a set, a collection, or a comma list, or within a composite predicate. Each such location is read exactly as it is in a typed statement, which is refused in every one of these forms: introducing a marking of a claimed fact there, or a refuted fact that the statement claims there, constitutes a contradiction, and marking a refuted fact changes nothing. A rule that a consequence derives may name a refuted fact, just as a typed rule may, including one that the binding completes: a condition on that fact never matches, a marking of it as a condition reads the refutation, and a consequence based on it results in a contradiction once the rule fires:
zelph> ¬(t p d)
zelph> t go k
zelph> (X go Y) => (((X p d) ~ refuted) => (X r s))
(((t p d) ~ refuted) => (t r s)) ⇐ (t go k)
(t r s) ⇐ ((t p d) ~ refuted)
zelph> S r O
Answer: t r s
zelph> (X go Y) => (X says {(X p d)})
! ⇐ (t go k)
Found one or more contradictions!
The C API refuses the marking within zelph_fact and states a refutation via zelph_refute (refer to the C API). A refutation cannot be refuted in turn: ¬((a p b) ~ refuted), the line ((a p b) ~ refuted) ~ refuted, and attempts to apply zelph/refute or zelph_refute to a marking are all refused, as the marking they wrote refuted its fact all the same, even a fact the graph claims. A refutation is withdrawn by removing its marking.
A refutation claims its own marking and nothing concerning the fact it refutes. A fact that a rule merely wrote down remains the rule’s pattern, while a fact generated by a refutation is written as a mention, together with its content: ¬(x says (a p b)) conveys no information about a p b, and any marking within it does not refute anything. A statement whose refutation is rejected keeps nothing it wrote, thus c q d, (c q d) ~ refuted results in no trace of c q d. A focus on a part of the marked statement hands that part to the marking: (x says *(a p b)) ~ refuted refutes a p b and records x says (a p b) beside it, which claims a p b. The line is thus rejected, as its two lines are in either sequence, except when the part appears within an argument of an opaque predicate, which mentions it. Withdrawing a refutation – pruning its marking via .prune-facts X ~ refuted, or erasing it through .remove – also removes the probability 0 from the fact’s edge, leaving the fact a pattern or a mention, whether in the current session or after a .save followed by a .load: it will not respond to any query and will not fire any rule until a statement claims it:
zelph> (a p b) => (c q d)
zelph> ¬(a p b)
zelph> .prune-facts X ~ refuted
Pruned 1 matching facts.
Consider running .cleanup.
zelph> S p O
zelph> a p b
zelph+> S q O
Answer: c q d
A statement that claims a refuted fact is refused as known to be wrong, as asserting the fact is, even if it holds the fact by node: a mention that a Janet block builds, the fact that the focus *(F) ~ refuted stands for, or a node that a Janet variable or an inline keyword hands in. A comma list that asserts a rule’s pattern while refuting it is rejected in the same way:
zelph> (a p b) => (c q d)
zelph> ¬(a p b)
zelph> x says (*(a p b) ~ refuted)
Error in line "x says (*(a p b) ~ refuted)": fact(): this fact is known to be wrong
A rule derives what holds, so a negated consequence still has no reading and is refused:
zelph> (A p B) => ¬(A q B)
Error in line "(A p B) => ¬(A q B)": "¬" is a condition operator and has no
meaning as a consequence: a rule derives what holds, not what does not. To say
that the two may not hold together, write a contradiction rule --
"(A p B, A q B) => !".
The contradiction rule the message names is what "these two must not hold together" is written as.
The other two condition operators have no reading outside a condition at all, and say so. ≈ asks what a network believes and ⁺ / ∗ ask what the engine can walk to; neither is something a line can assert. A path marker whose two ends are both concrete is refused, while the same shape with a variable in it is an ordinary question:
zelph> a P279 b
zelph> b P279 c
zelph> c P279 d
zelph> a P279⁺ d
Error in line "a P279⁺ d": "⁺" and "∗" are condition operators: reachability is
what the engine WALKS, not what you assert. Write a variable to ASK ("S p⁺ b"),
or use the path as a condition -- in a rule, or in a query (a line with a
variable).
zelph> S P279⁺ d
Answer: a P279⁺ d
Answer: b P279⁺ d
Answer: c P279⁺ d
Every answer constitutes a ground path, and when entered again, it is the line refused above. In a query, the ground path functions as a condition in addition to the others, and when both endpoints are bound, it acts as a reachability test, just as it does within a rule. The single step beneath the marker constitutes a pattern at that location, hence S P279 d does not answer a P279 d:
zelph> X P279 b, a P279⁺ d
Answer: a P279 b, a P279⁺ d
zelph> X P279 b, d P279⁺ a
zelph> S P279 d
Answer: c P279 d
Writing ¬ in front makes no difference to that. ¬(F) denies a fact, and neither of these two is one – there is no claim of reachability, or of what a net believes, for a line to deny:
zelph> ¬(a P279⁺ d)
Error in line "¬(a P279⁺ d)": "⁺" and "∗" are condition operators, and a "¬" in
front does not change that: reachability is what the engine WALKS, so there is
no claim of it to deny. Write the path as a condition -- in a rule, or in a
query (a line with a variable) -- under "¬" if what you want is the absence of a
path.
zelph> ¬≈net(a p b)
Error in line "¬≈net(a p b)": "≈" is a condition operator, and a "¬" in front
does not change that: it asks what a network believes, which a condition can
read and a statement can neither claim nor deny. Write it as a condition -- in a
rule, or in a query (a line with a variable) -- under "¬" for the case the net
does not confirm.
Nor does putting them one argument down. A line lacking a variable possesses no condition slot at any level of nesting outside a rule it mentions, thus all three operators are rejected within one:
zelph> x mentions (≈net(a p b))
Error in line "x mentions (≈net(a p b))": "≈" is a condition operator and has no
meaning in a statement that asserts: it asks what a network believes, which a
condition can read -- in a rule, or in a query (a line with a variable) -- and a
statement cannot claim.
zelph> x mentions (a P279⁺ d)
Error in line "x mentions (a P279⁺ d)": "⁺" and "∗" are condition operators and
have no meaning inside a statement that asserts: reachability is what the engine
WALKS. A condition reads it -- in a rule, or in a query (a line with a
variable), where "S p⁺ b" asks for it.
Under ¬ in a condition – whether part of a rule or a query – both constitute ordinary tests, as detailed in the next section.
Inside a rule the three do have slots – but the slot is a whole condition, and an operator one argument further in is read by nothing. It is refused there too, in a condition and in a consequence alike:
zelph> (x q (¬(a p b))) => (c r d)
Error in line "(x q (¬(a p b))) => (c r d)": "¬" applies to a whole condition,
not to something inside one: it negates the condition it stands in front of,
and nothing below a condition reads it. Write it in front of the condition --
"(A q B, ¬(A p B)) => ...".
zelph> (A p B) => (x q (a P279⁺ d))
Error in line "(A p B) => (x q (a P279⁺ d))": "⁺" and "∗" mark the predicate of
a CONDITION, not of a fact inside one: the closure is walked for the condition
itself, and a marker below it tags a fact nothing ever walks. Write the path as
its own condition.
An inner rule is a rule, so a rule generator writing (P lifts Q) => ((X P Y, ¬(X Q Y)) => (X flagged Y)) is untouched by this: the ¬ there stands at the top of the inner rule’s own condition.
What ¬ may be applied to among the guards. Three conditions are not fact lookups but procedures the engine runs: the inequality guard !=, the neural condition ≈, and the path condition ⁺ / ∗. Two of them read under ¬ and one does not.
¬(C P⁺ T) and ¬≈net(S P O) are tests: the first succeeds when there is no path, the second when the net does not confirm the fact. Both need every term bound, because a negation binds nothing, and both say so when a term is open.
¬(X != Y) is rejected. It asks for the two terms to be the same node, and writing the same variable twice already asks that – with the advantage that the engine then uses it to narrow the search rather than testing afterwards:
The refusal comes when the rule is evaluated, not when it is read: != is a
guard the engine runs, so what is rejected is the negation of that execution,
and until a fact reaches the rule there is nothing to run.
zelph> (A prop X, A prop Y, ¬(X != Y)) => (A pair X)
((A prop Y), (A prop X), ¬(X != Y)) => (A pair X)
zelph> a prop v1
Error: ¬ cannot be applied to "!=" -- write the same variable on both sides to
require two terms to be equal.
Stratified Evaluation¶
A negated condition inquires into absence – but absence at what time? While a reasoning run is underway, facts continue to be derived; a negation assessed during the run might succeed merely because the matching fact had not yet been derived, and zelph never retracts a derived fact, meaning the deduction would stand. zelph therefore evaluates rules in strata:
- Positive stratum: every rule lacking negated conditions proceeds until quiescence (fixpoint) is reached.
- Deferred strata: rules whose conditions include negation at any level of nesting are processed with respect to that saturated state, advancing one negation level at a time.
Results arising from deferred rules may activate positive rules, leading to alternating phases at one level until no additional derivations can be made; only then does progression to the next level start. This ordering guarantees that negation-as-failure stays sound in a forward-chaining system: facts continuously accumulate, so a later derivation may cause a negation to fail but never cause it to succeed anew – a negation that succeeds at a stratum boundary is final, assuming no subsequent process can derive a fact that the negation had checked for absence. In terms of logic programming, evaluation is inflationary – facts are introduced only, never removed – whereas a program employing ¬ is non-monotonic: an additional fact may invalidate a negation and thus necessitate retracting a prior conclusion. The strata serve to harmonize these two aspects; for rules they cannot order, check mode reports a derived fact whose negated condition has come to hold.
The levels guarantee precisely that. A rule depends on another if the latter is able to produce a fact – anywhere within the depth of its conclusion – whose predicate is accessed by the former, either affirmatively or within a negation, and whose object is the same where both name a constant one, as detailed following the .strata examples below. A negated rule executes solely after every rule whose facts it tests under negation – either directly or via positive rules in between – has derived all possible derivations. When such facts are accessed solely in affirmation, it runs no lower than the rule that produces them, potentially at the same level, where the two alternate until neither derives anything new. Rules that negate outcomes they contribute to cannot be ordered in any way; they represent the first of the two boundaries mentioned below. In
zelph> (¬(:blockp A), (:start A)) => (:q A)
(¬(:blockp A), (:start A)) => (:q A)
zelph> (:q A) => (:blockr A)
zelph> ((:start A), ¬(:blockr A)) => (:s A)
(¬(:blockr A), (:start A)) => (:s A)
zelph> :start w
(:q w) ⇐ {(¬(:blockp w)) (:start w)}
(:blockr w) ⇐ (:q w)
the third rule tests blockr, which comes into existence solely after the first rule has derived q. Consequently, the third rule operates at a later level, finds (w blockr w), and derives nothing.
Both evaluation strategies – classic and semi-naive – implement the same execution sequence, incorporating a rule that another rule derives during the run: this rule is collected before the subsequent negation level execution. .semi-naive check examines the semi-naive aspect of this process. After the run concludes, it applies classic passes to the result and re-tests every negation that could have been invalidated by a newer fact, ensuring that any fact overlooked by delta-driven evaluation, or one dependent on a negation now holding true, is reported as an error. It does not separately execute the classic evaluator and then compare results. The manner in which this check anchors progress in engine development is described in Internals: Measurement Methodology.
The payoff is that universally quantified conditions can be written the way a textbook would state them. The primality rule
(N testprime N, &2 < N, ¬(N hasdivisor D)) => (N isprime N)
is sound in its current form: it is deferred until all potential divisors have been evaluated, thus the negation quantifies over the entire traversal. This is an argument concerning this specific program, and .strata does not make it: it lists the rule as non-stratifiable, due to the explanation provided at the end of this section. Refer to Semantic Arithmetic for the full module.
Two boundaries are worth knowing:
-
Rules that negate what they help derive. If the conclusions of a rule, through supplementary rules, can generate a fact that the rule’s own negation tests –
(A p A, ¬(A q A)) => (A r A)together with(A r A) => (A q A)– the program fails to have any stratified reading. These rules operate at the same level and alternate as previously outlined. This method remains sound only when every negation is settled by facts obtained during the identical positive saturation phase, which is precisely how the identity fallback in the simplifier is built; otherwise, the result depends on the order of evaluation, and with.parallel, this sequence can differ between runs. Contradiction rules (conclusion!) stay fully safe: they derive no facts at all. -
Stratification arranges derived facts, not your input. Negation is evaluated during each run, based on the asserted facts currently present. Should a negated pattern need to be blocked by base facts, assert those facts prior to the triggering fact. In a typed or piped session, and in a script specified via the command line, inference runs after each statement; a module imported using
.importexecutes just once, following complete reading, meaning the sequence within a module does not matter.
Both boundaries may leave behind the same signature: a fact that was derived under a negation that no longer holds. .semi-naive check explicitly looks for this exact scenario. Upon completion of each execution, it re-evaluates every negation that could have been invalidated by a newly introduced fact, and it reports every fact whose negated condition now holds and which is not derived through any alternative route. The fact persists, as facts are only added over time. Each rule continues to be satisfied – the rule that derived the fact now has a condition that fails – but the state contains a fact that none of your rules supports any more: it is not a supported model. Three types of rule are not re-tested, since the test cannot differentiate between a fact that has been lost and one that continues to be derived: a rule featuring a neural condition, a rule that negates a path condition, and a rule whose path condition binds a variable that neither a fact condition nor the conclusion binds. What check mode is unable to identify is a choice between two outcomes, both of which are logically consistent. With (:p A, ¬(:q A)) => (:r A) and (:p A, ¬(:r A)) => (:q A), :p w ends with either (w r w) or (w q w), depending on the order in which the rules execute, and the rules support either outcome.
Outside check mode, enabling .negation-records on maintains identical records and runs the same test following each execution, yet issues a warning for a fact whose negated premise now holds: the execution completes successfully, and the fact remains present. The warning names the fact alongside the rule that derived it, allowing a front end to inform the user that a later statement has defeated an earlier conclusion. A man is considered happy if every dog they possess barks, and h1 marks a man who owns a dog that does not bark:
zelph> .negation-records on
Negation records: on
zelph> (M ~ man, M owns D, D ~ dog, ¬(D barks nil)) => (M h1 nil)
zelph> (M ~ man, ¬(M h1 nil)) => (M is happy)
zelph> bill ~ man
(bill is happy) ⇐ {(bill ~ man) (¬(bill h1 nil))}
zelph> bill owns max
zelph> max ~ dog
(bill h1 nil) ⇐ {(max ~ dog) (bill ~ man) (¬(max barks nil)) (bill owns max)}
Warning: 1 fact(s) no longer justified -- a negated premise they were derived
under now holds, and nothing else derives them; they stay:
bill is happy (by ((M ~ man), ¬(M h1 nil)) => (M is happy))
zelph> john owns fido
zelph> fido ~ dog
zelph> john ~ man
(john h1 nil) ⇐ {(fido ~ dog) (john ~ man) (¬(fido barks nil)) (john owns fido)}
zelph> fido barks nil
Warning: 1 fact(s) no longer justified -- a negated premise they were derived
under now holds, and nothing else derives them; they stay:
john h1 nil (by ((D ~ dog), (M ~ man), ¬(D barks nil), (M owns D)) => (M h1 nil))
zelph> X is happy
Answer: bill is happy
The warning names the fact that has lost its support, not what that fact blocks. After fido barks, (john is happy) ought to follow, yet locating it would require assessing the rules as though (john h1 nil) had been removed – its withdrawal, which zelph does not perform. Nor does the warning refer to a fact that a rule lacking negation derived from the stale one, since that fact is still derived. The records are held in memory, one per fact that a rule with a negated condition derives, which is why the toggle is off by default: disabling it frees those records, .new and a .load that replaces the network discard them, and a saved network excludes them. Each record contains the fact, the rule, the rule’s condition set, and the variable bindings from the firing event: 72 bytes in an array that grows by doubling, plus 48 bytes per binding. Measured over 200,000 and 400,000 derived facts, the process grew by approximately 250 bytes per record for a rule binding one variable, and by an additional 60 bytes for each further variable, so a million such facts cost roughly a quarter to two fifths of a gigabyte. The time is spent on re-evaluation: after each execution, every record whose rule negates a predicate that has acquired new facts since the last check is re-verified under its bindings, taking about a microsecond per record, while the remaining records incur a pass across the array that was too small to measure at this size. A session holding a million records with auto-run enabled thus pays about one second after each statement that adds a fact to a negated predicate. A Janet program switches the records on via (zelph/negation-records true) and retrieves the list of the most recent run from (zelph/defeated).
A warning names a fact once, as its record is removed with the report. A run within a cluster that is dropped later gives its reports back, because the drop takes back what the cluster wrote, potentially including the defeating fact: a later run names the fact again where its negated premise holds, whereas merging the cluster keeps the report. A name merge (.name) runs no inference: any defeat induced by the merge is reported by the next run, and the records, much like the list returned by (zelph/defeated), follow the nodes the merge rebuilt.
.strata shows the levels of the rules in their current state, without executing any of them. Regarding the three rules from the example above:
zelph> .strata
2 negation levels:
Level 1:
(¬(:blockp A), (:start A)) => (:q A)
Level 2:
(¬(:blockr A), (:start A)) => (:s A)
The rule that derives blockr carries no negated condition and thus possesses no level; it runs whenever there is pending work. The figures correspond to those a .run announces as "negation level 2 of 2" once .log -1 is active, and the rules appear exactly as .list-rules prints them. When rules negate their own derived outcomes, .strata names them, alongside the positive rules that close the cycle – before any fact exists, which occurs earlier than check mode is able to indicate:
zelph> (¬(:q A), (:p A)) => (:r A)
(¬(:q A), (:p A)) => (:r A)
zelph> (:r A) => (:q A)
zelph> .strata
1 negation level:
Level 1:
(¬(:q A), (:p A)) => (:r A)
Not stratifiable, on level 1 -- these rules negate what they derive:
(:r A) => (:q A)
(¬(:q A), (:p A)) => (:r A)
A pattern positioned at the top of a condition or conclusion is compared by its predicate, and if its object corresponds to a single constant, that constant is also taken into account. Each class membership constitutes a ~ fact, and the objects keep rules about different classes apart; married, bachelor, and husband order these two rules across two distinct levels:
zelph> (X ~ man, ¬(X ~ married)) => (X ~ bachelor)
zelph> (X ~ man, ¬(X ~ bachelor)) => (X ~ husband)
zelph> .strata
2 negation levels:
Level 1:
(¬(X ~ married), (X ~ man)) => (X ~ bachelor)
Level 2:
((X ~ man), ¬(X ~ bachelor)) => (X ~ husband)
A variable located in the object position, a term or several objects, and each statement enclosed within a pattern represent facts involving any object: a negation of (X ~ married) also waits for a rule that derives (X ~ C). A path condition counts as its predicate with any object, because its walk traverses facts that involve any object. When a rule governing predicates like the transitivity rule is in force, no object undergoes comparison (see Rules over predicates).
The analysis does not compare entire patterns, implying it also identifies cycles that only the subjects of the facts would resolve. Two shipped modules exemplify this behaviour. The gate rule in binary-nand-arithmetic negates ((A nand B) out 0), and the gate rules that read the out facts it generates yield out facts where the output is a variable, for instance ((A and B) out V). The primality rule referenced earlier appears alongside the entire arithmetic set, because the rule that reports its result, (N testprime N, N isprime N) => ((N testprime N) = prime), closes the cycle twice: it creates an = fact, which serves as the predicate for every arithmetic result the divisor scan reads, and the (N testprime N) within it initiates the scan. Neither element can produce a fact that the negation depends on. The = fact features a testprime term as its subject, never one of the arithmetic terms the scan reads, and (N testprime N) is already present, as it is the rule’s own premise. Consequently, every hasdivisor fact is derived before the rule’s level runs, and check mode confirms this during every run.
Rules over predicates¶
A meta-rule features a variable in place of the predicate, meaning the analysis cannot determine which predicates it creates.
When this variable corresponds to the predicate of a fact the rule has matched – (R is transitive, A R B, B R C) => (A R C), and likewise for the symmetric and reflexive rule – the rule only extends predicates that already possess associated facts, and the levels remain unchanged: whatever is awaiting those facts is already awaiting whatever generates them.
Which predicates the rule extends is determined by the declaration it reads, (R is transitive), hence every negation is positioned after the rules that derive such declarations. As long as this rule remains in force, the analysis compares predicates independently of their objects: the facts it produces inherit their objects from other facts – (w linked b) and (b linked c) give (w linked c) – and the predicates it extends are determined by the declarations present within the facts.
A rule that takes the predicate it creates from the subject or object of a fact – such as the opposite relations rule (R "is opposite of" S, X R Y) => (Y S X), or a sub-property axiom (P subpropertyof Q, X P Y) => (X Q Y) – or that reads a second predicate variable, is considered to create every predicate.
This kind of rule joins every negating rule it can reach into a single level, where they alternate as outlined in the first boundary description, and is listed under "Not stratifiable" in .strata.
Expressed as a rule that derives rules, (P subpropertyof Q) => ((X P Y) => (X Q Y)), the identical axiom maintains distinct levels, since each rule it derives explicitly names its predicates.
A rule that derives a rule is considered to create whatever the rule it writes will create, which is stated in the conclusion of that rule before its existence: (R kind gen) => ((X R Y) => (X qq Y)) is considered to create qq facts, hence a rule that negates qq depends on it, while other negations do not. When the conclusion contains a variable in the predicate position, as seen in the schemas above, it is treated as creating every possible predicate. After being written, the rule undergoes analysis just like any other, and the levels are recalculated before the subsequent level runs.
Inequality Constraints¶
The != operator is a built-in guard constraint — not a fact lookup.
It filters variable bindings after the involved variables are bound by positive conditions.
Key design decision: In zelph, two different variable names may bind to the same node.
This is consistent with standard first-order logic where ∀x ∀y. P(x,y) does not exclude x = y.
To require distinct bindings, an explicit != constraint is needed.
zelph> (A prop X, A prop Y, X != Y) => (A has_pair X Y)
((A prop Y), (X != Y), (A prop X)) => (A has_pair Y X)
zelph> a prop v
With only one value v, the binding X = v, Y = v is blocked by !=, so the rule does not fire.
zelph> a prop v1
(a has_pair v v1) ⇐ {(a prop v) (v1 != v) (a prop v1)}
zelph> a prop v2
(a has_pair v v2) ⇐ {(a prop v2) (v != v2) (a prop v)}
(a has_pair v1 v2) ⇐ {(a prop v2) (v1 != v2) (a prop v1)}
Once distinct values exist, the rule fires for the distinct pairings – for
every one of them, v included, since it too differs from the new values.
Practical use case — detecting functional-property violations (a pattern from Wikidata ontology work):
zelph> (P is functional, A P X, A P Y, X != Y) => !
((A P Y), (A P X), (P is functional), (X != Y)) => !
zelph> date_of_birth is functional
zelph> alice date_of_birth 1990
zelph> alice date_of_birth 1991
! ⇐ {(alice date_of_birth 1990) (alice date_of_birth 1991) (date_of_birth is functional) (1991 != 1990)}
Found one or more contradictions!
Without !=, the rule would also fire when the same value is entered redundantly, which is not a real conflict.
The standard library’s symbolic modules guard their own results with this pattern: (T simp A, T simp B, A != B) => ! reports a term that has reached two normal forms, and a rule with identical form reports a term possessing two raw derivatives with respect to the same variable (see The Symbolic Layer).
Why != matters — preventing spurious deductions:
Without !=, rules that quantify over pairs can produce false positives from reflexive bindings:
(X opposite Y, A ~ X, A ~ Y) => !
bright opposite bright
yellow ~ bright
Without !=, the engine binds X = bright, Y = bright, satisfies all conditions, and fires the contradiction — even though yellow is merely classified under the same category twice.
Adding X != Y blocks this reflexive binding and prevents the false positive.
Constraint checking — Graph coloring:
Multiple != constraints can enforce pairwise distinctness, enabling constraint-checking patterns:
zelph> (A adjacent B, A color X, B color X) => !
((B color X), (A adjacent B), (A color X)) => !
zelph> r1 adjacent r2
zelph> r2 adjacent r3
zelph> r1 color red
zelph> r2 color blue
zelph> r3 color red
No contradiction — the coloring is valid. But assigning r2 color red instead would trigger the contradiction, since adjacent regions r1 and r2 would share the same color.
Self-joins: derive the selection first¶
A rule that pairs a relation with itself is quadratic in that relation, and != does not
make it cheaper — the guard filters bindings after the join has produced them. When the
pairs you actually want are a small subset picked out by other conditions, deriving that
subset first and joining over it is the same statement in a far cheaper order:
# quadratic over every `hits` fact, then filtered
(A hits B, A hits C, B != C, B holds K, K ~ valuable, C holds L, L ~ valuable)
=> (A ~ double_attacker)
# the selection pushed below the join
(A hits B, B holds K, K ~ valuable) => (A threatens B)
(A threatens B, A threatens C, B != C) => (A ~ double_attacker)
Both derive the same facts. On a base of ~200 facts in which about 60 were hits and 8 of
those were threats, the two-rule form ran 14× faster — and the whole rule set it belonged
to went from 4.07 ms to 0.96 ms.
The reason is worth knowing, because it tells you when to expect this. optimize_order plans
the join by boundness: a condition whose subject and objects are already bound scores
higher, because unification can resolve it without scanning. It does not know how many
facts a relation has, and cannot — that is a property of the data, not of the rule. So the
planner can put a resolvable condition first, but it cannot tell a scan over 60 facts from a
scan over 8. Where a relation's size is what makes one order cheap, the rule author supplies
that knowledge by naming the smaller relation.
The same reasoning applies to a negated condition or an ≈ condition inside a self-join: both
are evaluated per candidate binding, so anything that shrinks the candidate set first pays for
itself.
"Is this the only one?"¶
A derived marker also answers the question that looks as if it needed a negation over a
conjunction — ¬(A prop Y, X != Y), which is not expressible. Derive the positive case with
the guard, then negate that single pattern:
zelph> b prop w
zelph> a prop v1
zelph> a prop v2
zelph> (A prop X, A prop Y, X != Y) => (A ~ several)
((X != Y), (A prop Y), (A prop X)) => (A ~ several)
(a ~ several) ⇐ {(v2 != v1) (a prop v1) (a prop v2)}
zelph> (A prop X, ¬(A ~ several)) => (X ~ sole)
(¬(A ~ several), (A prop X)) => (X ~ sole)
(w ~ sole) ⇐ {(¬(b ~ several)) (b prop w)}
Observe the sequence: facts precede rules. Evaluation of negation occurs per run based on the current state of the facts, and a derived fact is never revoked – given only a prop v1 in the graph, the second rule derives v1 ~ sole, and the subsequent arrival of a prop v2 cannot undo this.
Fresh Variables: Generative Rules¶
Variables that appear only in the consequence of a rule are treated as fresh: the engine generates new anonymous nodes for them during inference.
zelph> .deductions all
Deduction printing mode: all
Every derivation is printed.
zelph> (A is human) => (B nameof A)
zelph> tim is human
(?? nameof tim) ⇐ (tim is human)
zelph> X nameof tim
Answer: ?? nameof tim
The ?? represents a newly created node — an existential witness materialized in the graph.
It is the same node in both lines; a node the engine generated has no name to print.
.deductions all is needed here and is not decoration.
The default mode is quiet, which prints a deduction only when its subject came from something you entered (reference) — and the subject of a generative rule's consequence is the generated node itself, which by definition never did.
The fact is derived and stored either way; only the line announcing it is suppressed.
A fresh variable is not permitted to serve as a predicate. There exists no condition that provides a relation for it, and substituting a new node in its place would result in a relation type that remains unnamed by anyone, hence a rule whose consequence writes a fact using such a predicate is rejected upon creation. A negated condition does not bind anything, thus a variable that is named solely by a negated condition is considered unbound. The inner rule within a rule generator takes its predicate from the generator’s binding at the time the generator builds it, and a rule that a statement mentions does not fire, so neither is refused:
zelph> (X waits nil) => (X W nil)
Error in line "(X waits nil) => (X W nil)": The predicate of "X W nil" in the
rule's consequence is the variable W, which no condition binds: a firing has no
predicate to write, and a new node standing in for one would be a relation type
without a name. Bind W in a condition, or write the predicate as a name.
A rule expressed one fact at a time – using zelph/fact in Janet, or with zelph_fact in the C ABI – undergoes verification later than a typed rule, because the =>-writing call cannot know whether a generator or a statement will hold it: at the conclusion of the outermost Janet evaluation that wrote it, and before the next run or save. A rule that remains in force at that moment is removed and rejected, whereas an inner rule and a rule a statement holds are permitted to pass (refer to zelph/rule and zelph_fact). A rule authored by zelph/mention or zelph_mention constitutes a mention, and a call claiming it brings it into force: that call undergoes verification in the same way, and its rejection retracts the claim alone, leaving the rule as a mention.
No duplicate witnesses: Before producing a new node, zelph checks whether any assignment of the fresh variables already makes every consequence of the rule into a fact; if such an assignment exists, the rule creates nothing for this match. This verification operates as a join akin to the one applied across a rule’s conditions, meaning that any node can function as a witness, including the subject itself – a q a satisfies (A q B) for a – whereas a pattern that a rule merely records, among them its own consequence, never qualifies. A consequence is considered present even though it is not a fact when its instance would keep a variable from a rule it mentions, such as k about ((C r D, C s D) => (c q d)): a firing keeps the conditions of a mentioned rule exactly as written, meaning the instance would be rule text, no firing derives it (see Mentioning a Rule Is Not Asserting It), and the check concentrates exclusively on the remaining consequences. A consequence is likewise considered present when a rule inside a value constructed by the firing would keep a variable: within a value, the firing keeps every variable it leaves unbound, including a fresh variable for which only a consequence that is not derived would make a witness. A consequence that no firing writes, since the binding makes its predicate one of its objects, is regarded as present in the same way: given a p a, the rule (X p Y) => (Z Y X) (Z r X) makes one witness for Z r a and no additional witness. A witness that has already been made stays, even if a subsequent fact alone would have satisfied the consequence.
The arithmetic that follows requires no such thing: a rule builds a result list like (D cons T) using variables its conditions bound, and a fact node built from those identical components is the same node.
The check does not make every generative rule terminate. A rule whose consequence meets its own condition once more, with the newly created node placed in a new position, never stops:
(X p Y) => (Y p Z)
a p b
derives b p ??, followed by a fact concerning that newly created node, then another regarding the subsequent one, indefinitely. Datalog engines employing existential rules face the same limit; preventing these rules from feeding themselves rests with the rule set.
A collection literal within a consequence generates nodes too: during a firing, a collection is built for every binding of the consequence’s variables (refer to A literal a rule derives). Building it again under the identical binding finds the same node, hence such a rule terminates provided that what it builds does not re-enter its own binding. In the rules presented below, it does, so .run would not return, nor would a statement typed with auto-run on; single passes illustrate the outcome:
zelph> .auto-run
Auto-run is now disabled.
zelph-> .deductions all
Deduction printing mode: all
Every derivation is printed.
zelph-> (X p Y) => (X likes @{bucket})
zelph-> (X likes C) => (C p k)
zelph-> b p k
zelph-> .run-once
...
(b likes @{bucket}) ⇐ (b p k)
...
zelph-> .run-once
...
(@{bucket} p k) ⇐ (b likes @{bucket})
(@{bucket} likes @{bucket}) ⇐ (@{bucket} p k)
...
zelph-> .run-once
...
(@{bucket} p k) ⇐ (@{bucket} likes @{bucket})
(@{bucket} likes @{bucket}) ⇐ (@{bucket} p k)
...
The @{bucket} printed here represent distinct collections: the one built for b, followed by the one built for that collection, and so forth. They print alike because each contains solely bucket. Starting from the second pass onward, each pass introduces four nodes – the p fact associated with the last collection, the subsequent collection featuring its member bucket, and the likes fact that refers to it – and no pass constitutes the final one. The rules define precisely this behaviour, as every newly formed collection corresponds to a new binding of X, and zelph evaluates them exactly as written; when a shared object is meant, a set constant or a named node explicitly indicates it, and {bucket} in the first rule ends the example after three deductions.
A Predicate Logic Perspective¶
For readers with a background in formal logic, here is how zelph's constructs map to first-order logic.
Universal Quantification¶
Variables in rule conditions behave like universally quantified variables. The transitive-closure rule
(R is transitive, X R Y, Y R Z) => (X R Z)
reads as:
with the caveat that quantification ranges over the current fact base (closed-world evaluation), rather than over every conceivable interpretation. R occupies the predicate position and is quantified, an operation that standard first-order syntax does not allow: in zelph it ranges over nodes, not over relations, thus R(X,Y) serves as an abbreviation for holds(R, X, Y) – the encoding detailed in Prolog and Datalog – and under this interpretation the formula is first-order.
Existential Quantification¶
Fresh variables (those present solely in the consequence) represent constructive existential quantification, assessed in the manner of the restricted chase when handling existential rules: a new node is created only if no assignment of the fresh variables already makes the consequence hold (refer to Fresh Variables). Thus, the witness does not constitute a Skolem term of the condition variables: an existing node may serve as its substitute, and the order in which matches are examined not only determines which node that is but also whether a new node is created at all. With .parallel, this sequence differs across executions, meaning two runs on identical input may derive distinct facts (see Deduction Output Modes). In contrast, a collection constructed by a consequence is a Skolem term: its node is determined by the collection written in the rule and by the binding of the consequence’s variables, so a firing under the same binding will locate it again, and no alternative node can substitute for it.
Conjunction¶
The comma-separated condition syntax (cond1, cond2, cond3) is a conjunction: all conditions must match under a shared variable assignment. The conditions are evaluated as a joint constraint (the semantics are order-independent, even if the engine may internally choose an evaluation order for efficiency).
Negation¶
¬(Pattern) corresponds to negation-as-failure (NAF) — the same semantics as in Datalog with stratified negation or Prolog's \+.
It tests the absence of evidence in the current graph state, not the evidence of absence in the model-theoretic sense.
Readers familiar with Answer Set Programming (ASP) or well-founded semantics will recognize this as a form of default negation operating over the graph's Herbrand base. zelph enforces these semantics operationally by deferring rules with negated conditions until the positive rules reach their fixpoint (see Stratified Evaluation).
Inequality¶
The != operator corresponds to dif/2 in Prolog or disequality constraints in CLP(FD).
It is a guard, not a fact pattern.
Disjunction¶
zelph currently supports conjunction but not explicit disjunction in rule conditions. As in Datalog, disjunction is expressed through multiple rules with the same consequence pattern:
(A is bird) => (A can fly)
(A is bat) => (A can fly)
This is equivalent to (bird(A) ∨ bat(A)) → can_fly(A).
When both branches hold, the consequence is derived once, not twice: a fact is a node and nodes are hash-consed, so the second rule finds the fact the first one made. A query therefore answers a doubly-justified conclusion exactly once.
Unary Predicates and Self-Facts¶
A zelph fact establishes a connection from a subject to a single object via a predicate, or to an unordered set of objects (refer to Facts with Multiple Objects); there is no specific form for arity-1 facts. Consequently, a unary predicate P(x) can be expressed as a self-fact – a fact in which the subject and object are the identical node:
x P x
The term is zelph’s own coinage; in graph-theoretic terms, a self-fact corresponds to a loop at x, while in relational terms, it positions x along the diagonal of the binary relation P – asserting P(x) through x P x represents a standard encoding of unary predicates within a formalism whose primitive is a binary relation. The alternative is class membership, x ~ P, which the symbolic modules use for denoting sorts (x ~ symvar). The standard library uses self-facts as request markers: (N testprime N) initiates a primality test, (T simplify T) activates simplification. The self-fact prefix : enables bidirectional ease – :testprime N as input, and the identical concise form as output.
A natural question, especially from a mathematical perspective: why not
assign every operator a fixed arity — simplify unary, + binary — so
that simplify(T) is primitive and no marker encoding is needed? The
answer is the first-class-predicate design discussed
above: a predicate in zelph is an ordinary node
without a signature. The node + is not exclusively an operator. The fact
(&2 + &3) is itself a node that appears as the subject of the result
fact ((&2 + &3) = &5); meta-rules quantify over predicates (R is
transitive); and facts may carry several objects, so even "binary" is not
structurally fixed. A schema layer assigning arities would have to
constrain exactly the flexibility that makes
meta-rules expressible.
Consequently, whether a predicate acts as a term-forming operator or as a
marker is knowledge of the module that defines it, not of the engine —
which is why the corresponding display decision is a script-level
declaration (zelph/no-selffact-sugar, the same philosophy as
zelph/number), not a built-in rule.
Semantic Math: Computation as Graph Rewriting¶
Numbers in zelph are not opaque primitives.
They are cons-lists of digit nodes — topological structures within the graph, built from the same cons and nil predicates used for any list.
Arithmetic is not hard-coded; it is defined by inference rules that transform these structures.
This architecture has a remarkable consequence: calculating numbers and reasoning about numbers happen in the same system.
If a knowledge base (e.g. Wikidata) records that 13 is a prime number, that semantic fact is directly accessible wherever the list <13> appears in a computation.
Numbers as Cons-Lists¶
The list <42> is internally stored as 2 cons (4 cons nil) — least significant digit first.
The display reverses the order for human readability, so results appear in conventional notation.
For details on the list syntax, see Angle Brackets: Lists.
This representation means digits are ordinary named nodes.
The node "4" is the same node everywhere in the graph — in a number, in a Wikidata entity, in a classification.
Peano-style Successor Addition¶
The simplest possible addition rule uses a successor table:
zelph> <0> followed-by <1>
zelph> <1> followed-by <2>
zelph> <2> followed-by <3>
zelph> (A followed-by B) => ((<1> + A) = B)
((<1> + <0>) = <1>) ⇐ (<0> followed-by <1>)
((<1> + <2>) = <3>) ⇐ (<2> followed-by <3>)
((:+ <1>) = <2>) ⇐ (<1> followed-by <2>)
This states: if A is followed by B in the number succession, then 1 + A = B.
The engine derives one sum per successor fact, and it derives them in whatever
order the run reaches them. (<1> + <1>) = <2> is among them: subject and
object of the sum coincide there, so it is printed with the
self-fact prefix as (:+ <1>) = <2>, which
re-enters as the same fact.
The key point: followed-by is a user-defined relation. zelph has no arithmetic kernel. The rule works because the graph contains the corresponding facts.
Rule-based Multi-digit Addition¶
Deep dive: this section develops the addition module as a proof of concept. The dedicated page Semantic Arithmetic covers the full arithmetic system — subtraction, comparison, and multiplication — the shared architecture behind all four rule modules, the base-independence property, and the engine machinery (bound-pattern grounding, semi-naive evaluation) that makes rule-based computation fast.
zelph is capable of executing arbitrary-precision addition exclusively through graph rules. The rules are located in stdlib/common-arithmetic.zph; the digit tables they access originate from a substrate module, stdlib/decimal-arithmetic.zph for base 10 or stdlib/binary-arithmetic.zph for base 2. Neither script includes any rule; both import the identical recursion module. In base 2, the addition knowledge shrinks to the 16 facts of a full adder truth table, manually authored, meaning the binary module does not require any generated lookup table – except for a single Janet block at the decimal interface (handling literal conversion and display registration), it is composed entirely in native zelph syntax. The recursion rules are independent of base, clearly illustrating that the base is a property of the data, not of the rules.
The algorithm consists of three parts:
1. A digit-level lookup table (generated programmatically via Janet):
For all digits a,b ∈ {0..9} and carry-in c ∈ {0,1}, two facts encode the sum and carry-out:
((a d+ b) tci c) sum swiths = (a + b + c) mod 10((a d+ b) tci c) co ewithe = ⌊(a + b + c) / 10⌋
This turns digit arithmetic into ordinary facts in the network — 200 entries total.
2. Base cases for the recursion endpoint (when both operands are nil):
((nil add nil) ci 0) sum nil((nil add nil) ci 1) sum <1>
3. Eight inference rules that decompose, propagate carries, assemble results, and connect to the user-facing = predicate.
The rules handle three cases each for decomposition (both operands non-nil, left nil, right nil) and assembly, plus a trigger rule and a connection rule.
A Worked Example¶
Note: since
decimal-arithmetic.zphregisters its digit alphabet, a live session displays these lists as decimal&-literals (e.g.&12345instead of<12345>).The intermediate states below are shown with
.deductions all. The default mode (quiet) derives them all the same but prints only the final=fact — see Deduction Output Modes.
.import decimal-arithmetic
(<12345> + <98765>) = X
Trigger (Rule A0): Seeds the internal addition state with carry-in 0:
((&12345 add &98765) ci 0)
Decomposition (Rules D1–D3): Peels off least-significant digits, propagates carry:
((&1234 add &9876) ci 1)
((&123 add &987) ci 1)
((&12 add &98) ci 1)
((&1 add &9) ci 1)
Base case: The recursion ends at nil + nil with carry-in 1:
(((nil add nil) ci 1) sum &1)
Assembly (Rules As1–As3): Constructs the result on the way back up, prepending digits via cons:
(((&1 add &9) ci 1) sum &11)
(((&12 add &98) ci 1) sum &111)
...
(((&12345 add &98765) ci 0) sum &111110)
Connection (Rule C0): Exposes the result under the user-facing = predicate:
((&12345 + &98765) = &111110)
Nothing in the engine is hard-coded for addition. The computation emerges from the same topological primitives used for ordinary knowledge representation — facts, conjunctions, cons-lists — plus eight generic inference rules.
Asserting vs. Querying¶
&123456 + &987654 is an assertion, not a query: it adds the + fact to the
graph, and the inference engine derives the result (plus all intermediate
add/ci/sum states) exactly once. Re-entering the same assertion produces
no output -- the fixpoint has already been reached, which is correct
forward-chaining behaviour. To retrieve a result (again), use a query:
(&123456 + &987654) = X
Queries contain variables and are always evaluated, so this prints the result no matter how often it is repeated. The derived intermediate facts deliberately stay in the graph: they are reusable knowledge for subsequent computations. To sandbox a computation instead, wrap it in a cluster and drop it afterwards.
By default, the REPL's deduction trace is filtered to facts about your input; see Deduction Output Modes.
Semantic Integration with Knowledge Graphs¶
Because list elements are ordinary graph nodes, any arithmetic rule that produces a digit automatically inherits all semantic facts known about that digit. If the Wikidata graph is loaded, querying all prime numbers is a standard pattern query:
.lang wikidata
X P31 Q49008
This lists all 10,018 prime numbers recorded in Wikidata — the same nodes that would appear in a cons-list produced by arithmetic rules. Knowledge and computation are not separate layers.
Comparison and Subtraction¶
The addition pattern extends further: the shared recursion module additionally establishes comparison and subtraction, both of which remain unaltered across every substrate – only the digit tables vary (100/400 generated facts in base 10, 4/16 manually crafted facts in base 2; the subtraction table corresponds to the truth table of a full subtractor).
Comparison (N cmp M) walks both lists LSB-first and combines a digit table (dcmp) with a dominance rule: the more significant rest determines the outcome unless it is eq, in which case the current digit pair governs the result. In all cases, the current cells must be digits: a list that includes any cell which is not a digit fails to be a number, thus its comparison yields no result: (<x 1> cmp &0) does not yield a <, > or == fact, and (<x 1> cmp &0) = X returns no answer. Missing digits are zero-extended, ensuring that lists with leading zeros are compared by value accurately. The results are ordinary relational facts – N < M, N > M, N == M – and hence can be combined with meta-rules just like any explicitly stated fact:
(R is transitive, A R B, B R C) => (A R C)
> is transitive
&30 cmp &20
...
(&30 > &20) ⇐ {((&30 lcmp &20) res gt) (&30 cmp &20)}
...
&20 cmp &10
...
(&20 > &10) ⇐ {((&20 lcmp &10) res gt) (&20 cmp &10)}
...
(&30 > &10) ⇐ {(> is transitive) (&20 > &10) (&30 > &20)}
Computed order and declared knowledge feed the same inference engine.
Additionally, the outcome is exposed under = for uniform result queries: (A cmp B) = X answers gt/lt/eq.
Subtraction (N - M) mirrors addition exactly, with borrow (bi/bo)
instead of carry. It is deliberately a partial function on the naturals:
if M > N, the borrow chain reaches the base case with borrow-in 1, for
which no base fact exists — the derivation simply produces no result.
Undefinedness is encoded as the absence of a fact; no error machinery is
involved.
Non-canonical results: performing digit-wise subtraction may generate
lists that begin with leading zeros (&105 - &98 produces the raw
difference <007>). This list keeps its <...> presentation, as the
&-display mandates the canonical form; the = result is normalized
((&105 - &98) = &7), and comparisons evaluate such lists as equal by
value ((<007> cmp &7) = eq) – yet they persist as separate nodes.
Operands are expected in the canonical form produced by &-literals.
Multiplication: Cross-Module Computation¶
Multiplication completes the picture and introduces a new structural element:
rules that delegate to other rule modules. The recursion runs over the
first operand's digits — (A cons R) × M = A×M + base × (R×M) — and because
numbers are stored LSB-first, multiplying by the base is a single cons:
base × X = (0 cons X). No shift machinery exists; it falls out of the
representation.
The digit-times-number products use a third digit table (dx, with running
carry — 1800 generated facts in base 10, 16 hand-written facts in base 2: an
AND gate plus increment, completing the full-adder/full-subtractor family).
The accumulation, however, is not implemented in the multiplication module at
all: rule MA1 asserts an ordinary + fact, the addition module derives its
= result through its own rules, and rule MA2 consumes it. Computation
cascades across modules through nothing but shared facts — the same mechanism
that lets computed comparison facts feed declared meta-rules.
Just as with the other operations, the multiplication rules are defined only once, in common-arithmetic.zph, and execute unchanged across every substrate. Because intermediate states are represented as hash-consed graph nodes, partial products that have common suffixes are inherently shared – memoization is a property of the representation, not an added capability.
A schema note for rule authors: all three digit tables are keyed by dedicated table-carry predicates (
tcifor the addition and multiplication tables,tbifor subtraction) while recursion states useci/bi/mci. Keeping table space and state space on distinct predicates ensures tables are only ever accessed through direct, grounded lookups and never appear in the extensions scanned when a rule's first condition is matched -- those extensions then contain nothing but the small, dynamic recursion states. Sharingtcibetween two tables is deliberately harmless: table-keying predicates are never scanned.
Division and remainder complete the four operations; see Semantic Arithmetic for the candidate-selection design.
Number Literals¶
Cons-lists are a general-purpose structure — numbers are merely one use of them, and zelph deliberately does not hard-code any numeric representation. Which base is used, or whether digits are decimal characters at all, is decided entirely by the loaded rule scripts. The parser, however, offers two pieces of syntax sugar that make the numeric use case pleasant without constraining it:
-
Inverting angle brackets. Compact lists like
<123>reverse their characters before cons construction, so the least significant digit becomes the outermost cell — the natural orientation for right-to-left arithmetic rules (see Angle Brackets: Lists). -
The
&prefix. A token like&42is always decimal input, regardless of the internal representation. The parser transforms it into(zelph/number "42")— a call to the redefinable Janet functionzelph/number, whose default implementation raises an error until a representation is loaded.stdlib/decimal-arithmetic.zphmaps it to a decimal digit list (&42≡<42>), whilestdlib/binary-arithmetic.zphconverts to base 2 (&5≡<101>). The prefix applies unconditionally: a token starting with&is a number literal, and if the loadedzelph/numbercannot interpret it, that is an error — by design, there is no silent fallback to an atom. Every stdlib substrate reads the literal the same way, which is what makes them interchangeable under the shared module IDarithmetic: non-digits are rejected (&abcis an error, not a cons list of letters), and leading zeros are stripped, so&007and&7denote the same node. (The choice of&is a small homage to classic home-computer BASICs, where&prefixed number literals.) -
Symmetric output. The display side mirrors the input side: a script can register its digit alphabet via
(zelph/set-number-digits ["0" "1" ...])(digit nodes or names, in ascending order of value). From then on,node_to_stringrenders any properlynil-terminated cons list that contains solely registered digit nodes and is in canonical form (with no leading zeros) as a decimal&-literal – regardless of the internal base.stdlib/decimal-arithmetic.zphregisters0–9,stdlib/binary-arithmetic.zphregisters0and1, so both display&5for their respective internal lists<5>and<101>. Any other cons list -- including lists of single-character nodes that are not registered digits -- keeps the generic<...>display, so cons lists remain general-purpose. An empty array disables the feature.
This split keeps the philosophy intact: the representation of numbers lives in scripts and rules, while the convenience of familiar decimal input lives in the parser — decoupled through one redefinable function.
Beyond Arithmetic¶
The methods illustrated by the addition algorithm – deep unification, recursive decomposition using cons-lists, result lists built from bound variables (hash-consed, ensuring identical lists share a single node), and lookup tables operating at the digit level – are general-purpose. They apply whenever computation can be expressed as structure transformation across a graph.
Statements About Statements¶
Because fact nodes can themselves appear as subjects or objects, zelph naturally supports higher-order assertions. For example, declaring a relation to be symmetric, transitive, or functional is a statement about a predicate — and the inference engine treats it as an ordinary fact that conditions can match against.
This allows for concise, generic rules. In traditional logic programming, the same takes an encoding of each fact in Datalog, or a call via a variable predicate (call/N) in Prolog.
Neural Rule Conditions¶
Since version 0.9.7, rule conditions can also consult a neural network living inside the same graph, via the ≈ operator — verifying facts against a learned model (guard mode) or generating candidate bindings above a confidence threshold (generator mode), with the confidence flowing into the deduced fact's probability. This neuro-symbolic capability has its own page: Neural Networks in the Graph.
Transitive Path Conditions¶
A condition may follow a predicate any number of steps instead of exactly one. Suffix the predicate with ⁺ (U+207A) for one or more steps, or with ∗ (U+2217) for zero or more:
zelph> Q1 P279 Q2
zelph> Q2 P279 Q3
zelph> Q3 P279 Q4
zelph> alice member Q1
zelph> (X member C, C P279⁺ T) => (X "belongs to" T)
((C P279⁺ T), (X member C)) => (X "belongs to" T)
(alice "belongs to" Q2) ⇐ {((Q1 P279 Q2) closure one-or-more) (alice member Q1)}
(alice "belongs to" Q3) ⇐ {((Q1 P279 Q3) closure one-or-more) (alice member Q1)}
(alice "belongs to" Q4) ⇐ {((Q1 P279 Q4) closure one-or-more) (alice member Q1)}
C is bound by the first condition, so the path condition walks forward from Q1 and produces one binding for T per class reached. With the target bound instead, it walks backward; with both ends bound it is a reachability test that filters rather than generates. Reachability is answered by the same indexed closure engine utilized by zelph/closure and the SPARQL layer’s p+ / p* – constructed once per predicate and stored alongside the .bin file until a fact involving that predicate is modified, rather than walked for each query.
A walk proceeds through the facts that satisfy a condition and nothing else: a rule’s own pattern does not constitute a step, nor does the engine’s bookkeeping, that is, the mark of such a pattern and the record of a contradiction (see Contradiction Detection).
Both ends free is refused, with a message asking you to bind one: a path over an unanchored pair would enumerate every path in the graph. A path condition terminating in a constant is not held back: it is processed according to the same scoring mechanism as any other condition, and frequently scheduled first, as a walk originating from the constant through the indexed closure is computationally inexpensive. It only delays execution when both of its endpoints remain unbound, awaiting another condition to bind one; thus, the order in which conditions are written has no influence. The predicate itself must be a concrete predicate — a closure is indexed per predicate, and quantifying over predicates remains the business of an ordinary condition, which can do it.
The operator is not a reserved character. It is read only as a trailing marker in predicate position, and only when a name is left over once it is removed, so Na⁺ is an ordinary node name in any position, a⁺b is an ordinary predicate, and ⁺ on its own is the predicate ⁺. ASCII + deliberately has no such reading, because z+ and d+ are the addition predicates of the arithmetic modules, and * is the focus operator.
Like ≈, the sugar is input syntax over an ordinary fact: (C P279⁺ T) is the fact ((C P279 T) closure one-or-more), and when this fact is typed within a condition, it is the same condition. In any context where a condition appears – within .list-rules, in the echo of a rule or query – it prints as the sugar form, which re-enters as the identical rule. It appears so in all other contexts too – the fact displayed independently, as (zelph/rules) hands it out, within .node, inside a statement that holds it, or in a rule that a statement mentions – since closure and one-or-more are names in the zelph language: spelled out under .lang en, the fact points to other nodes and constitutes a different statement. The commands that take a fact as input – .node, .mermaid, .explain – take it in that same spelling: .node a P279⁺ b finds the condition that .node printed as a P279⁺ b. The premises after ⇐, and the entries in .explain, are not conditions, but instead represent the facts recognized during a firing, hence they refer to the fact.
A marker on a self-fact inquires if a node reaches itself, since :pred X is (X pred X) and predicate position is where the marker is read. That is a cycle test, and it needs nothing beyond what is already here – one condition to bind the node, and the path condition to ask:
zelph> Q1 ~ class
zelph> Q2 ~ class
zelph> Q5 ~ class
zelph> Q7 ~ class
zelph> Q1 P279 Q2
zelph> Q2 P279 Q1
zelph> Q5 P279 Q6
zelph> Q7 P279 Q7
zelph> (C ~ class, :P279⁺ C) => (C "sits in a cycle" C)
((C ~ class), (:P279⁺ C)) => (C "sits in a cycle" C)
(Q1 "sits in a cycle" Q1) ⇐ {(Q1 ~ class) ((:P279 Q1) closure one-or-more)}
(Q2 "sits in a cycle" Q2) ⇐ {(Q2 ~ class) ((:P279 Q2) closure one-or-more)}
(Q7 "sits in a cycle" Q7) ⇐ {(Q7 ~ class) ((:P279 Q7) closure one-or-more)}
Q5 is excluded: it has a superclass, but no path back to itself. Q7 serves as its own superclass, forming a loop of one step and thus constituting a path of length one. With ∗ every node qualifies instead, since zero steps is a path.
Under ¬ the condition asks the same question the other way round: does this node not reach that one.
zelph> Q1 P279 Q2
zelph> Q2 P279 Q3
zelph> Q4 P279 Q9
zelph> alice member Q1
zelph> bob member Q4
zelph> (X member C, ¬(C P279⁺ Q3)) => (X clear-of Q3)
((X member C), ¬(C P279⁺ Q3)) => (X clear-of Q3)
(bob clear-of Q3) ⇐ {(bob member Q4) (¬((Q4 P279 Q3) closure one-or-more))}
alice is excluded since Q1 reaches Q3 in two steps. A negated path condition requires both ends bound, and it reports it otherwise: the affirmative version accepts one bound endpoint and produces the other, but a negation binds nothing, thus there is nothing for an open endpoint to transform into. "Reaches nothing at all" poses a distinct inquiry, and it is asked by binding the far end.
The cost operates in reverse as well, and it is important to recognize prior to crafting one for a large graph. The positive form walks the closure once from the bound end. The negated form involves a test for each candidate, so a rule whose other conditions leave thousands of candidates incurs one reachability walk for each of them. Where the inquiry is genuinely a set difference over one predicate – every class below A that is not below B – the SPARQL layer's MINUS computes the two closures once and subtracts, which is the shape to reach for at that scale.
A result derived through a path condition stays reconstructible. .explain marks the walked premise [closure] rather than [axiom], because nobody asserted the path — the engine walked it, and there is no fact to expand further:
zelph> .explain (alice "belongs to" Q4)
alice "belongs to" Q4
├─ alice member Q1 [axiom]
└─ (Q1 P279 Q4) closure one-or-more [closure]
Contradiction Detection¶
Rules with ! as the consequence detect logical inconsistencies:
zelph> (X "is opposite of" Y, A ~ X, A ~ Y, X != Y) => !
((X "is opposite of" Y), (A ~ X), (X != Y), (A ~ Y)) => !
zelph> bright "is opposite of" dark
zelph> yellow ~ bright
zelph> yellow ~ dark
! ⇐ {(bright "is opposite of" dark) (yellow ~ bright) (bright != dark) (yellow ~ dark)}
Found one or more contradictions!
When a contradiction is detected during fact assertion, the contradictory fact is not entered into the graph. Instead, a record of the contradiction is stored, making it visible in reports. This mechanism is central to zelph's Wikidata ontology work, where thousands of constraint violations in the knowledge graph are detected automatically.
The record is a fact in the graph, and it says what a contradiction says: the set of the statements that matched, entered as refuted – these do not hold together. None of them is retracted; each stays asserted and keeps answering queries, and the set is the only node created.
That is also why a contradiction is announced once rather than on every later run. A set constant is identified by its members, so the same contradiction always yields the same node, and the next run finds it already there – the same way a derived fact stays quiet the second time because the graph holds it. Details, including the switch that turns the record off, are on the overview page and in .help .contradiction-records.
The record stands as the engine’s own account of the contradiction, not a declaration made by anyone: it answers no query and matches no rule condition, nor do the memberships within its set. A refutation you compose yourself functions as a statement and continues to answer as previously:
zelph> (X p Y, X q Y) => !
zelph> a p b
zelph> a q b
! ⇐ {(a p b) (a q b)}
Found one or more contradictions!
zelph> ¬(c p d)
zelph> S ~ refuted
Answer: (c p d) ~ refuted
zelph> S in O
zelph>
Otherwise, a rule whose condition matches ~ facts and whose consequence refutes a claimed fact would meet the record of each contradiction it causes as a new fact, causing its execution to never end.
A set constant consists solely of its content, so a set that a statement names over the same facts is the record’s set as well, and it stays that statement’s set: its memberships answer as those of any set do, while the marking ~ refuted continues to belong exclusively to the record. A ground rule condition that names the record yields no match, and zelph/exists reports the record as missing, because it asks what a rule condition asks; a path condition likewise does not traverse the record. zelph/sources, zelph/targets, and .node enumerate it, reflecting the graph’s structural perspective:
zelph> {(a p b) (a q b)} label foo
zelph> (X p Y, X q Y) => !
! ⇐ {(a q b) (a p b)}
Found one or more contradictions!
zelph> (a p b) in O
Answer: (a p b) in {(a p b) (a q b)}
zelph> ({(a p b) (a q b)} ~ refuted) => (k r s)
zelph> S r O
A rule featuring one condition not enclosed within a condition set is recorded just like any other (refer to the overview page). A rule whose conditions consist entirely of negations, guards, or paths does not have a matched fact to record and is announced on every run.
Silence differs from a clean graph, thus the summary of a run says which of the two applies. A network that already holds records reports them next to the count of what this run found: 0 contradictions found (1 already recorded in this network). The number is extracted from the graph rather than counted as the run meets them, so it counts contradictions and not the rule instantiations that reach them – a symmetric rule matches the same pair twice and still reports one. A network you downloaded therefore states what it holds on the very first run over it.
Wikidata at Scale¶
zelph can load and reason over millions of Wikidata facts. A typical consistency check uses negation to detect missing inverse relations:
.load wikidata-20260309-all-pruned-medium.bin
.lang wikidata
(X P361 Y, ¬(Y P527 X)) => !
.run
Here, P361 ("part of") and P527 ("has part") are inverse properties. The rule flags every entity declared "part of" something whose parent does not list it among its parts.
On wikidata-20260309-all-pruned-medium.bin this reports 355,073 contradictions from 547,551 unification matches, in five minutes of reasoning. How many a given network yields depends on which one – each published variant carries a different set of individual items – but the order of magnitude is the point: these are not a handful of stragglers. They are also not necessarily errors, since they may reflect deliberate modeling choices about redundancy; detecting them systematically is the first step toward improving data quality at scale. This is exactly the kind of analysis performed in the Wikidata Ontology Cleaning Task Force, supported by a Wikimedia Community Fund grant.
The Programmatic Layer: Janet¶
zelph embeds Janet, a lightweight functional programming language, as its scripting layer. Janet serves as a powerful macro system: it constructs graph structures that are then processed by zelph's reasoning engine. During inference, only zelph's native engine runs.
Janet is used for:
- Generating facts programmatically — e.g. the 200-entry digit addition lookup table is generated by a Janet loop, not entered manually.
- Parameterized rules — functions that create rule topologies for any relation.
- Querying and inspecting the graph —
zelph/queryreturns results as Janet data structures. - External integration — Janet's standard library provides file I/O, networking, and data processing, enabling zelph to exchange data with external systems.
For the full Janet API reference and examples, see the Janet scripting documentation.
A quick taste — generating a transitive rule for any relation:
%
(defn transitive-rule [rel]
(zelph/rule
[(zelph/fact 'X rel 'Y)
(zelph/fact 'Y rel 'Z)]
(zelph/fact 'X rel 'Z)))
(transitive-rule "is part of")
(transitive-rule "is ancestor of")
%
A single function call creates the entire rule topology — conjunction set, conditions, consequence, and the => link — for any named relation.
Getting Started¶
To try zelph yourself, see the Quick Start Guide for pre-compiled binaries on all major platforms. The interactive REPL lets you enter facts and rules and observe inference in real time — every example on this page can be entered directly.
The project is open source (AGPL v3 / commercial dual license) and hosted on GitHub.