Datalog, with Nemo and clingo

path(?x, ?z) :- edge(?x, ?y), path(?y, ?z) .

Why Datalog

A language with no loops, no variables to assign and no control flow, which is exactly why it can answer questions SQL struggles with.

Datalog is a small logic language. You write down facts, you write down rules for deriving new facts, and an engine works out everything that follows. There is no order of execution to think about, because there is no execution in the sense you are used to: the engine keeps applying rules until a round produces nothing new, and then stops.

That is the whole idea. It sounds limiting, and the limits are what make the guarantees possible: every Datalog program terminates, every program has exactly one answer, and the engine is free to evaluate it in whatever order is fastest. Hold on to both promises, because the rest of the book is honest about their price: arithmetic can buy back non-termination if you let it, and one of the two engines here will deliberately trade the single answer away for something it wants more.

hello.rls

%! The smallest complete Nemo program.
%!
%! Run: nmo hello.rls -e idb
%! Verify: path = a b | a c | a d | b c | b d | c d

%%% Facts: what we were told.
edge(a, b) .
edge(b, c) .
edge(c, d) .

%%% Base case: an edge is a path.
path(?from, ?to) :- edge(?from, ?to) .

%%% Recursive case: an edge followed by a path is a path.
path(?from, ?to) :- edge(?from, ?middle), path(?middle, ?to) .

@export path :- csv{resource="paths.csv"} .

Two rules. The first says an edge is a path. The second says an edge followed by a path is a path. Between them they define reachability over a graph of any shape and any size, and the engine works out how to compute it.

Here is the same thing in the two languages you would otherwise reach for.

SQL

-- Transitive closure in SQL. This is the shortest correct version.
WITH RECURSIVE in_network(x, y) AS (
    -- The anchor member: the base case.
    SELECT person_a, person_b FROM knows

    UNION            -- UNION rather than UNION ALL, or a cycle runs forever

    -- The recursive member. It may reference in_network exactly once, may
    -- not appear on the right of an outer join, may not use an aggregate,
    -- and may not appear in a subquery. The restrictions differ by engine.
    SELECT k.person_a, n.y
    FROM knows k
    JOIN in_network n ON k.person_b = n.x
)
SELECT * FROM in_network;

-- Two mutually recursive relations are where this stops being practical.
-- A CTE can reference itself but not another recursive CTE, so a pair of
-- rules that each mention the other has no direct translation at all.

Python 3.12

"""What a Datalog engine does, written out by hand.

Naive evaluation: apply every rule to everything known, add whatever is new,
and repeat until a round adds nothing. That last condition is the fixpoint,
and it is why recursion in Datalog terminates without anyone bounding it.
"""


def transitive_closure(edges: set[tuple[str, str]]) -> set[tuple[str, str]]:
    # Round zero: the base rule, path(X, Y) :- edge(X, Y).
    paths = set(edges)

    while True:
        # The recursive rule, path(X, Z) :- edge(X, Y), path(Y, Z).
        derived = {
            (x, z)
            for (x, y) in edges
            for (y2, z) in paths
            if y == y2
        }

        new = derived - paths
        if not new:
            # Nothing changed, so nothing ever will. Stop.
            return paths
        paths |= new


def main() -> None:
    edges = {("a", "b"), ("b", "c"), ("c", "d")}
    for pair in sorted(transitive_closure(edges)):
        print(pair)

    # Everything an engine adds to this is performance and honesty:
    # semi-naive evaluation joins only against the facts the last round
    # produced, indexes pick the join order, and stratification decides when
    # negation is allowed to look at a predicate. None of it changes the
    # answer, which is what makes the answer worth trusting.


if __name__ == "__main__":
    main()

What you get

recursion

Recursion that is not an afterthought

A rule may mention itself, and mutually recursive rules are ordinary. SQL's WITH RECURSIVE allows one self reference under a list of restrictions, and two rules that each mention the other have no translation at all.

joins

Joins with nowhere to put a mistake

Reusing a variable name is the join. There is no ON clause to get wrong, no alias to mix up, and no accidental cross product from a forgotten condition.

termination

It always finishes

Every fact is derived once and there is no way to invent new values out of thin air, so evaluation reaches a fixed point. A recursive rule cannot run away, which is why nobody writes a depth limit.

planning

The engine chooses the order

Rules are a specification, not a procedure. Join order, indexes and evaluation strategy belong to the engine, so a change in the data changes the plan rather than the program.

Two engines, two different questions

This book uses two, because they answer genuinely different questions and the difference is worth understanding early.

	Nemo	clingo
Asks	what follows from these facts	does a world exist where these hold
Answer	every derived fact	a model, or a proof that none exists
Negation	stratified, one fixed answer	full stable model semantics
Contradiction	not expressible, a violation is just another fact	first class, and UNSAT is a result
Optimisation	none	`#minimize` and `#maximize`
Scale	streams bottom up over millions of facts	grounds everything into memory, so small worlds
Reach for it when	you want a report of what is true	you want a proof, a plan or a counterexample

nmo program.rls -e idb

Installing Nemo and clingo

Two binaries, no build system and no project layout. You can be running rules inside five minutes, and in the browser inside one.

install.sh

# Nemo. A single Rust binary, with nothing to configure.
# Assets are named per release, so the tag goes in the URL.
curl -fsSL -o nemo.tar.gz \
  https://github.com/knowsys/nemo/releases/download/v0.10.0/nemo_v0.10.0_x86_64-unknown-linux-gnu.tar.gz
tar -xzf nemo.tar.gz && mv nmo ~/.local/bin/
nmo --version

# There is also a browser playground at https://tools.iccl.inf.tu-dresden.de/nemo/,
# which needs no install at all and is the fastest way to try a rule.

# clingo. A Python wheel, a conda package, or your distribution. The wheel
# installs the module only: it puts no `clingo` command on PATH, so you run it
# as `python3 -m clingo`, and that entry point always exits zero.
pip install clingo          # then: python3 -m clingo program.lp
conda install -c potassco clingo
#   macOS      brew install clingo
#   Debian     apt install gringo   # this is the package that ships clingo
clingo --version

# Souffle, if you are working with the examples in the Souffle chapter.
# There is no souffle package in Debian or Ubuntu: take the .deb built for
# your release from the GitHub releases page.
#   macOS      brew install souffle
#   Debian     curl -LO https://github.com/souffle-lang/souffle/releases/download/2.5/x86_64-ubuntu-2404-souffle-2.5-Linux.deb
#              sudo apt install ./x86_64-ubuntu-2404-souffle-2.5-Linux.deb

Nemo

One Rust binary from the GitHub releases page. Nothing to configure and nothing to link against. There is also a browser playground, which runs the same engine compiled to WebAssembly and is the quickest way to try a rule you are unsure about.
clingo

pip install clingo gives you the Python module, but no clingo command on your PATH: run it as python3 -m clingo. The wheel and the native binary differ in one way worth knowing: the wheel's python3 -m clingo always exits zero, while the native binary uses exit codes to report the answer.
An editor

Neither ships a language server, and none I know of exists. Syntax files exist for Vim and VS Code, and the honest answer is that these languages are small enough that a comment describing each predicate's columns does more good than any tooling would.

Running something

Terminal

$ nmo hello.rls -e idb
Reasoning completed in 0ms. Derived 9 facts.
   Data import:     0ms
   Reasoning:       0ms
   Data export:     0ms
$ ls results
edge.csv
paths.csv

-e idb is the flag to learn first. It ignores the export directives and dumps every predicate the rules derived, which is what you want while the rules are still being written.

hello.lp

% The smallest complete clingo program.
% Run:    clingo hello.lp
% Expect: SATISFIABLE, 1 model, containing path(a,b), path(b,c), path(c,d),
%         path(a,c), path(b,d) and path(a,d).

edge(a, b).
edge(b, c).
edge(c, d).

% Variables are capitalised, constants are not. That is the whole rule.
path(X, Y) :- edge(X, Y).
path(X, Z) :- edge(X, Y), path(Y, Z).

#show path/2.

Command	Does
nmo program.rls	run, and write whatever @export says
nmo program.rls -e idb	dump every derived predicate instead
nmo program.rls -e none	evaluate and write nothing, the fastest sanity check
nmo program.rls --trace 'fact(a)'	print the proof tree for one fact
clingo program.lp	find one model
clingo program.lp 0	find all of them
clingo program.lp --text	show the grounding rather than the models
clingo program.lp --enum-mode=cautious	what is true in every model

path(X, Y) :- edge(X, Y).

Your first rules, in both engines

The same three-node graph in Nemo and in clingo, so the syntactic differences are out of the way before anything interesting starts.

Both engines are Datalog underneath and they write it differently. Getting the differences straight now means the rest of the book can talk about ideas rather than punctuation.

hello.rls

%! The smallest complete Nemo program.
%!
%! Run: nmo hello.rls -e idb
%! Verify: path = a b | a c | a d | b c | b d | c d

%%% Facts: what we were told.
edge(a, b) .
edge(b, c) .
edge(c, d) .

%%% Base case: an edge is a path.
path(?from, ?to) :- edge(?from, ?to) .

%%% Recursive case: an edge followed by a path is a path.
path(?from, ?to) :- edge(?from, ?middle), path(?middle, ?to) .

@export path :- csv{resource="paths.csv"} .

hello.lp

% The smallest complete clingo program.
% Run:    clingo hello.lp
% Expect: SATISFIABLE, 1 model, containing path(a,b), path(b,c), path(c,d),
%         path(a,c), path(b,d) and path(a,d).

edge(a, b).
edge(b, c).
edge(c, d).

% Variables are capitalised, constants are not. That is the whole rule.
path(X, Y) :- edge(X, Y).
path(X, Z) :- edge(X, Y), path(Y, Z).

#show path/2.

	Nemo	clingo
Variables	?x, ?name	X, Name
Constants	alice, "alice"	alice, "alice"
Rule	head :- body .	head :- body.
Space before the full stop	conventional	not used
Comment	%	%
Negation	~atom	not atom
Anonymous	_	_
Output	@export p :- csv{...} .	#show p/2.
Ranges	not built in	1..10
Strings	first class, with functions	opaque constants

clingo coloring.lp 0

$ clingo coloring.lp 0
clingo version 5.6.2
Reading from coloring.lp
Solving...
Answer: 1
assign(1,green) assign(2,blue) assign(3,green) assign(4,red)
Answer: 2
...
SATISFIABLE

Models       : 18
Calls        : 1
Time         : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

The three parts of every program

Facts are what you were told. edge(a, b) . asserts that this relation holds between these two constants. In database language these are the extensional database, and in practice they come from a CSV file, a query, or a compiler front end rather than from the program text.

Rules derive new facts. head :- body reads as "head holds if body holds", and the comma between body atoms is an AND. Several rules with the same head are an OR. These are the intensional database, which is to say the interesting part.

Directives say where facts come from and where results go. They differ most between engines and matter least to the logic.

Try it yourself

The graph already has four nodes. Add the one edge that closes it into a cycle, edge(d, a), then run both programs again. Predict how many path facts you will get before you look.

Hint: Every node now reaches every node, including itself. Four nodes give sixteen paths, and neither engine loops forever working that out.

Show one solution

hello.rls

%! The smallest complete Nemo program.
%!
%! Run: nmo hello.rls -e idb
%! Verify: path = a b | a c | a d | b c | b d | c d

%%% Facts: what we were told.
edge(a, b) .
edge(b, c) .
edge(c, d) .

%%% Base case: an edge is a path.
path(?from, ?to) :- edge(?from, ?to) .

%%% Recursive case: an edge followed by a path is a path.
path(?from, ?to) :- edge(?from, ?middle), path(?middle, ?to) .

@export path :- csv{resource="paths.csv"} .

SELECT ... JOIN ... ON -> a(?x, ?y), b(?y, ?z)

The SQL translation table

Everything you already know how to write, and what it turns into here. Worth keeping open for the first week.

SQL	Datalog	Note
`CREATE TABLE person(...)`	nothing, or `.decl` in Souffle	Nemo and clingo infer the schema from use
`INSERT INTO person VALUES ('ada')`	`person("ada") .`	a fact is a row
`CREATE VIEW`	a rule	except that views here can be recursive
`SELECT name FROM p WHERE age > 18`	`adult(?n) :- p(?n, ?a), ?a > 18 .`	the head is the SELECT list
`JOIN b ON a.id = b.id`	`a(?id, ?x), b(?id, ?y)`	the shared variable is the condition
`UNION`	two rules with the same head	duplicates never arise, so there is no ALL
`NOT EXISTS (SELECT ...)`	`~b(?x)` or `not b(X)`	the variable must be bound positively first
`GROUP BY region`	region appears in the head, unaggregated	grouping is implicit
`COUNT(*), SUM(x)`	`#count(?id)`, `#sum(?x, ?id)`	over distinct tuples, which is the opposite default
`WITH RECURSIVE`	a rule that mentions itself	no restrictions, and no UNION ALL trap
`DISTINCT`	nothing	a relation is a set, so it is always implied
`ORDER BY, LIMIT`	nothing	a relation has no order. Sort where you consume the output
`NULL`	nothing	an absent fact is the absence, and there is no three valued logic
`LEFT JOIN`	two rules, or an existential	one for the matched case, one for the unmatched

The same three questions, three ways

Nemo

%! Joins, filters and projections, which are the three things SQL does.
%! Verify: unarmed = Sam
%! Verify: ancientWarrior = Legolas Bow | Gimli Axe

%%% character(name, race, age)
character("Frodo", "Hobbit", 50) .
character("Sam", "Hobbit", 38) .
character("Legolas", "Elf", 2931) .
character("Gimli", "Dwarf", 139) .
character("Aragorn", "Human", 87) .

%%% weapon(owner, item, damage)
weapon("Frodo", "Sting", 15) .
weapon("Legolas", "Bow", 20) .
weapon("Gimli", "Axe", 25) .
weapon("Aragorn", "Anduril", 30) .

%%% A filter and a projection. The underscore says the column is not needed.
hobbit(?name) :- character(?name, "Hobbit", _) .

%%% A join. Writing ?name in both atoms is the join condition.
armed(?name, ?item) :- character(?name, _, _), weapon(?name, ?item, _) .

%%% A join with a comparison on top of it.
ancientWarrior(?name, ?item) :-
    character(?name, _, ?age),
    weapon(?name, ?item, _),
    ?age > 100 .

%%% An anti-join. The variable has to be bound positively first, which is
%%% why character comes before the negation.
unarmed(?name) :- character(?name, _, _), ~weapon(?name, _, _) .

%%% A self join: two characters of the same race who are not the same person.
sameRace(?a, ?b) :-
    character(?a, ?race, _),
    character(?b, ?race, _),
    ?a != ?b .

@export ancientWarrior :- csv{resource="ancient.csv"} .
@export unarmed :- csv{resource="unarmed.csv"} .

SQL

-- The same three questions, in the language you already write.
-- Filtering and projection.
SELECT name
FROM character
WHERE race = 'Hobbit';

-- A join, where the condition has to be spelled out and can be wrong.
SELECT c.name, w.item
FROM character c
JOIN weapon w ON c.name = w.owner
WHERE c.age > 100;

-- An anti-join. Three ways to write it, two of which behave badly when the
-- column can be NULL, and the reason so much SQL advice is about NOT IN.
SELECT c.name
FROM character c
WHERE NOT EXISTS (
    SELECT 1 FROM weapon w WHERE w.owner = c.name
);

Python 3.12

"""The joins from the tutorial, written imperatively.

Each one works. Each one also fixes a decision the Datalog version leaves to
the engine: which relation to scan first, what to index, and in what order to
apply the filters. Change the data and those decisions go stale.
"""

characters = [
    ("Frodo", "Hobbit", 50),
    ("Sam", "Hobbit", 38),
    ("Legolas", "Elf", 2931),
    ("Gimli", "Dwarf", 139),
    ("Aragorn", "Human", 87),
]

weapons = [
    ("Frodo", "Sting", 15),
    ("Legolas", "Bow", 20),
    ("Gimli", "Axe", 25),
    ("Aragorn", "Anduril", 30),
]


def hobbits() -> list[str]:
    return [name for name, race, _ in characters if race == "Hobbit"]


def ancient_warriors() -> list[tuple[str, str]]:
    # An index, because the nested loop version is quadratic and this one is
    # not. In Datalog the engine builds this and picks the order itself.
    by_owner: dict[str, list[tuple[str, int]]] = {}
    for owner, item, dmg in weapons:
        by_owner.setdefault(owner, []).append((item, dmg))

    return [
        (name, item)
        for name, _, age in characters
        if age > 100
        for item, _ in by_owner.get(name, [])
    ]


def unarmed() -> list[str]:
    armed = {owner for owner, _, _ in weapons}
    return [name for name, _, _ in characters if name not in armed]


if __name__ == "__main__":
    print(hobbits())
    print(ancient_warriors())
    print(unarmed())

ancestor(?c, ?a) :- ancestor(?c, ?m), parent(?m, ?a) .

Facts, rules and what an engine does with them

The whole language is two constructs. Understanding how the engine gets from one to the other is most of understanding Datalog.

fact: A ground atom, meaning one with no variables in it. person("ada") is a fact. Facts are what you supply.
rule: head :- body. Read the turnstile as if. The body is a conjunction of atoms and comparisons; the head is one atom that follows from them.
EDB: The extensional database: the predicates you supplied facts for. In practice, whatever came out of your CSV, your database or your compiler.
IDB: The intensional database: the predicates that only rules produce. These are the answers.
ground: Containing no variables. Grounding a rule means substituting constants for its variables, which is literally what clingo does before it solves.
fixpoint: The state where applying every rule to everything known produces nothing new. Evaluation stops there, and that is why it stops at all.

family.rls

%! Ancestors, and the ones two people share.
%! Verify: nearestShared = alice
%! Verify: sharedAncestor = alice

father(bob, alice) .
father(daniel, cho) .
mother(cho, alice) .
mother(eiko, cho) .
mother(eiko, finley) .

%%% Two rules with the same head are an OR: a parent is a father or a mother.
parent(?child, ?p) :- father(?child, ?p) .
parent(?child, ?p) :- mother(?child, ?p) .

%%% The base case and the recursive case, which is all transitive closure is.
ancestor(?child, ?a) :- parent(?child, ?a) .
ancestor(?child, ?a) :- ancestor(?child, ?middle), parent(?middle, ?a) .

%%% Reusing ?a in both atoms is the join: an ancestor of one and of the other.
sharedAncestor(?a) :- ancestor(bob, ?a), ancestor(eiko, ?a) .

%%% The nearest shared ancestor: one with no descendant who also qualifies.
%%% Derive the ones that are not nearest, then negate. Negation needs a
%%% fully computed predicate underneath it, which this gives it.
notNearest(?a) :- sharedAncestor(?a), sharedAncestor(?below), ancestor(?below, ?a) .
nearestShared(?a) :- sharedAncestor(?a), ~notNearest(?a) .

@export nearestShared :- csv{resource="nearest.csv"} .

How the engine actually evaluates this

Bottom up, in rounds. Round one applies every rule whose body is satisfied by the facts you supplied, and adds what comes out. Round two applies every rule again, now with the round one results available. This continues until a round adds nothing.

On the family program above, watch it happen. The five father and mother facts become five parent facts in one application. Those become five base ancestor facts. The recursive rule then extends the new ones by a parent each round: the first extension finds the two grandparent paths, daniel to alice through cho and eiko to alice through cho, and the next round joins those two against parent, finds that alice has no parent on record, adds nothing, and stops. Seven ancestor facts, and the stopping condition was not a bound anyone wrote; it was the data running out of ways to be extended.

The negated rules at the bottom of the file wait their turn. nearestShared asks whether notNearest holds, so it cannot run until notNearest is completely finished, which cannot happen until sharedAncestor is. The engine sorts that dependency order out on its own, and the sorting has a name, stratification, which gets a chapter of its own once negation does.

Naive evaluation does exactly that and redoes an enormous amount of work each round. Semi-naive evaluation, which is what every real engine uses, only joins against the facts the previous round produced, since anything derivable from older facts was already derived. The answer is identical; the difference is the constant factor, and it is large.

This is why the order of your rules does not matter, and why the order of atoms within a body does not change the answer. It can change the speed, and the engine is the one that decides.

Reading a rule out loud

The habit that catches most mistakes: read a rule as an English sentence, with "for all" in front of it and "and" between the body atoms.

ancestor(?child, ?a) :- ancestor(?child, ?middle), parent(?middle, ?a) . reads as: for all child, middle and a, if middle is an ancestor of child and a is a parent of middle, then a is an ancestor of child. Any variable that appears in only one place could have been an underscore, and any variable that appears in two places is a join.

Try it yourself

Add a sibling rule to the family program. Then look at your output and work out why everybody is their own sibling, and fix it.

Hint: Two people share a parent, including each person with themselves. The fix is a disequality: ?a != ?b.

Show one solution

family.rls

%! Ancestors, and the ones two people share.
%! Verify: nearestShared = alice
%! Verify: sharedAncestor = alice

father(bob, alice) .
father(daniel, cho) .
mother(cho, alice) .
mother(eiko, cho) .
mother(eiko, finley) .

%%% Two rules with the same head are an OR: a parent is a father or a mother.
parent(?child, ?p) :- father(?child, ?p) .
parent(?child, ?p) :- mother(?child, ?p) .

%%% The base case and the recursive case, which is all transitive closure is.
ancestor(?child, ?a) :- parent(?child, ?a) .
ancestor(?child, ?a) :- ancestor(?child, ?middle), parent(?middle, ?a) .

%%% Reusing ?a in both atoms is the join: an ancestor of one and of the other.
sharedAncestor(?a) :- ancestor(bob, ?a), ancestor(eiko, ?a) .

%%% The nearest shared ancestor: one with no descendant who also qualifies.
%%% Derive the ones that are not nearest, then negate. Negation needs a
%%% fully computed predicate underneath it, which this gives it.
notNearest(?a) :- sharedAncestor(?a), sharedAncestor(?below), ancestor(?below, ?a) .
nearestShared(?a) :- sharedAncestor(?a), ~notNearest(?a) .

@export nearestShared :- csv{resource="nearest.csv"} .

armed(?n, ?i) :- character(?n, _, _), weapon(?n, ?i, _) .

Joins, filters and projection

Everything a SELECT does, expressed by where you put a variable name.

joins.rls

%! Joins, filters and projections, which are the three things SQL does.
%! Verify: unarmed = Sam
%! Verify: ancientWarrior = Legolas Bow | Gimli Axe

%%% character(name, race, age)
character("Frodo", "Hobbit", 50) .
character("Sam", "Hobbit", 38) .
character("Legolas", "Elf", 2931) .
character("Gimli", "Dwarf", 139) .
character("Aragorn", "Human", 87) .

%%% weapon(owner, item, damage)
weapon("Frodo", "Sting", 15) .
weapon("Legolas", "Bow", 20) .
weapon("Gimli", "Axe", 25) .
weapon("Aragorn", "Anduril", 30) .

%%% A filter and a projection. The underscore says the column is not needed.
hobbit(?name) :- character(?name, "Hobbit", _) .

%%% A join. Writing ?name in both atoms is the join condition.
armed(?name, ?item) :- character(?name, _, _), weapon(?name, ?item, _) .

%%% A join with a comparison on top of it.
ancientWarrior(?name, ?item) :-
    character(?name, _, ?age),
    weapon(?name, ?item, _),
    ?age > 100 .

%%% An anti-join. The variable has to be bound positively first, which is
%%% why character comes before the negation.
unarmed(?name) :- character(?name, _, _), ~weapon(?name, _, _) .

%%% A self join: two characters of the same race who are not the same person.
sameRace(?a, ?b) :-
    character(?a, ?race, _),
    character(?b, ?race, _),
    ?a != ?b .

@export ancientWarrior :- csv{resource="ancient.csv"} .
@export unarmed :- csv{resource="unarmed.csv"} .

SQL

-- The same three questions, in the language you already write.
-- Filtering and projection.
SELECT name
FROM character
WHERE race = 'Hobbit';

-- A join, where the condition has to be spelled out and can be wrong.
SELECT c.name, w.item
FROM character c
JOIN weapon w ON c.name = w.owner
WHERE c.age > 100;

-- An anti-join. Three ways to write it, two of which behave badly when the
-- column can be NULL, and the reason so much SQL advice is about NOT IN.
SELECT c.name
FROM character c
WHERE NOT EXISTS (
    SELECT 1 FROM weapon w WHERE w.owner = c.name
);

Python 3.12

"""The joins from the tutorial, written imperatively.

Each one works. Each one also fixes a decision the Datalog version leaves to
the engine: which relation to scan first, what to index, and in what order to
apply the filters. Change the data and those decisions go stale.
"""

characters = [
    ("Frodo", "Hobbit", 50),
    ("Sam", "Hobbit", 38),
    ("Legolas", "Elf", 2931),
    ("Gimli", "Dwarf", 139),
    ("Aragorn", "Human", 87),
]

weapons = [
    ("Frodo", "Sting", 15),
    ("Legolas", "Bow", 20),
    ("Gimli", "Axe", 25),
    ("Aragorn", "Anduril", 30),
]


def hobbits() -> list[str]:
    return [name for name, race, _ in characters if race == "Hobbit"]


def ancient_warriors() -> list[tuple[str, str]]:
    # An index, because the nested loop version is quadratic and this one is
    # not. In Datalog the engine builds this and picks the order itself.
    by_owner: dict[str, list[tuple[str, int]]] = {}
    for owner, item, dmg in weapons:
        by_owner.setdefault(owner, []).append((item, dmg))

    return [
        (name, item)
        for name, _, age in characters
        if age > 100
        for item, _ in by_owner.get(name, [])
    ]


def unarmed() -> list[str]:
    armed = {owner for owner, _, _ in weapons}
    return [name for name, _, _ in characters if name not in armed]


if __name__ == "__main__":
    print(hobbits())
    print(ancient_warriors())
    print(unarmed())

The four operations

Operation	How
Projection	Put in the head only the variables you want. Everything else is dropped, and an underscore says a column is not needed at all.
Selection	A comparison in the body, such as `?age > 100`, or a constant in an argument position, such as `character(?n, "Hobbit", _)`.
Join	The same variable in two atoms. There is no separate syntax, which is why a join condition cannot be forgotten or written the wrong way round.
Union	Two rules with the same head. Since a relation is a set, duplicates never appear and there is nothing corresponding to UNION ALL.

Order does not change the answer

a(?x, ?y), b(?y, ?z) and b(?y, ?z), a(?x, ?y) mean the same thing, and both engines are free to evaluate whichever way is cheaper. That is a real difference from a hand written loop, where the order is the plan and goes stale when the data changes.

It also means you cannot hand tune a join by rearranging the body, which is occasionally frustrating. Souffle provides .plan for exactly that case, and needing it is rare enough that neither engine here offers one.

Try it yourself

Write a rule for characters who own a weapon strictly stronger than every weapon owned by any hobbit. Then check whether your answer would still be right if there were no hobbits at all.

Hint: Derive the maximum hobbit damage first, then compare against it. The no-hobbits case is why: with no maximum derived, the rule produces nothing rather than everything, which may or may not be what you meant.

Show one solution

joins.rls

%! Joins, filters and projections, which are the three things SQL does.
%! Verify: unarmed = Sam
%! Verify: ancientWarrior = Legolas Bow | Gimli Axe

%%% character(name, race, age)
character("Frodo", "Hobbit", 50) .
character("Sam", "Hobbit", 38) .
character("Legolas", "Elf", 2931) .
character("Gimli", "Dwarf", 139) .
character("Aragorn", "Human", 87) .

%%% weapon(owner, item, damage)
weapon("Frodo", "Sting", 15) .
weapon("Legolas", "Bow", 20) .
weapon("Gimli", "Axe", 25) .
weapon("Aragorn", "Anduril", 30) .

%%% A filter and a projection. The underscore says the column is not needed.
hobbit(?name) :- character(?name, "Hobbit", _) .

%%% A join. Writing ?name in both atoms is the join condition.
armed(?name, ?item) :- character(?name, _, _), weapon(?name, ?item, _) .

%%% A join with a comparison on top of it.
ancientWarrior(?name, ?item) :-
    character(?name, _, ?age),
    weapon(?name, ?item, _),
    ?age > 100 .

%%% An anti-join. The variable has to be bound positively first, which is
%%% why character comes before the negation.
unarmed(?name) :- character(?name, _, _), ~weapon(?name, _, _) .

%%% A self join: two characters of the same race who are not the same person.
sameRace(?a, ?b) :-
    character(?a, ?race, _),
    character(?b, ?race, _),
    ?a != ?b .

@export ancientWarrior :- csv{resource="ancient.csv"} .
@export unarmed :- csv{resource="unarmed.csv"} .

reaches(?x, ?z) :- reaches(?x, ?y), edge(?y, ?z) .

Recursion and the fixpoint

The reason to use this language at all. A rule may mention itself, mutual recursion is ordinary, and neither can fail to terminate.

graphs.rls

%! Graph recipes: reachability, cycles, components and distance.
%! Verify: inCycle = a | b | c
%! Verify: component = a a | b a | c a | d a | e e | f e

edge(a, b) .
edge(b, c) .
edge(c, a) .
edge(c, d) .
edge(e, f) .

%%% Reachability, directed.
reaches(?x, ?y) :- edge(?x, ?y) .
reaches(?x, ?z) :- reaches(?x, ?y), edge(?y, ?z) .

%%% A cycle is a node that reaches itself.
inCycle(?x) :- reaches(?x, ?x) .

%%% Undirected connectivity: make the edge symmetric first, then close it.
%%% Doing this in one recursive rule instead is a common way to write a
%%% program that is correct and much slower.
link(?x, ?y) :- edge(?x, ?y) .
link(?y, ?x) :- edge(?x, ?y) .

connected(?x, ?y) :- link(?x, ?y) .
connected(?x, ?z) :- connected(?x, ?y), link(?y, ?z) .

node(?x) :- edge(?x, _) .
node(?y) :- edge(_, ?y) .

%%% Every node is connected to itself, which the closure above does not say
%%% for isolated nodes.
connected(?x, ?x) :- node(?x) .

%%% A component is named by its alphabetically smallest member, which gives
%%% every member of a component the same label. #min orders strings too.
component(?x, #min(?y)) :- connected(?x, ?y) .

%%% Path length. Recursion is safe, but this counts every path rather than
%%% the shortest one, so take the minimum afterwards.
hops(?x, ?y, 1) :- edge(?x, ?y) .
hops(?x, ?z, ?n) :- hops(?x, ?y, ?m), edge(?y, ?z), ?n = ?m + 1, ?m < 10 .

distance(?x, ?y, #min(?n)) :- hops(?x, ?y, ?n) .

@export component :- csv{resource = "components.csv"} .
@export distance :- csv{resource = "distance.csv"} .

SQL

-- Shortest distance from one node, in SQL. Compare with the four Datalog
-- rules that say the same thing.
WITH RECURSIVE hops(node, dist) AS (
    SELECT b, 1 FROM edge WHERE a = 'a'
    UNION
    SELECT e.b, h.dist + 1
    FROM hops h
    JOIN edge e ON e.a = h.node
    WHERE h.dist < 100          -- a hand written bound, or this never ends
)
SELECT node, MIN(dist) AS dist
FROM hops
GROUP BY node;

-- The UNION deduplicates whole rows, so a node reached at two different
-- distances stays twice and the MIN at the end is doing the real work. The
-- engine has explored every path, not every node, which is why this gets
-- slow long before the graph gets large.

Python 3.12

"""What a Datalog engine does, written out by hand.

Naive evaluation: apply every rule to everything known, add whatever is new,
and repeat until a round adds nothing. That last condition is the fixpoint,
and it is why recursion in Datalog terminates without anyone bounding it.
"""


def transitive_closure(edges: set[tuple[str, str]]) -> set[tuple[str, str]]:
    # Round zero: the base rule, path(X, Y) :- edge(X, Y).
    paths = set(edges)

    while True:
        # The recursive rule, path(X, Z) :- edge(X, Y), path(Y, Z).
        derived = {
            (x, z)
            for (x, y) in edges
            for (y2, z) in paths
            if y == y2
        }

        new = derived - paths
        if not new:
            # Nothing changed, so nothing ever will. Stop.
            return paths
        paths |= new


def main() -> None:
    edges = {("a", "b"), ("b", "c"), ("c", "d")}
    for pair in sorted(transitive_closure(edges)):
        print(pair)

    # Everything an engine adds to this is performance and honesty:
    # semi-naive evaluation joins only against the facts the last round
    # produced, indexes pick the join order, and stratification decides when
    # negation is allowed to look at a predicate. None of it changes the
    # answer, which is what makes the answer worth trusting.


if __name__ == "__main__":
    main()

Why it stops

The set of possible facts is finite

Every derived fact is built from constants already present in the program. There are finitely many of those, so there are finitely many facts that could ever be derived. On the six node graph above, the ceiling for reaches is every ordered pair, thirty six facts; thirteen turn out to actually hold. The ceiling is what guarantees the counting stops, not what does the stopping.
Each round either grows the set or ends it

Facts are only ever added, never removed, and each round adds a subset of a finite set. The sequence has to stop.
The stopping point is unique

The result does not depend on the order rules were applied in, so there is exactly one answer. This is the property that lets an engine reorder and parallelise freely.
Arithmetic is the exception

?n = ?m + 1 can invent a value that was not there before, and a rule that does so with no upper bound will climb forever. That is why the hops rule above carries ?m < 10. Any rule that computes a new number needs a reason it cannot run away.

nmo --trace

$ nmo graphs.rls -e none --trace 'reaches(a, d)'
Reasoning completed in 0ms. Derived 117 facts.
   Data import:     0ms
   Reasoning:       0ms
   Data export:     0ms

 reaches(a, d) :- reaches(a, c), edge(c, d) .
 ├─ reaches(a, c) :- reaches(a, b), edge(b, c) .
 │  ├─ reaches(a, b) :- edge(a, b) .
 │  │  └─ edge(a, b)
 │  └─ edge(b, c)
 └─ edge(c, d)

A trace is the proof tree for one fact: what derived it, and what derived those. When a recursive rule produces something you did not expect, this answers the question directly rather than by experiment.

Patterns worth knowing

Try it yourself

Add an edge that creates a cycle, and check that reaches still terminates. Then add a second edge relation and write mutual recursion: a path may alternate between the two, starting with either.

Hint: Two predicates that each mention the other in their bodies. No engine here needs anything special for that, and SQL has no translation for it at all.

Show one solution

graphs.rls

%! Graph recipes: reachability, cycles, components and distance.
%! Verify: inCycle = a | b | c
%! Verify: component = a a | b a | c a | d a | e e | f e

edge(a, b) .
edge(b, c) .
edge(c, a) .
edge(c, d) .
edge(e, f) .

%%% Reachability, directed.
reaches(?x, ?y) :- edge(?x, ?y) .
reaches(?x, ?z) :- reaches(?x, ?y), edge(?y, ?z) .

%%% A cycle is a node that reaches itself.
inCycle(?x) :- reaches(?x, ?x) .

%%% Undirected connectivity: make the edge symmetric first, then close it.
%%% Doing this in one recursive rule instead is a common way to write a
%%% program that is correct and much slower.
link(?x, ?y) :- edge(?x, ?y) .
link(?y, ?x) :- edge(?x, ?y) .

connected(?x, ?y) :- link(?x, ?y) .
connected(?x, ?z) :- connected(?x, ?y), link(?y, ?z) .

node(?x) :- edge(?x, _) .
node(?y) :- edge(_, ?y) .

%%% Every node is connected to itself, which the closure above does not say
%%% for isolated nodes.
connected(?x, ?x) :- node(?x) .

%%% A component is named by its alphabetically smallest member, which gives
%%% every member of a component the same label. #min orders strings too.
component(?x, #min(?y)) :- connected(?x, ?y) .

%%% Path length. Recursion is safe, but this counts every path rather than
%%% the shortest one, so take the minimum afterwards.
hops(?x, ?y, 1) :- edge(?x, ?y) .
hops(?x, ?z, ?n) :- hops(?x, ?y, ?m), edge(?y, ?z), ?n = ?m + 1, ?m < 10 .

distance(?x, ?y, #min(?n)) :- hops(?x, ?y, ?n) .

@export component :- csv{resource = "components.csv"} .
@export distance :- csv{resource = "distance.csv"} .

unarmed(?n) :- character(?n, _, _), ~weapon(?n, _, _) .

Negation, and why it has rules

Absence is expressible, with two conditions attached: the variable must be bound first, and no recursion may pass through the negation.

Datalog's negation means "not derivable", which is not the same as "false". The engine computes everything a predicate can be, and then a negated atom asks whether a particular fact is among them. That is the closed world assumption, and it is exactly the assumption a database makes when you write NOT EXISTS.

negation.rls

%! Negation, stratification, and the shapes that need it.
%! Verify: enrolledInEverything = ana
%! Verify: notEnrolled = ben databases | cleo databases | cleo logic

student("ana") .
student("ben") .
student("cleo") .

course("logic") .
course("databases") .

enrolled("ana", "logic") .
enrolled("ana", "databases") .
enrolled("ben", "logic") .

%%% NOT EXISTS. ?s is bound by a positive atom first, so the negation only
%%% has to answer a yes or no question about a value we already have.
notEnrolled(?s, ?c) :- student(?s), course(?c), ~enrolled(?s, ?c) .

%%% A variable that appears only under the negation is quantified inside it:
%%% this says "there is no course at all that this student is enrolled in".
enrolledInNothing(?s) :- student(?s), ~enrolled(?s, _) .

%%% Set difference, which is the same shape again.
%%% enrolledInEverything is the students with no course they are missing.
missingSome(?s) :- notEnrolled(?s, _) .
enrolledInEverything(?s) :- student(?s), ~missingSome(?s) .

@export notEnrolled :- csv{resource="not-enrolled.csv"} .
@export enrolledInEverything :- csv{resource="all-courses.csv"} .

negation.lp

% Negation as failure, and the safety rule that goes with it.
% Run:    clingo negation.lp
% Expect: SATISFIABLE with lonely(c), lonely(d), unreached(a), unreached(d)
%         and stranded(d). c is lonely because nothing leaves it, and d is
%         both lonely and unreached because nothing leaves or enters it.

node(a; b; c; d).
edge(a, b). edge(b, c).

% #defined declares a predicate that a facts file may legitimately leave
% empty. Without it every rule mentioning the predicate produces a warning,
% and warning spam trains people to ignore warnings.
#defined banned/1.

% not means "not derivable", which is not the same as "false". X has to be
% bound by a positive literal first: `lonely(X) :- not edge(X, _).` is
% rejected as unsafe, because clingo has no idea what X ranges over.
lonely(X) :- node(X), not edge(X, _).

% The same shape for "nothing points at it".
unreached(X) :- node(X), not edge(_, X).

% Negation over a derived predicate is fine as long as no cycle passes
% through it. This one does not: reachable is finished before allowed looks
% at it.
reachable(Y) :- edge(a, Y).
reachable(Y) :- reachable(X), edge(X, Y).
stranded(X) :- node(X), X != a, not reachable(X).

#show lonely/1.
#show unreached/1.
#show stranded/1.

The two conditions

Safety: bind the variable positively first

lonely(?x) :- ~edge(?x, _) is rejected in every dialect. There is no way to enumerate the things that are not edges, because the universe of possible values is not a thing the engine has. Put a positive atom in front that says what ?x ranges over.
Stratification: no recursion through negation

p(?x) :- q(?x), ~p(?x) asks for a fact that holds exactly when it does not. Engines refuse this by sorting rules into strata: a negated predicate is computed completely before anything that negates it runs. A cycle through a negation cannot be stratified and is a compile error.

An unsafe rule

$ clingo unsafe.lp
clingo version 5.6.2
Reading from unsafe.lp
unsafe.lp:3:1-29: error: unsafe variables in:
  lonely(X):-[#inc_base];not #p_edge(#b(X),#p).
unsafe.lp:3:8-9: note: 'X' is unsafe

*** ERROR: (clingo): grounding stopped because of errors

What negation is for

Question	Shape
Rows with no match	p(?x), ~q(?x)
Rows with no match at all	p(?x), ~q(?x, _)
Set difference	a(?x), ~b(?x)
The maximal ones	derive notMaximal, then p(?x), ~notMaximal(?x)
Everything is covered	derive missing, then ~missing(?x)

The last two are the pattern worth internalising. Datalog cannot directly say "there is no greater one", so you say the opposite positively, let the engine compute it, and negate that. Every "maximum", "latest", "only" and "all" query is that shape, and once you see it the rest of the language opens up.

revenue(?r, #sum(?amount, ?id)) :- sale(?id, ?r, ?amount) .

Aggregates, and the distinctness trap

Counting and summing work in both engines, and both aggregate over distinct tuples rather than over rows. That default is the opposite of SQL's and it catches everybody once.

aggregates.rls

%! Aggregates, and the distinctness rule that surprises everyone once.
%! Verify: revenue = north 350 | south 600
%! Verify: bestRegion = south

%%% sale(id, region, amount)
sale(1, "north", 100) .
sale(2, "north", 250) .
sale(3, "south", 100) .
sale(4, "south", 400) .
sale(5, "south", 100) .

%%% Grouping is implicit: every head variable that is not aggregated is a
%%% group key. This groups by region.
%%%
%%% ?amount alone would sum the DISTINCT amounts, so the south's two
%%% hundreds would count once. Adding ?id makes the tuples distinct, and
%%% only the first argument is actually summed.
revenue(?region, #sum(?amount, ?id)) :- sale(?id, ?region, ?amount) .

%%% Counting rows means counting a key. Counting ?amount would count
%%% distinct amounts, which is a different and usually wrong question.
orderCount(?region, #count(?id)) :- sale(?id, ?region, _) .

%%% One aggregate per rule, so an average takes three.
totalAmount(#sum(?amount, ?id)) :- sale(?id, _, ?amount) .
totalOrders(#count(?id)) :- sale(?id, _, _) .
averageOrder(DOUBLE(?total) / ?count) :- totalAmount(?total), totalOrders(?count) .

%%% Argmax: take the maximum, then join back to find who holds it.
bestRevenue(#max(?amount)) :- revenue(_, ?amount) .
bestRegion(?region) :- bestRevenue(?best), revenue(?region, ?best) .

@export revenue :- csv{resource="revenue.csv"} .
@export bestRegion :- csv{resource="best.csv"} .

aggregates.lp

% Aggregates, and the tuple rule that catches everyone once.
% Run:    clingo aggregates.lp
% Expect: SATISFIABLE with headcount(3), payroll(190), distinct_pay(120),
%         by_dept(eng,140) and by_dept(ops,50). 120 is 70 + 50: the two
%         engineers on 70 are one tuple, and that is the whole trap.

employee(ada, eng, 70).
employee(grace, eng, 70).
employee(alan, ops, 50).

% #count over a distinguishing term counts rows.
headcount(N) :- N = #count { E : employee(E, _, _) }.

% Aggregate elements are deduplicated as TUPLES. `#sum { S : ... }` adds up
% the distinct salaries, so two people on 70 contribute 70 once. Including
% the employee makes each tuple distinct, and the first term is the one
% summed.
payroll(S) :- S = #sum { Pay, E : employee(E, _, Pay) }.
% checker: expected
distinct_pay(S) :- S = #sum { Pay : employee(_, _, Pay) }.

% Grouping is a rule with a group key in the head.
by_dept(D, S) :- employee(_, D, _), S = #sum { Pay, E : employee(E, D, Pay) }.

% Aggregates work in constraints too, which is how you write "at most".
:- #count { E : employee(E, eng, _) } > 5.

#show headcount/1.
#show payroll/1.
#show distinct_pay/1.
#show by_dept/2.

SQL

-- Grouping, and the difference between summing rows and summing values.
SELECT region, SUM(amount) AS revenue, COUNT(*) AS orders
FROM sale
GROUP BY region;

-- SQL sums rows by default. Summing distinct values needs saying so, which
-- is the exact opposite of Datalog's default and worth holding on to.
SELECT region, SUM(DISTINCT amount) AS distinct_revenue
FROM sale
GROUP BY region;

-- Argmax: the region with the most revenue. A window function, a subquery
-- or a LIMIT, and all three behave differently on ties.
SELECT region, revenue
FROM (
    SELECT region, SUM(amount) AS revenue,
           RANK() OVER (ORDER BY SUM(amount) DESC) AS position
    FROM sale
    GROUP BY region
) ranked
WHERE position = 1;

The trap, stated plainly

SUM(amount) in SQL adds up one value per row. An aggregate here ranges over the distinct tuples of its arguments, so #sum(?amount) adds up the distinct amounts. Two sales of 100 contribute 100 once, and nothing warns you.

The fix is to include something that makes each tuple distinct, usually the key of the row. Only the first argument is summed; the rest are there purely so the tuples differ.

Written	Means
#sum(?amount)	the sum of the distinct amounts
#sum(?amount, ?id)	the sum over distinct (amount, id) pairs, which is per row
#count(?age)	how many distinct ages
#count(?id)	how many rows, if ?id is unique per row
#sum { Pay : e(_, Pay) }	clingo's version of the same trap
#sum { Pay, E : e(E, Pay) }	clingo's version of the fix

The rules around them

Grouping is implicit. Every head variable that is not inside the aggregate is a group key. There is no GROUP BY clause, and no way to accidentally group by the wrong thing.

One aggregate per rule in Nemo, which is why an average takes three rules: one for the total, one for the count, and one for the division. Remember to convert to a double first, or integer division will quietly give you the wrong answer.

Aggregates stratify like negation. No recursive cycle may pass through one, because the aggregate needs its input to be finished before it can be computed. That is what stops "the count of things whose count is the count" from being a question.

Try it yourself

Compute the average sale per region, correctly, including the conversion that stops integer division from truncating. Then work out what your program says about a region that exists but has no sales.

Hint: Three rules: a sum, a count, and a division. For the empty region, add a rule that supplies zero for any region with no sale, using negation.

Show one solution

aggregates.rls

%! Aggregates, and the distinctness rule that surprises everyone once.
%! Verify: revenue = north 350 | south 600
%! Verify: bestRegion = south

%%% sale(id, region, amount)
sale(1, "north", 100) .
sale(2, "north", 250) .
sale(3, "south", 100) .
sale(4, "south", 400) .
sale(5, "south", 100) .

%%% Grouping is implicit: every head variable that is not aggregated is a
%%% group key. This groups by region.
%%%
%%% ?amount alone would sum the DISTINCT amounts, so the south's two
%%% hundreds would count once. Adding ?id makes the tuples distinct, and
%%% only the first argument is actually summed.
revenue(?region, #sum(?amount, ?id)) :- sale(?id, ?region, ?amount) .

%%% Counting rows means counting a key. Counting ?amount would count
%%% distinct amounts, which is a different and usually wrong question.
orderCount(?region, #count(?id)) :- sale(?id, ?region, _) .

%%% One aggregate per rule, so an average takes three.
totalAmount(#sum(?amount, ?id)) :- sale(?id, _, ?amount) .
totalOrders(#count(?id)) :- sale(?id, _, _) .
averageOrder(DOUBLE(?total) / ?count) :- totalAmount(?total), totalOrders(?count) .

%%% Argmax: take the maximum, then join back to find who holds it.
bestRevenue(#max(?amount)) :- revenue(_, ?amount) .
bestRegion(?region) :- bestRevenue(?best), revenue(?region, ?best) .

@export revenue :- csv{resource="revenue.csv"} .
@export bestRegion :- csv{resource="best.csv"} .

byIri(alice, 30) vs byString("alice", 30)

Terms, types and the empty result

Nothing about a value is coerced for you. The single most common reason a program runs and derives nothing is two values that look the same and are not.

types.rls

%! Datatypes, and the strictness that causes most empty results.
%! Verify: matched = alice
%! Verify: parsed = 17

@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix wd: <http://www.wikidata.org/entity/> .

%%% A bare name is a relative IRI. A quoted name is a string. They are two
%%% different values, and they never join with each other.
byIri(alice, 30) .
byString("alice", 30) .

%%% This finds nothing, because <alice> is not "alice". Bridge the gap with
%%% STR, which turns anything into its plain string form.
matched(?name) :- byIri(?name, _), byString(STR(?name), _) .

%%% Numbers are strict across families and normalised within one.
%%% 42 and 42.0 are different values; 42 and "42"^^xsd:byte are the same.
count(42) .
ratio(42.0) .
tagged("42"^^xsd:byte) .

sameAsCount(?v) :- tagged(?v), count(?v) .

%%% Language tags are part of the value.
label("Dresden"@de) .
label("Dresden"@en) .
germanLabel(?l) :- label(?l), LANG(?l) = "de" .

%%% Conversions are how you cross a type boundary on purpose. A conversion
%%% that cannot succeed derives nothing at all rather than raising, so INT
%%% doubles as a filter for rows that are not really numbers.
raw("17") .
raw("not a number") .
parsed(INT(?text)) :- raw(?text) .

%%% Full IRIs, prefixed names and f-strings for building new ones.
entity(wd:Q42) .
entityText(?s) :- entity(?e), ?s = f"entity {STR(?e)}" .

@export parsed :- csv{resource="parsed.csv"} .

What a term can be

Term	Nemo	clingo	Souffle
Constant	alice, an IRI	alice	declared as a type
String	"alice"	"alice"	symbol
Integer	42	42	number
Decimal	3.14	not supported	float
Language tagged	"Dresden"@de	no	no
Typed literal	"42"^^xsd:byte	no	no
Full IRI	<http://example.org/a>	no	no
Structure	no	n(1), edge(a, b)	records and ADTs
Null	_:b1, from existentials	no	nil in records

The rules of equality

Across families, never equal. In Nemo, the bare name alice is the IRI <alice> and is not the string "alice". 42 is not 42.0. "Dresden"@de is not "Dresden"@en and neither is "Dresden". In clingo, a and "a" are different terms in exactly the same way.

Within a family, normalised. All the XSD integer types denote the same values, so "42"^^xsd:byte really does equal 42, and the engine prints the normalised form rather than what you typed.

Comparisons convert, equality does not. ?x < 42.0 promotes to a double and works across numeric types. ?x = 42.0 does not.

every variable needs a positive binder

Safety, stratification and arity

Three restrictions that every dialect enforces, what each is protecting you from, and what the error messages look like.

Datalog buys its guarantees by refusing some programs. Three refusals account for nearly all of them, and each has a clear reason behind it.

Safety

Every variable in the head, in a negated atom, or in a comparison must also appear in a positive body atom that can bind it.

bad(?x) :- ~good(?x) . asks for everything that is not good. There is no universe to enumerate, so there is no answer to give. Adding thing(?x) in front says what to range over and makes the question finite.

clingo on an unsafe rule

$ clingo unsafe.lp
clingo version 5.6.2
Reading from unsafe.lp
unsafe.lp:3:1-29: error: unsafe variables in:
  lonely(X):-[#inc_base];not #p_edge(#b(X),#p).
unsafe.lp:3:8-9: note: 'X' is unsafe

*** ERROR: (clingo): grounding stopped because of errors

The anonymous variable version is the one that gets through review

admin_or_owner(V, _) :- admin(V). looks like a harmless shrug: an admin qualifies, whatever the second argument is. But every _ is a fresh variable, so this is an unbound variable in a head, and clingo rejects it for exactly the reason above. The trap has two teeth. First, the underscore reads as "anything", which is head language, when it means "a new variable nobody binds", which is body language. Second, the error message names #Anon0, a variable that appears nowhere in your source, so it reads like a bug in the grounder until you know what it is. The fix is to name the variable and give it a domain: admin_or_owner(V, T) :- admin(V), thread(T).

This one is not hypothetical. It is the single bug that shipped in this book's own repository, in a file its structural checker passed, and it was caught only when the program was finally handed to the engine. The checker learned the rule the same day.

Stratification

No recursive cycle may pass through a negation or an aggregate. The engine sorts predicates into strata and computes each one completely before anything that negates or aggregates it.

The reason is that a cycle through negation has no single answer. p :- ~p holds if it does not, which is not a fact about the world so much as a badly posed question. Nemo rejects it. clingo allows it, and answers a different question: it looks for stable models, and a program like that simply has none, or has several.

Written	Nemo	clingo
p(?x) :- q(?x), ~p(?x)	rejected, not stratifiable	no stable model
p :- ~q. q :- ~p.	rejected	two models, one with p and one with q
p(?x) :- q(?x), ~r(?x)	fine, r is a lower stratum	fine
total(#sum(?x)) :- total(?x)	rejected, aggregate in a cycle	accepted, and solved under the stable model semantics

Arity

A predicate has one arity for the whole program. Using person with two arguments in one rule and three in another is a hard error in Nemo, and in clingo it silently creates two unrelated predicates that share a name, which is worse.

nmo on drifted arity

$ nmo broken.rls -e none
[219] Error: predicate `person` used with arity 3.
   ╭─[ broken.rls:9:1 ]
   │
 9 │ person(?name, ?age, ?city) :- record(?name, ?age, ?city) .
   │ ────────────────────────────┬───────────────────────────
   │                             ╰───────────────────────────── predicate `person` used with arity 3.
   │
   ├─[ broken.rls:9:1 ]
   │
 3 │ person(alice) .
   │ ──────┬──────
   │       ╰──────── predicate was used here with arity 1
   │
   │ Note: each predicate is only allowed to have one arity
───╯

Write the schema down

A comment above each predicate giving its columns, in order. It costs one line and prevents the whole class of bug where an argument slipped a position.
Give imports an explicit format

In Nemo, format=(string, int) fixes the arity, documents the types and drops rows that do not parse. Without it, an import whose predicate appears nowhere else cannot have its arity inferred at all.
Declare the fact interface

In clingo, #defined banned/1. says that a facts file may legitimately leave this predicate empty. It removes the warning spam, and it doubles as a machine-checked statement of what the program expects to be given.
Prefer more predicates to wider ones

A relation with nine columns is one where arguments get transposed. Two relations joined on a key are harder to get wrong and usually faster, since the engine can index each one for what it is used for.

@parameter $minAge = 18 .

The shape of a Nemo program

A tour of the .rls file: directives, prefixes, parameters, comments and the order to put them in.

Nemo is a bottom-up Datalog engine written in Rust, from the Knowledge-Based Systems group at TU Dresden. It is built for materialising large derivations over data from many sources at once, and it is unusually good at the parts other engines leave out: reading RDF and CSV and SPARQL results directly, existential rules, and typed values.

family.rls

%! Ancestors, and the ones two people share.
%! Verify: nearestShared = alice
%! Verify: sharedAncestor = alice

father(bob, alice) .
father(daniel, cho) .
mother(cho, alice) .
mother(eiko, cho) .
mother(eiko, finley) .

%%% Two rules with the same head are an OR: a parent is a father or a mother.
parent(?child, ?p) :- father(?child, ?p) .
parent(?child, ?p) :- mother(?child, ?p) .

%%% The base case and the recursive case, which is all transitive closure is.
ancestor(?child, ?a) :- parent(?child, ?a) .
ancestor(?child, ?a) :- ancestor(?child, ?middle), parent(?middle, ?a) .

%%% Reusing ?a in both atoms is the join: an ancestor of one and of the other.
sharedAncestor(?a) :- ancestor(bob, ?a), ancestor(eiko, ?a) .

%%% The nearest shared ancestor: one with no descendant who also qualifies.
%%% Derive the ones that are not nearest, then negate. Negation needs a
%%% fully computed predicate underneath it, which this gives it.
notNearest(?a) :- sharedAncestor(?a), sharedAncestor(?below), ancestor(?below, ?a) .
nearestShared(?a) :- sharedAncestor(?a), ~notNearest(?a) .

@export nearestShared :- csv{resource="nearest.csv"} .

The parts of a file, in order

%! the file comment

At the very top, first line as a title. %%% documents the statement directly below it and travels with it. % is an ordinary comment. Using the three deliberately makes a rule file readable a year later.
@prefix and @base

Abbreviations for IRIs, exactly as in Turtle. @base sets what relative names expand against. Quoted strings never expand, which is the difference to hold on to.
@parameter

@parameter $minAge = 18 . with an optional default, overridden by --param "minAge=21". Parameters work anywhere a constant does, including inside import paths and f-strings, which turns one program into a family of them.
@import, then facts, then rules

Rules grouped into strata, each with a comment saying what the stratum is for. Then @export at the bottom. That order is conventional rather than required, and following it makes files skimmable.

Syntax	Means
?x	a variable
!x	an existential variable, in a head only
_	anonymous, matching anything and binding nothing
$x	a parameter
~p(?x)	negation
:-	if
,	and
alice	a relative IRI
"alice"	a string
wd:Q42	a prefixed IRI
<http://example.org/a>	a full IRI
"Dresden"@de	a language tagged string
f"{?a} and {?b}"	an f-string
#[name("Rule")]	an attribute, for nicer traces

@import p :- csv{resource="f.csv", format=(string, int)} .

Reading and writing data

CSV, RDF, JSON and SPARQL results, all as predicates. This is where Nemo earns its place over a general purpose Datalog.

io.rls

%! Reading and writing files.
%!
%! Run: nmo io.rls -D out -o

@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .

%%% A parameter can be overridden from the command line with
%%% --param "minSalary=50000", which is how one program serves many runs.
@parameter $minSalary = 40000 .

%%% format fixes the arity, documents the column types, and quietly drops
%%% rows that do not parse. skip ignores a column entirely.
@import rawEmployee :- csv{
    resource = "employees.csv",
    format = (string, string, int, skip)
} .

%%% Copy the import into a predicate of our own before doing anything with
%%% it. Nemo pushes filters down into the reader as an optimisation, and in
%%% 0.10 that can let rows through that a filter should have dropped. One
%%% projection rule makes the data real first, and it is good practice
%%% regardless: the schema is now written down in one place.
employee(?name, ?email, ?salary) :- rawEmployee(?name, ?email, ?salary) .

wellPaid(?name, ?salary) :- employee(?name, _, ?salary), ?salary >= $minSalary .

validEmail(?name) :- employee(?name, ?email, _), CONTAINS(?email, "@") .
invalidEmail(?name) :- employee(?name, ?email, _), NOT(CONTAINS(?email, "@")) .

%%% RDF goes in the same way. The format is inferred from the extension,
%%% and gzipped files are read directly.
@import triple :- rdf{resource = "facts.nt.gz"} .

subject(?s) :- triple(?s, _, _) .

%%% Exports are what write files. @output is for the browser playground and
%%% produces nothing at all on the command line.
@export wellPaid :- csv{resource = "well-paid.csv"} .
@export invalidEmail :- csv{resource = "invalid-email.csv"} .

%%% An export with no resource writes to standard output.
@export subject :- csv{resource = ""} .

The formats

Directive	Reads or writes
csv{resource="f.csv"}	comma separated, with dsv and tsv alongside
rdf{resource="f.nt"}	N-Triples, Turtle, RDF/XML, and .gz of any of them
rdf{resource="f.nq"}	quads, giving a four column predicate
json{resource="f.json"}	JSON, flattened into triples
sparql{endpoint=..., query=...}	results from a live endpoint, such as Wikidata
resource="https://..."	any of the above over HTTP
resource=""	standard input on import, standard output on export

format is not optional in practice

format=(string, int, skip) does three jobs at once. It fixes the arity, which the engine otherwise cannot infer for a predicate that appears nowhere else. It documents the columns for whoever reads the file next. And it drops rows that do not parse, which turns a dirty CSV into a clean relation and a count of what was rejected.

skip ignores a column entirely, which is the cheapest possible way to read a wide export you only need three columns from.

Develop against a slice

limit=100 on an import while the rules are still moving. A rule set that is wrong is wrong on a hundred rows too, and the loop is seconds rather than minutes.
Export the intermediate steps

Or run with -e idb. Seeing what each stratum produced answers most questions faster than reasoning about why the last one is empty.
Parameterise the paths

@parameter $day = "2026-07-01" . and then resource = f"events-{$day}.csv". The same program now runs over any day without editing.

f"{UCASE(SUBSTR(?s, 1, 1))}{SUBSTR(?s, 2)}"

Built-in functions

Strings, numbers, conversions and f-strings, with one syntactic restriction that produces a famously unhelpful error message.

builtins.rls

%! Built-in functions: strings, numbers, conversions and f-strings.
%! Verify: early = ada lovelace | ada lovelance
%! Verify: unreachable = grace hopper

person("ada lovelace", "ada@example.org", "1815") .
person("ada lovelance", "ada.l@example.org", "1815") .
person("grace hopper", "grace(at)example.org", "1906") .
person("alan turing", "alan@example.org", "not a year") .

%%% Boolean built-ins work directly as body conditions. Older tutorials
%%% define a TRUE fact and wrap filters in it; that has not been needed
%%% since 0.10 and is only noise in new programs.
contactable(?name) :- person(?name, ?email, _), CONTAINS(?email, "@") .
unreachable(?name) :- person(?name, ?email, _), NOT(CONTAINS(?email, "@")) .
domainOk(?name) :- person(?name, ?email, _), REGEX(?email, "^[a-z]+@[a-z.]+$") .

%%% A conversion that cannot succeed derives nothing rather than failing, so
%%% INT is a filter for rows that only look numeric.
born(?name, INT(?year)) :- person(?name, _, ?year) .

%%% String work. SUBSTR is one based, and STRBEFORE returns nothing when
%%% the delimiter is absent, so append it first if the match must succeed.
family(?name, STRAFTER(?name, " ")) :- person(?name, _, _) .
given(?name, STRBEFORE(?name, " ")) :- person(?name, _, _) .

%%% An f-string interpolates any expression and converts it with STR.
%%% Capitalising a word takes one, and no separate function.
display(?name, ?shown) :-
    given(?name, ?first),
    ?shown = f"{UCASE(SUBSTR(?first, 1, 1))}{SUBSTR(?first, 2)}" .

%%% Arithmetic at the top level of a body is written infix. Inside a nested
%%% call it is not: OR(?a > 1, ?b > 1) is a parse error, and the prefix
%%% names are what parse.
%%% Infix table: = EQUALITY, != UNEQUALITY, > NUMGREATER, >= NUMGREATEREQ,
%%% < NUMLESS, <= NUMLESSEQ, + SUM, - SUBTRACTION, * PRODUCT, / DIVISION.
century(?name, ?c) :- born(?name, ?year), ?c = 1 + ?year / 100 .
early(?name) :- born(?name, ?year), OR(NUMLESS(?year, 1850), EQUALITY(?year, 1900)) .

%%% Fuzzy matching, for entity resolution against dirty data. The
%%% misspelled duplicate above is one edit away; unrelated names are many.
similar(?a, ?b) :-
    person(?a, _, _),
    person(?b, _, _),
    ?a != ?b,
    LEVENSHTEIN(?a, ?b) <= 2 .

@export display :- csv{resource = "display.csv"} .
@export early :- csv{resource = "early.csv"} .

The infix restriction

Infix operators are not allowed inside a nested function call. The parse error says expected `.`, which points nowhere near the problem and has cost a great many people an afternoon.

OR(?x > 2, ?y = 0) does not parse. OR(NUMGREATER(?x, 2), EQUALITY(?y, 0)) does. At the top level of a body, infix is fine.

Infix	Prefix name	Infix	Prefix name
=	EQUALITY	+	SUM
!=	UNEQUALITY	-	SUBTRACTION
>	NUMGREATER	*	PRODUCT
>=	NUMGREATEREQ	/	DIVISION
<	NUMLESS
<=	NUMLESSEQ

The functions worth knowing

Group	Functions
Strings	STRLEN, UCASE, LCASE, CONCAT, SUBSTR, STRAFTER, STRBEFORE, STRREV, COMPARE
Tests	STRSTARTS, STRENDS, CONTAINS, REGEX
Fuzzy	LEVENSHTEIN, for entity resolution against dirty data
Language	LANG, STRLANG, for joining plain strings against RDF labels
Numbers	ABS, SQRT, ROUND, CEIL, FLOOR, LOG, POW, REM, MIN, MAX
Conversions	INT, DOUBLE, FLOAT, IRI, STR, FULLSTR
Type tests	isInteger, isNumeric, isString, isIri, isNull
Logic	AND, OR, NOT, all prefix
General	DATATYPE, URIENCODE, URIDECODE

person(?x, ?given, !family) :- givenName(?x, ?given) .

Existential rules and the chase

How to say that something must exist without knowing what it is, and when to build a deterministic identifier instead.

Plain Datalog cannot invent values, which is what makes it terminate. An existential rule lifts that restriction in a controlled way: a !variable in the head asks the engine to invent a fresh value when it needs one.

Nemo uses the Datalog-first restricted chase, which means the rule only fires when no matching fact already exists. Invented values fill gaps rather than duplicating what is already there, and that is the difference between a useful feature and one that never terminates.

existential.rls

%! Inventing values: existential rules, and deterministic identifiers.

@prefix foaf: <http://xmlns.com/foaf/0.1/> .

givenName(p1, "Ada") .
givenName(p2, "Grace") .
familyName(p1, "Lovelace") .

%%% The complete case: both names are known.
person(?x, ?given, ?family) :- givenName(?x, ?given), familyName(?x, ?family) .

%%% The fallback. `!family` asks Nemo to invent a value, and under the
%%% restricted chase it only fires when no matching person row exists yet,
%%% so p1 is left alone and p2 gets a placeholder rather than a duplicate.
person(?x, ?given, !family) :- givenName(?x, ?given) .

%%% Invented values print as _:123, are not stable between runs, and have no
%%% datatype. That is fine for a gap filler and wrong for anything you need
%%% to join on later or show to a person.
placeholder(?x) :- person(?x, _, ?family), isNull(?family) .

%%% When identifiers must be stable and structurally equal, build them
%%% instead. Two calls with the same arguments produce the same string, so
%%% the same pair is never given two identities.
edge(a, b) .
edge(b, c) .
edgeId(?from, ?to, ?id) :- edge(?from, ?to), ?id = f"EDGE({STR(?from)},{STR(?to)})" .

%%% Minting one key per distinct tuple across two sources, where an
%%% invented value is exactly right: the name does not matter, only that
%%% each tuple gets one.
sourceA("acme", "london") .
sourceB("acme", "london") .
sourceB("globex", "berlin") .

company(?name, ?city, !key) :- sourceA(?name, ?city) .
company(?name, ?city, !key) :- sourceB(?name, ?city) .

@export edgeId :- csv{resource = "edge-ids.csv"} .

Two ways to mint an identifier

	!existential	f-string
Value	an invented null, printed as `_:123`	a string you constructed
Stable across runs	no	yes
Equal for equal structure	no	yes, which is the point
Has a datatype	no	yes
Fires when a fact exists	no, the chase suppresses it	always
Grows with recursion depth	no	yes, the strings get longer
Use for	fallbacks, keys whose name does not matter	hash consing, reification, anything joined on later

nmo program.rls --trace 'reaches(a, d)'

When the answer is empty

Datalog programs fail quietly. Here is the checklist, in the order that finds the problem fastest.

A Datalog program that is wrong usually still runs. There is no exception, no stack trace and no crash: a rule that cannot fire simply does not, and the result is a relation with nothing in it. That makes a checklist more useful than a debugger. It also makes a test more useful than either, and the testing chapter is about arranging never to run this checklist twice for the same bug; this one is about the first time.

The six things to check, in order

one

A type mismatch

The bare name alice is an IRI and never equals the string "alice". 42 is not 42.0. A CSV column imported as a string joined against a bare constant matches nothing. This is the first thing to check every time, because it is the answer more often than everything else combined.

two

An aggregate over the wrong thing

#sum(?x) adds distinct values, not rows. If a total is suspiciously low, this is why.

three

Arity

A predicate has one arity for the whole program. An import whose predicate appears nowhere else cannot have its arity inferred at all, and needs an explicit format.

four

A built-in that quietly failed

STRLEN(42), INT("abc"), STRBEFORE with no match: none of these raise, they just produce no result and the rule does not fire. One wrong type in a chain of calls empties the whole relation.

five

A filter applied straight to an import

Materialise the import through a projection rule first, then filter. Both because of a known 0.10 issue with filters being pushed into readers, and because it makes the schema explicit.

six

@output rather than @export

The program ran, derived everything correctly, and wrote no files because @output is for the browser playground.

The two tools

Why was this derived

$ nmo graphs.rls -e none --trace 'reaches(a, d)'
Reasoning completed in 0ms. Derived 117 facts.
   Data import:     0ms
   Reasoning:       0ms
   Data export:     0ms

 reaches(a, d) :- reaches(a, c), edge(c, d) .
 ├─ reaches(a, c) :- reaches(a, b), edge(b, c) .
 │  ├─ reaches(a, b) :- edge(a, b) .
 │  │  └─ edge(a, b)
 │  └─ edge(b, c)
 └─ edge(c, d)

An error that is loud, for once

$ nmo broken.rls -e none
[219] Error: predicate `person` used with arity 3.
   ╭─[ broken.rls:9:1 ]
   │
 9 │ person(?name, ?age, ?city) :- record(?name, ?age, ?city) .
   │ ────────────────────────────┬───────────────────────────
   │                             ╰───────────────────────────── predicate `person` used with arity 3.
   │
   ├─[ broken.rls:9:1 ]
   │
 3 │ person(alice) .
   │ ──────┬──────
   │       ╰──────── predicate was used here with arity 1
   │
   │ Note: each predicate is only allowed to have one arity
───╯

For a fact you did not expect: trace it

--trace 'reaches(a, d)' prints the proof tree. When a rule fires more often than you meant, the tree shows exactly which join let it through.
For a fact you did expect: bisect

Run with -e idb and read down the strata. The first empty predicate is where the problem is, and everything downstream of it is a symptom rather than a cause.
Then shrink the input

Take three rows that should produce the fact and run against those alone. Most causes are visible immediately at that size, and the ones that are not were never about the data.
Then check the join by exporting it

Give the join its own predicate and export it. If it is empty, the problem is upstream of the rule you were looking at, and it is almost always a type mismatch.
For the fact that stubbornly stays missing: assert it

--trace answers why a fact is there, and nothing answers why one is not, so make it be there. Add the fact you expected as a temporary base fact and rerun. Whatever fires downstream of it was waiting on it, which tells you the rules above it are fine and the missing link is in its own derivation. Repeat one level down and you bisect the missing chain the way you bisected the strata. Then delete the assertion, because a debugging fact that survives into the program is a bug with a comment's credibility.

missing(?n) :- expected(?n), ~derived(?n) .

Testing a rule set

Rules are code, and code that nobody has watched fail is code nobody has tested. The harness is four rules and one line of shell, and pass is an empty relation.

A rule set is code. It has edge cases, it has regressions, and it goes wrong in the specific way this language goes wrong: quietly, deriving nothing, with no exception and no stack trace. The debugging chapter is about finding that after the fact. This chapter is about arranging never to look for it twice.

The good news is that Datalog needs no testing framework, because the thing a test does — compare what happened against what should have happened — is a join, and stating the difference is two rules.

rule-tests.rls

%! Testing rules with rules: the expect/actual diff, in both directions.
%!
%! Run: nmo rule-tests.rls -D out -o
%!      && ! test -s out/missing.csv && ! test -s out/unexpected.csv \
%!      && echo PASS || echo FAIL
%!
%! Verify: missing =
%! Verify: unexpected =

%%% ------------------------------------------------------------------
%%% THE FIXTURE. A hand written world small enough to check by eye, with
%%% the boundary values in it on purpose: ben is exactly 40, which is the
%%% only interesting number in the rule under test.
%%% ------------------------------------------------------------------
employee("ada",   "eng", 55) .
employee("ben",   "eng", 40) .
employee("cleo",  "ops", 31) .
employee("dara",  "ops", 39) .

%%% ------------------------------------------------------------------
%%% THE RULES UNDER TEST. In a real project these live in their own file
%%% and this one imports them; keeping them here makes the example
%%% runnable on its own.
%%% ------------------------------------------------------------------
senior(?name) :- employee(?name, _, ?age), ?age >= 40 .
junior(?name) :- employee(?name, _, ?age), ?age < 40 .

%%% ------------------------------------------------------------------
%%% THE EXPECTATION, written by hand from the fixture. This is the part
%%% that must never be generated from the rules: an expectation derived
%%% from the thing it tests agrees with it by construction.
%%% ------------------------------------------------------------------
expectSenior("ada") .
expectSenior("ben") .
expectJunior("cleo") .
expectJunior("dara") .

%%% ------------------------------------------------------------------
%%% THE DIFF, in both directions. Pass is two empty relations, which is
%%% the whole trick: the harness needs no assertion library, and the
%%% shell line at the top is the entire test runner.
%%%
%%% Only one direction would let a rule that derives too much pass.
%%% ------------------------------------------------------------------
missing("senior", ?n)    :- expectSenior(?n), ~senior(?n) .
missing("junior", ?n)    :- expectJunior(?n), ~junior(?n) .
unexpected("senior", ?n) :- senior(?n), ~expectSenior(?n) .
unexpected("junior", ?n) :- junior(?n), ~expectJunior(?n) .

@export missing :- csv{resource = "missing.csv"} .
@export unexpected :- csv{resource = "unexpected.csv"} .

% Watch it fail once, before you trust it green. Change >= 40 to > 40 and
% rerun: ben moves into missing.csv and the shell line prints FAIL. Put it
% back and it returns to green.
%
% Plain % comments here on purpose. A %%% comment documents the statement
% below it, so a trailing %%% block with no statement after it is a parse
% error rather than a comment.

Pass is two empty relations. That is the whole trick, and it is what makes the runner a line of shell rather than a dependency: a file with nothing in it is a green test, and test -s already knows how to ask.

Both directions, always

missing catches a rule that derives too little. unexpected catches one that derives too much. A harness with only the first passes happily on the day somebody widens a condition, which is the more common regression and the harder one to notice, because more output rarely looks like a failure.

It is the same argument as the contract chapter's leak and over-filter, and it comes back every time two descriptions of the same thing are compared: a difference has two directions and a checker that only looks one way is half a checker.

Test	Why it earns its place
Each stratum against a fixture you can check by eye	The first empty predicate is the cause; everything downstream is a symptom
The empty input	Half of these rule sets pass vacuously, and you want to know which half
A deliberate duplicate	A relation is a set. If a duplicate changes a count, an aggregate is counting values where you meant rows
The boundary value	`>=` against `>` is the most common one-character bug in any language
Bare name against quoted string	The failure this book keeps returning to, pinned by a test so it can only happen once

Running it like a test suite

One fixture per scenario, switched by a parameter

@parameter $fixture = "small" . and then resource = f"fixtures/{$fixture}/sales.csv". One --param on the command line runs the same rules against another world, which is exactly what a parameterised test is.
Keep the rules in their own file

Facts in one file, rules in another, expectations in a third. The rules under test are then the same bytes in the test run and the production run, which is the property the whole exercise depends on.
Exit code as the verdict

! test -s out/missing.csv && ! test -s out/unexpected.csv. No parsing, no framework, and it drops into CI beside everything else.
Never delete a regression fixture

When a bug is found, the world that exposed it becomes a permanent fixture. Supersede, never remove: the fixed rules must stay clean on that exact world forever, whether or not anyone would think to look for it again.

golden files

When the output is large

Export the relation, sort both sides, diff. Sorting matters: a relation has no order, so an unsorted diff reports a difference that is not one.

properties

When the answer is hard to write down

Assert a property instead of a value. Reachability is transitive; a component label is shared by everything it labels; a total equals the sum of its parts. Each is a rule whose output must be empty.

Try it yourself

Add a third rule to the file under test, and a bug to go with it: a rule that also fires for people it should not. Confirm your harness reports it in unexpected.csv rather than in missing.csv, and say why you knew which one it would be before you ran it.

Hint: Deriving too much is an unexpected. Deriving too little is a missing. A checker that only wrote one of those two rules would have gone green on this.

Show one solution

rule-tests.rls

%! Testing rules with rules: the expect/actual diff, in both directions.
%!
%! Run: nmo rule-tests.rls -D out -o
%!      && ! test -s out/missing.csv && ! test -s out/unexpected.csv \
%!      && echo PASS || echo FAIL
%!
%! Verify: missing =
%! Verify: unexpected =

%%% ------------------------------------------------------------------
%%% THE FIXTURE. A hand written world small enough to check by eye, with
%%% the boundary values in it on purpose: ben is exactly 40, which is the
%%% only interesting number in the rule under test.
%%% ------------------------------------------------------------------
employee("ada",   "eng", 55) .
employee("ben",   "eng", 40) .
employee("cleo",  "ops", 31) .
employee("dara",  "ops", 39) .

%%% ------------------------------------------------------------------
%%% THE RULES UNDER TEST. In a real project these live in their own file
%%% and this one imports them; keeping them here makes the example
%%% runnable on its own.
%%% ------------------------------------------------------------------
senior(?name) :- employee(?name, _, ?age), ?age >= 40 .
junior(?name) :- employee(?name, _, ?age), ?age < 40 .

%%% ------------------------------------------------------------------
%%% THE EXPECTATION, written by hand from the fixture. This is the part
%%% that must never be generated from the rules: an expectation derived
%%% from the thing it tests agrees with it by construction.
%%% ------------------------------------------------------------------
expectSenior("ada") .
expectSenior("ben") .
expectJunior("cleo") .
expectJunior("dara") .

%%% ------------------------------------------------------------------
%%% THE DIFF, in both directions. Pass is two empty relations, which is
%%% the whole trick: the harness needs no assertion library, and the
%%% shell line at the top is the entire test runner.
%%%
%%% Only one direction would let a rule that derives too much pass.
%%% ------------------------------------------------------------------
missing("senior", ?n)    :- expectSenior(?n), ~senior(?n) .
missing("junior", ?n)    :- expectJunior(?n), ~junior(?n) .
unexpected("senior", ?n) :- senior(?n), ~expectSenior(?n) .
unexpected("junior", ?n) :- junior(?n), ~expectJunior(?n) .

@export missing :- csv{resource = "missing.csv"} .
@export unexpected :- csv{resource = "unexpected.csv"} .

% Watch it fail once, before you trust it green. Change >= 40 to > 40 and
% rerun: ben moves into missing.csv and the shell line prints FAIL. Put it
% back and it returns to green.
%
% Plain % comments here on purpose. A %%% comment documents the statement
% below it, so a trailing %%% block with no statement after it is a parse
% error rather than a comment.

1 { assign(N, C) : colour(C) } 1 :- node(N).

clingo, and what answer set programming adds

Datalog plus three things: choice, constraints and optimisation. Together they turn a query language into a way of stating problems.

Everything from the core language chapters works in clingo. Facts, rules, joins, recursion, negation and aggregates are all there, with capitalised variables and no question marks.

What is new is that a clingo program does not have one answer. It has some number of stable models, each one a consistent world in which every rule holds. Zero models means the program is contradictory, which is a useful thing to be able to prove. Several models means there is more than one way for the rules to be satisfied, which is what you want when you are looking for a plan rather than a report.

negation.lp

% Negation as failure, and the safety rule that goes with it.
% Run:    clingo negation.lp
% Expect: SATISFIABLE with lonely(c), lonely(d), unreached(a), unreached(d)
%         and stranded(d). c is lonely because nothing leaves it, and d is
%         both lonely and unreached because nothing leaves or enters it.

node(a; b; c; d).
edge(a, b). edge(b, c).

% #defined declares a predicate that a facts file may legitimately leave
% empty. Without it every rule mentioning the predicate produces a warning,
% and warning spam trains people to ignore warnings.
#defined banned/1.

% not means "not derivable", which is not the same as "false". X has to be
% bound by a positive literal first: `lonely(X) :- not edge(X, _).` is
% rejected as unsafe, because clingo has no idea what X ranges over.
lonely(X) :- node(X), not edge(X, _).

% The same shape for "nothing points at it".
unreached(X) :- node(X), not edge(_, X).

% Negation over a derived predicate is fine as long as no cycle passes
% through it. This one does not: reachable is finished before allowed looks
% at it.
reachable(Y) :- edge(a, Y).
reachable(Y) :- reachable(X), edge(X, Y).
stranded(X) :- node(X), X != a, not reachable(X).

#show lonely/1.
#show unreached/1.
#show stranded/1.

The three additions

Choice rules generate

{ p(X) : q(X) } in a head says any subset of these may hold. With bounds, 1 { ... } 1, it says exactly one. This is how a search space is described without describing a search.
Integrity constraints eliminate

A rule with no head, :- body., says this must never happen. Every world where the body holds is discarded. Constraints do not compute anything; they remove possibilities, and that is why they compose so well.
Optimisation ranks

#minimize and #maximize put an order on the surviving worlds, so the solver can report the best rather than any.

Grounding, and why it matters

clingo works in two phases. Grounding replaces every variable with every constant it could take, producing a propositional program with no variables in it. Solving then searches that program for stable models with a conflict driven SAT solver.

This is the fundamental difference from Nemo, and it sets the shape of everything you can do. The grounding has to fit in memory, so clingo works on small worlds and thinks hard about them, while Nemo streams over large ones and thinks in straight lines.

Meta statement	Does
#const n = 4.	a constant, overridable with -c n=6
#show p/2.	whitelist the output. Any #show hides everything else
#show.	show nothing at all except explicit terms
#defined p/1.	declare an input a facts file may leave empty
#include "other.lp".	textual inclusion
#minimize { W, X : p(X, W) }.	optimise
#external toggle(1..3).	atoms whose truth is set from the API between solves
#program step(t).	a named subprogram, for incremental grounding

1 { queen(R, C) : column(C) } 1 :- row(R).

Generate, define, test

The shape of nearly every answer set program. Describe the space, define what the terms mean, then say what must never be true.

coloring.lp

% Generate, define, test: the shape of nearly every ASP program.
% Run:    clingo coloring.lp 0
% Expect: SATISFIABLE, 18 models. A four cycle has (k-1)^n + (k-1)(-1)^n
%         proper colourings, which for k=3, n=4 is 16 + 2.

node(1..4).
edge(1,2). edge(2,3). edge(3,4). edge(4,1).
colour(red; green; blue).

% GENERATE: exactly one colour per node. The bounds matter. Without the
% leading 1 the empty assignment is a model, which is the usual reason a
% first ASP program returns something degenerate.
1 { assign(N, C) : colour(C) } 1 :- node(N).

% TEST: an integrity constraint forbids the worlds you do not want. A rule
% with no head reads as "never this".
:- edge(X, Y), assign(X, C), assign(Y, C).

#show assign/2.

Three lines of logic, and no search algorithm. The choice rule says each node gets exactly one colour, the constraint says two adjacent nodes may not share one, and everything else is the solver's problem.

Python 3.12

"""Graph colouring by hand, which is what a solver saves you from.

The encoding in clingo is three lines: one choice rule, one constraint, one
#show. This is the same problem with the search written out, and the search
is the part that gets harder every time a requirement arrives.
"""

from itertools import product

NODES = [1, 2, 3, 4]
EDGES = [(1, 2), (2, 3), (3, 4), (4, 1)]
COLOURS = ["red", "green", "blue"]


def brute_force() -> list[dict[int, str]]:
    """Try every assignment. 3^4 here, 3^30 for a thirty node graph."""
    models = []
    for combination in product(COLOURS, repeat=len(NODES)):
        assignment = dict(zip(NODES, combination))
        if all(assignment[a] != assignment[b] for a, b in EDGES):
            models.append(assignment)
    return models


def backtracking() -> list[dict[int, str]]:
    """Better, and now you own a search algorithm as well as a problem."""
    models: list[dict[int, str]] = []
    assignment: dict[int, str] = {}

    def consistent(node: int, colour: str) -> bool:
        for a, b in EDGES:
            if a == node and assignment.get(b) == colour:
                return False
            if b == node and assignment.get(a) == colour:
                return False
        return True

    def step(index: int) -> None:
        if index == len(NODES):
            models.append(dict(assignment))
            return
        node = NODES[index]
        for colour in COLOURS:
            if consistent(node, colour):
                assignment[node] = colour
                step(index + 1)
                del assignment[node]

    step(0)
    return models


if __name__ == "__main__":
    print(len(brute_force()), "models by brute force")
    print(len(backtracking()), "models by backtracking")
    # Now add "the busiest colour must not be used more than twice" and see
    # which of these two files you would rather edit.

clingo coloring.lp 0

$ clingo coloring.lp 0
clingo version 5.6.2
Reading from coloring.lp
Solving...
Answer: 1
assign(1,green) assign(2,blue) assign(3,green) assign(4,red)
Answer: 2
...
SATISFIABLE

Models       : 18
Calls        : 1
Time         : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

The same shape, on a real problem

queens.lp

% N queens, the traditional way to see that a constraint is a sentence.
% Run:    clingo queens.lp -c n=8
% Expect: SATISFIABLE. With `0` instead, 92 models for n=8.

#const n = 8.

row(1..n).
column(1..n).

% One queen per row, which already rules out most of the search space.
1 { queen(R, C) : column(C) } 1 :- row(R).

% No two on a column, and none on a shared diagonal. Each constraint is one
% sentence about what must never be true, and none of them says how to
% search.
:- queen(R1, C), queen(R2, C), R1 != R2.
:- queen(R1, C1), queen(R2, C2), R1 != R2, R1 - R2 == C1 - C2.
:- queen(R1, C1), queen(R2, C2), R1 != R2, R1 - R2 == C2 - C1.

#show queen/2.

GENERATE

A choice rule per decision. The bounds are the important part: { p(X) : q(X) } with no lower bound allows the empty selection, and a first program that returns a suspiciously empty world is almost always missing a 1.
DEFINE

Ordinary rules that give names to the things the constraints will talk about. This is where the Datalog you already know goes, and keeping it separate from the choices is what makes a program readable.
TEST

Integrity constraints. Each one is a single sentence about what must never be true, and they can be added and removed independently, which is why requirements arriving late is not a problem here the way it is in a hand written search.

Try it yourself

Add a requirement to the colouring program: red may be used at most once. Then add another: node 1 must not be blue. Notice that each one is a single line and that neither disturbs the others.

Hint: The first is an aggregate in a constraint. The second is a constraint over one atom. Neither needs the generate part to change at all.

Show one solution

coloring.lp

% Generate, define, test: the shape of nearly every ASP program.
% Run:    clingo coloring.lp 0
% Expect: SATISFIABLE, 18 models. A four cycle has (k-1)^n + (k-1)(-1)^n
%         proper colourings, which for k=3, n=4 is 16 + 2.

node(1..4).
edge(1,2). edge(2,3). edge(3,4). edge(4,1).
colour(red; green; blue).

% GENERATE: exactly one colour per node. The bounds matter. Without the
% leading 1 the empty assignment is a model, which is the usual reason a
% first ASP program returns something degenerate.
1 { assign(N, C) : colour(C) } 1 :- node(N).

% TEST: an integrity constraint forbids the worlds you do not want. A rule
% with no head reads as "never this".
:- edge(X, Y), assign(X, C), assign(Y, C).

#show assign/2.

:- sat(b).

Constraints, and UNSAT as a result

A constraint is a sentence about what must never happen. When no world survives them all, that is a proof, and it is often the answer you came for.

:- body. is a rule with nothing in the head. It reads as "never this", and it eliminates every world where the body holds. Constraints do not derive anything, which is why adding one can only ever reduce the set of models and never change what the surviving ones contain.

That property is what makes UNSAT meaningful. If a program has no models, no world satisfies your rules, and the solver has proved it rather than failed to find one.

equivalence.lp

% Proving two conditions equivalent, by failing to find a world that
% separates them. UNSAT is the proof; a model would be the counterexample.
%
% Run:    clingo equivalence.lp
% Expect: UNSATISFIABLE, which means (p and q) really is contained in (p).
%         Swap the last two lines and it becomes SATISFIABLE, and the model
%         printed is the world where they differ.

% Free atoms. Anything the encoder does not understand becomes one of these,
% and since a free atom only ever makes a program more satisfiable, every
% UNSAT verdict survives them: you prove less, and what you prove is true.
{ holds(p) }.
{ holds(q) }.

sat(a) :- holds(p), holds(q).
sat(b) :- holds(p).

% Demand a world where A holds and B does not. If none exists, A implies B.
:- not sat(a).
:- sat(b).

clingo equivalence.lp

$ clingo equivalence.lp
clingo version 5.6.2
Reading from equivalence.lp
Solving...
UNSATISFIABLE

Models       : 0
Calls        : 1
Time         : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)

Turning questions into constraints

Does A imply B?

Demand a world where A holds and B does not. UNSAT proves the implication. SAT hands you the world where it fails, which is a counterexample you can read.
Are A and B equivalent?

Two runs, one in each direction. Equivalence is containment both ways, and running the two separately tells you which direction failed.
Is this condition ever satisfiable?

Encode it and ask for one model. UNSAT means the condition is a contradiction, which for a filter, a permission rule or a query means it can never match anything.
Can these two implementations disagree?

Encode both, demand a disagreement, and solve. UNSAT is a proof of parity across every world of that size. SAT is a bug report with a witness attached.

#minimize { 1, S : add(S) }.

Optimisation and minimal counterexamples

Among the worlds that satisfy the rules, prefer the best. This is what turns a diagnosis into a suggestion and a bug report into the smallest one.

repair.lp

% Minimal repair: not "what is broken" but "what is the smallest fix".
% Run:    clingo repair.lp --opt-mode=optN 0
% Expect: OPTIMUM FOUND with cost 1. Adding beta alone covers f2 and f3,
%         which gamma and delta would need two packages to do.

referenced(f1; f2; f3).

have(alpha).
provides(alpha, f1).

available(beta; gamma; delta).
provides(beta, f2).
provides(beta, f3).
provides(gamma, f2).
provides(delta, f3).

% GENERATE: any subset of the available packages.
{ add(S) : available(S) }.

covered(F) :- provides(S, F), have(S).
covered(F) :- provides(S, F), add(S).

% TEST: every referenced field must end up covered.
:- referenced(F), not covered(F).

% OPTIMISE: among the worlds that satisfy the constraints, prefer the ones
% that add least. This is the line that turns a diagnosis into a suggestion.
#minimize { 1, S : add(S) }.

#show add/1.

clingo repair.lp --opt-mode=optN

$ clingo repair.lp --opt-mode=optN
clingo version 5.6.2
Reading from repair.lp
Solving...
Answer: 1
add(gamma) add(delta)
Optimization: 2
Answer: 2
add(beta)
Optimization: 1
Answer: 1
add(beta)
Optimization: 1
OPTIMUM FOUND

Models       : 3
  Optimum    : yes
Optimization : 1
Calls        : 1

The solver prints improving models as it finds them and then says OPTIMUM FOUND once it has proved no better one exists. That last step is a proof, not a timeout, which is the difference between this and a heuristic search.

A larger example

scheduling.lp

% A shift roster: generate, constrain, then optimise for fairness.
% Run:    clingo scheduling.lp --opt-mode=optN
% Expect: OPTIMUM FOUND with Optimization: 2. Everyone works, nobody works
%         a shift they cannot,
%         and the busiest person is as unbusy as the constraints allow.

day(mon; tue; wed).
shift(early; late).
person(ada; ben; cleo).

% What people cannot do. Written as facts, so the roster and the constraints
% never drift apart: change the fact, rerun, get a new roster.
unavailable(ada, mon).
unavailable(ben, early).
unavailable(cleo, wed).

% GENERATE: exactly one person on every shift of every day.
1 { assign(D, S, P) : person(P) } 1 :- day(D), shift(S).

% TEST: respect the unavailability, whichever form it took.
:- assign(D, _, P), unavailable(P, D).
:- assign(_, S, P), unavailable(P, S).

% Nobody works both shifts in one day.
:- assign(D, early, P), assign(D, late, P).

shifts(P, N) :- person(P), N = #count { D, S : assign(D, S, P) }.

% OPTIMISE: minimise the largest individual load. Minimising the total would
% do nothing, since the total is fixed at six.
worst(M) :- M = #max { N : shifts(_, N) }.
#minimize { M : worst(M) }.

#show assign/3.
#show shifts/2.

Notice what changes when a requirement arrives. Somebody cannot work Wednesdays: one fact. Nobody may work both shifts in a day: one constraint. Spread the load fairly: one minimize. None of them disturbs the others, and none requires thinking about how the search is performed.

Written	Means
#minimize { W, X : p(X, W) }.	minimise the total of W over distinct (W, X) tuples
#minimize { 1, X : p(X) }.	minimise how many p there are
#maximize { W, X : p(X, W) }.	the same, the other way
#minimize { W@2, X : ... }.	priority 2, which dominates any lower level
--opt-mode=optN	prove the optimum, then enumerate the models achieving it
--opt-mode=opt	report improving models and stop at the optimum

Try it yourself

Add a second objective to the roster: as well as balancing the load, prefer rosters where nobody works two days in a row. Decide whether it belongs at the same priority as fairness or a lower one, and justify the choice.

Hint: Derive an atom for each consecutive pair a person works, then minimise how many there are. If fairness must never be traded away for it, put it at a lower priority level.

Show one solution

scheduling.lp

% A shift roster: generate, constrain, then optimise for fairness.
% Run:    clingo scheduling.lp --opt-mode=optN
% Expect: OPTIMUM FOUND with Optimization: 2. Everyone works, nobody works
%         a shift they cannot,
%         and the busiest person is as unbusy as the constraints allow.

day(mon; tue; wed).
shift(early; late).
person(ada; ben; cleo).

% What people cannot do. Written as facts, so the roster and the constraints
% never drift apart: change the fact, rerun, get a new roster.
unavailable(ada, mon).
unavailable(ben, early).
unavailable(cleo, wed).

% GENERATE: exactly one person on every shift of every day.
1 { assign(D, S, P) : person(P) } 1 :- day(D), shift(S).

% TEST: respect the unavailability, whichever form it took.
:- assign(D, _, P), unavailable(P, D).
:- assign(_, S, P), unavailable(P, S).

% Nobody works both shifts in one day.
:- assign(D, early, P), assign(D, late, P).

shifts(P, N) :- person(P), N = #count { D, S : assign(D, S, P) }.

% OPTIMISE: minimise the largest individual load. Minimising the total would
% do nothing, since the total is fixed at six.
worst(M) :- M = #max { N : shifts(_, N) }.
#minimize { M : worst(M) }.

#show assign/3.
#show shifts/2.

clingo program.lp --enum-mode=cautious

Running clingo, and reading what it says

Enumeration modes, the Python API, exit codes, and the four ways a solve result can lie to code that reads it carelessly.

clingo-cli.sh

# One model, or all of them. 0 means "as many as exist".
clingo program.lp
clingo program.lp 0
clingo program.lp -n 5

# Set a #const from the command line.
clingo queens.lp -c n=12

# Optimisation. optN proves the optimum and then enumerates the models that
# achieve it, which is usually what you wanted.
clingo repair.lp --opt-mode=optN

# What is true in EVERY model, and what is true in at least one. Check
# satisfiability first: on an unsatisfiable program the cautious consequence
# set is empty, which reads exactly like "nothing is ever true".
clingo program.lp --enum-mode=cautious
clingo program.lp --enum-mode=brave

# Look at the grounding rather than the models, when a rule is not firing.
clingo program.lp --text

# Exit codes: 10 satisfiable, 20 unsatisfiable, 30 satisfiable AND the search
# space was exhausted. 30 is what you get from `clingo program.lp 0` with no
# optimisation anywhere, as well as from a proved optimum, so do not read it
# as "optimum found". Errors exit 65. None of these is zero, so `set -e` will
# end your script on a perfectly good solve.
clingo program.lp; echo "exit $?"

Enumeration modes

Mode	Answers
default	one model, if any exists
`0` or `-n 0`	all of them
`--enum-mode=cautious`	the atoms true in every model
`--enum-mode=brave`	the atoms true in at least one
`--opt-mode=optN`	the optimum, then every model achieving it

Cautious consequences are the interesting one. They answer "what must be true regardless of how the remaining choices go", which for a planning problem means the decisions that are forced and for a verification problem means the conclusions that hold in every world consistent with what you know.

Four ways to misread a result

Exit codes are not success codes

10 is satisfiable, 20 unsatisfiable, 30 satisfiable with the search space exhausted, and 65 an error. Read the first three as two flags, a model was found and the search ran to the end, and the values explain themselves: UNSAT is the second flag alone, and 30 covers both a proved optimum and a plain 0 enumeration that ran to the end, so it does not by itself mean an optimum was found. A shell script with set -e dies on every one of them. The pip wheel's python3 -m clingo exits zero regardless, so its exit code carries no information at all. Read the verdict, or use the API.
An interrupted solve is not an answer

Under a time limit or a conflict bound, satisfiable is None and the model list is partial. Read that through a boolean and cautious becomes "nothing is forced", counterexample search becomes "no violating world", and enumeration becomes "an exhaustive census". Three false certifications from one None. Guard for it at every consumer.
UNSAT gives you no consequences

Cautious enumeration on an unsatisfiable program returns nothing, which reads exactly like "no atom is always true". Check satisfiability first.
A checker you have never seen fail is theatre

Before trusting any verification program, reintroduce the bug it is supposed to catch and watch it go red. A check that has passed since the day it was written may be validating nothing at all, and there is no way to tell from the outside.

:- not violation(_, _, _).

When the answer is wrong

Nemo's failure is an empty relation. clingo's is worse: it answers, the answer looks like a result, and it is the answer to a question you did not ask.

A Nemo program that is wrong derives nothing, and nothing is at least visibly nothing. A clingo program that is wrong returns UNSATISFIABLE, or a model, or an optimum, and every one of those looks exactly like success. The verdict is the diagnosis, so the flow starts there.

Verdict	First thing to suspect
UNSATISFIABLE you did not expect	A generator whose domain is empty, so the choice rule chose from nothing
SATISFIABLE where you wanted a proof	Either a real counterexample, or an encoding that permits a world the system cannot reach
A model missing atoms you derive	A `#show` is hiding them
An optimum that looks wrong	Interrupted, dominated by a priority level, or optimising a constant
Grounding that never finishes	One rule whose variables range over more than you think

Unexpected UNSAT

UNSATISFIABLE means no world satisfies the rules, and when you expected one, the usual reason is not that your constraints are too strong but that your generator produced nothing to constrain. 1 { assign(N, C) : colour(C) } 1 :- node(N). is unsatisfiable the moment colour is empty, because it demands exactly one of nothing. Check the domains first, every time: --text shows the grounding, and an absent generator is absent there in a way it never is in the source.

Once the domains are real, bisect. Comment out half the constraints. If it becomes satisfiable, the culprit is in the half you removed; if not, it is in the half you kept. Six halvings will find one constraint among sixty, and this is faster than reasoning about them.

A model where you wanted a proof

contract.lp

% The spec oracle: one rule, written once, and two implementations that must
% agree with it. Seam bugs live exactly here, where the same rule was
% written twice and one copy drifted.
%
% Run:    clingo contract.lp 0
% Expect: SATISFIABLE, and every model is a world where the implementation
%         and the spec disagree. Each one is a bug report with a witness.
%         Fix impl_visible and it turns UNSATISFIABLE, which is the proof.

% GENERATE a small world. Three users and two threads find the visibility
% bugs that matter; larger worlds mostly find the same ones again, slower.
user(u1; u2; u3).
thread(t1; t2).

{ owner(T, U) : user(U) } = 1 :- thread(T).
{ admin(U) } :- user(U).
{ blocked(U, V) } :- user(U), user(V), U != V.
{ deleted(T) } :- thread(T).

% THE SPEC: one written truth. A thread is visible to a viewer when it is
% not deleted, and the viewer is not blocked by its owner, and the viewer
% owns it or is an admin. Note that the block check wraps the admin check
% rather than the other way round: being an admin does not defeat a block.
spec_visible(T, V) :-
    thread(T), user(V), owner(T, O),
    not deleted(T),
    not blocked(O, V),
    admin_or_owner(V, T).

admin_or_owner(V, T) :- owner(T, V).
admin_or_owner(V, T) :- admin(V), thread(T).

% THE IMPLEMENTATION, translated from what the code actually does rather
% than copied from the spec. A diff is only meaningful between two separate
% derivations. This one checks admin first and never gets to the block.
impl_visible(T, V) :- thread(T), user(V), admin(V), not deleted(T).
impl_visible(T, V) :- thread(T), user(V), owner(T, V), not deleted(T), not blocked(V, V).

% THE CONTRACT: both directions. A leak is a thread shown when it should be
% hidden; an over-filter is one hidden when it should be shown. Both are
% regressions, and a checker that only looks for one of them will pass on
% the day the other happens.
violation(leak, T, V) :- impl_visible(T, V), not spec_visible(T, V).
violation(overfilter, T, V) :- spec_visible(T, V), not impl_visible(T, V).

% Demand a disagreement. UNSAT here would be a proof of parity across every
% world of this size.
:- not violation(_, _, _).

#show violation/3.
#show blocked/2.
#show admin/1.
#show owner/2.

What the engine says

$ clingo equivalence.lp
clingo version 5.6.2
Reading from equivalence.lp
Solving...
UNSATISFIABLE

Models       : 0
Calls        : 1
Time         : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)

When a verification program returns a model, one of two things is true, and both are progress. Either the model is a real counterexample, in which case you have found the bug and it comes with a witness you can reproduce. Or it is a world your encoding permits and reality does not, in which case you have found a missing constraint, and adding it makes the proof stronger rather than weaker.

Telling the two apart takes reading the model, which is why it pays to keep the generated world small enough to read. Three users and two threads fit on a line. Thirty users produce the same bugs in a form nobody checks by hand.

Grounding that never finishes

Grounding instantiates every rule over every combination its variables admit, so one careless body can produce more instances than the solver will ever see. The rule is always findable: run with --text on progressively smaller subsets of the facts and watch which rule's instance count grows fastest. It is nearly always one where a variable is bound by something larger than the thing it is really about.

narrow

Bind from the smallest generator

If a variable ranges over every integer when it means "a shift on this day", say so. The fix is usually a domain predicate that already exists a few lines above.

order

Put the selective atom first

Grounding is not solving, and unlike the solver it does not reorder freely. A body atom that narrows the range early narrows everything after it.

measure

Read --stats before optimising

Grounding time and solving time have different cures, and the statistics say which one you have. Guessing here wastes an afternoon reliably.

reach

Know when to leave

If the honest domain is genuinely enormous, no encoding trick will save it. That is the boundary where clingo hands over to Nemo, or to clingo-dl for arithmetic over wide ranges.

Optima that are not

Check it was proved, not interrupted

OPTIMUM FOUND is a proof. A model printed under a time limit is not, and the + after the model count is the tell. Read the verdict, never the last model printed.
Check the total is not fixed

Minimising something that cannot change reports OPTIMUM FOUND instantly, having optimised a constant. Six shifts covered by somebody always total six. Minimise the maximum instead, and watch the objective actually move.
Check the priorities

@2 dominates every magnitude at @1. If a large improvement is being ignored for a small one, that is not a bug, it is the priority doing what priorities do, and the two objectives probably belong at the same level with weights.

Try it yourself

Take the colouring program and make it unsatisfiable in two different ways: once by deleting the colour facts, and once by adding a constraint that genuinely cannot be met. Then look at the two outputs and note how little they differ.

Hint: They are identical apart from the timing. That is the whole reason the empty-domain check comes first: the verdict cannot tell you which kind of UNSAT you have, so you have to ask separately.

Show one solution

coloring.lp

% Generate, define, test: the shape of nearly every ASP program.
% Run:    clingo coloring.lp 0
% Expect: SATISFIABLE, 18 models. A four cycle has (k-1)^n + (k-1)(-1)^n
%         proper colourings, which for k=3, n=4 is 16 + 2.

node(1..4).
edge(1,2). edge(2,3). edge(3,4). edge(4,1).
colour(red; green; blue).

% GENERATE: exactly one colour per node. The bounds matter. Without the
% leading 1 the empty assignment is a model, which is the usual reason a
% first ASP program returns something degenerate.
1 { assign(N, C) : colour(C) } 1 :- node(N).

% TEST: an integrity constraint forbids the worlds you do not want. A rule
% with no head reads as "never this".
:- edge(X, Y), assign(X, C), assign(Y, C).

#show assign/2.

component(?x, #min(?y)) :- connected(?x, ?y) .

Graph recipes

Reachability, cycles, components and distance, and which of them is genuinely easy here and which needs care.

graphs.rls

%! Graph recipes: reachability, cycles, components and distance.
%! Verify: inCycle = a | b | c
%! Verify: component = a a | b a | c a | d a | e e | f e

edge(a, b) .
edge(b, c) .
edge(c, a) .
edge(c, d) .
edge(e, f) .

%%% Reachability, directed.
reaches(?x, ?y) :- edge(?x, ?y) .
reaches(?x, ?z) :- reaches(?x, ?y), edge(?y, ?z) .

%%% A cycle is a node that reaches itself.
inCycle(?x) :- reaches(?x, ?x) .

%%% Undirected connectivity: make the edge symmetric first, then close it.
%%% Doing this in one recursive rule instead is a common way to write a
%%% program that is correct and much slower.
link(?x, ?y) :- edge(?x, ?y) .
link(?y, ?x) :- edge(?x, ?y) .

connected(?x, ?y) :- link(?x, ?y) .
connected(?x, ?z) :- connected(?x, ?y), link(?y, ?z) .

node(?x) :- edge(?x, _) .
node(?y) :- edge(_, ?y) .

%%% Every node is connected to itself, which the closure above does not say
%%% for isolated nodes.
connected(?x, ?x) :- node(?x) .

%%% A component is named by its alphabetically smallest member, which gives
%%% every member of a component the same label. #min orders strings too.
component(?x, #min(?y)) :- connected(?x, ?y) .

%%% Path length. Recursion is safe, but this counts every path rather than
%%% the shortest one, so take the minimum afterwards.
hops(?x, ?y, 1) :- edge(?x, ?y) .
hops(?x, ?z, ?n) :- hops(?x, ?y, ?m), edge(?y, ?z), ?n = ?m + 1, ?m < 10 .

distance(?x, ?y, #min(?n)) :- hops(?x, ?y, ?n) .

@export component :- csv{resource = "components.csv"} .
@export distance :- csv{resource = "distance.csv"} .

SQL

-- Shortest distance from one node, in SQL. Compare with the four Datalog
-- rules that say the same thing.
WITH RECURSIVE hops(node, dist) AS (
    SELECT b, 1 FROM edge WHERE a = 'a'
    UNION
    SELECT e.b, h.dist + 1
    FROM hops h
    JOIN edge e ON e.a = h.node
    WHERE h.dist < 100          -- a hand written bound, or this never ends
)
SELECT node, MIN(dist) AS dist
FROM hops
GROUP BY node;

-- The UNION deduplicates whole rows, so a node reached at two different
-- distances stays twice and the MIN at the end is doing the real work. The
-- engine has explored every path, not every node, which is why this gets
-- slow long before the graph gets large.

Question	Rules	Note
Reachability	two	the base case and the recursive case
Cycle detection	one more	a node that reaches itself
Undirected connectivity	three	symmetrise first, then close
Connected components	one aggregate	label each node with the smallest node it reaches
Same component	one join	two nodes with the same label
Path length	two, plus a bound	counts every path, so take the minimum after
Shortest path	hard	wants subsumption, which Souffle has and these two do not
Topological order	hard	a relation has no order. Derive depth instead

The two that are harder than they look

That last trick is worth seeing written out, because "insert this between those two" is the request an ordering relation makes awkward and the one that keeps arriving. Doubling every position on the way in buys a named gap between each adjacent pair, so a new item can be placed without renumbering anything around it.

ranks.lp

% Ordering without a sequence: dense ranks, and the gaps between them.
% Run:    clingo ranks.lp
% Expect: SATISFIABLE, 1 model, with placed(x, r(5)): the gap between b
%         at rank 4 and c at rank 6. Never a rank an item already holds.
%
% A relation has no order, so "insert this between those two" has no direct
% expression. The way through is to make the order a relation and to give
% the gaps names of their own.

item(a; b; c).
position(a, 1).
position(b, 2).
position(c, 3).

% Existing items sit at EVEN ranks, so every gap between two neighbours has
% an odd rank of its own to be named by. Doubling on the way in is what buys
% the room; without it, "between 2 and 3" has nowhere to go and the whole
% list has to be renumbered to make space.
rank(I, 2 * P) :- position(I, P).

% The odd ranks are the gaps. r(3) sits between a at 2 and b at 4; r(5)
% between b at 4 and c at 6. Every adjacent pair has exactly one, so an
% insertion point can be named without disturbing anything around it.
gap(R) :- rank(_, Hi), R = Hi - 1, R > 0.

% GENERATE: put the new item in exactly one gap.
1 { placed(x, r(R)) : gap(R) } 1.

% TEST: the requirement, stated directly. x goes after b and before c.
% This is the whole point of the encoding: the constraint mentions the
% neighbours it cares about, and no other item's rank has to change.
:- placed(x, r(R)), rank(b, Rb), R < Rb.
:- placed(x, r(R)), rank(c, Rc), R > Rc.

% x is new, so it may not land exactly on an existing item's rank. With the
% doubling this is automatic - gaps are odd, items are even - and stating it
% anyway means the constraint still holds if the encoding ever changes.
:- placed(x, r(R)), rank(_, R).

#show placed/2.
#show rank/2.

Try it yourself

Find every node that lies on a cycle, and then every node that can reach a cycle without being on one. The second is the interesting one for dependency analysis: those are the modules that are not themselves circular but cannot be built without something that is.

Hint: inCycle is one rule. The second is reachability into inCycle, with the cycle members negated out.

Show one solution

graphs.rls

%! Graph recipes: reachability, cycles, components and distance.
%! Verify: inCycle = a | b | c
%! Verify: component = a a | b a | c a | d a | e e | f e

edge(a, b) .
edge(b, c) .
edge(c, a) .
edge(c, d) .
edge(e, f) .

%%% Reachability, directed.
reaches(?x, ?y) :- edge(?x, ?y) .
reaches(?x, ?z) :- reaches(?x, ?y), edge(?y, ?z) .

%%% A cycle is a node that reaches itself.
inCycle(?x) :- reaches(?x, ?x) .

%%% Undirected connectivity: make the edge symmetric first, then close it.
%%% Doing this in one recursive rule instead is a common way to write a
%%% program that is correct and much slower.
link(?x, ?y) :- edge(?x, ?y) .
link(?y, ?x) :- edge(?x, ?y) .

connected(?x, ?y) :- link(?x, ?y) .
connected(?x, ?z) :- connected(?x, ?y), link(?y, ?z) .

node(?x) :- edge(?x, _) .
node(?y) :- edge(_, ?y) .

%%% Every node is connected to itself, which the closure above does not say
%%% for isolated nodes.
connected(?x, ?x) :- node(?x) .

%%% A component is named by its alphabetically smallest member, which gives
%%% every member of a component the same label. #min orders strings too.
component(?x, #min(?y)) :- connected(?x, ?y) .

%%% Path length. Recursion is safe, but this counts every path rather than
%%% the shortest one, so take the minimum afterwards.
hops(?x, ?y, 1) :- edge(?x, ?y) .
hops(?x, ?z, ?n) :- hops(?x, ?y, ?m), edge(?y, ?z), ?n = ?m + 1, ?m < 10 .

distance(?x, ?y, #min(?n)) :- hops(?x, ?y, ?n) .

@export component :- csv{resource = "components.csv"} .
@export distance :- csv{resource = "distance.csv"} .

depends("app", "left-pad") .

Getting the facts out

Every applied chapter assumes the facts arrived from somewhere. This is the somewhere: twenty lines of ordinary code, and the decisions inside them that the rules can never recover from.

The rules in this book are short. That is the honest advertisement for the language, and it is also slightly misleading, because the reason they are short is that something else already did the hard part: it turned a program, a lockfile, a database or a config tree into ground atoms. Nothing in Datalog helps with that step. It is ordinary code in an ordinary language, it is usually about twenty lines, and it decides whether the analysis on top of it means anything at all.

So here is the step every other chapter skipped, end to end: a real artefact, an extractor, and the rules from the graph chapter pointed at the result.

extract.py

"""Turning a real artefact into facts, which is the step every chapter assumes.

The rules in this book are short because the hard part happened before them:
somebody turned a program, a database or a config file into ground atoms. That
step is ordinary code, it is usually about twenty lines, and it is where the
honesty of the whole analysis is decided.

This reads an npm lockfile and writes `depends(a, b) .` facts. Point the graph
chapter's rules at the output and you get cycles, orphans and reachability over
your own dependency tree.

    python3 extract.py package-lock.json > deps.rls
    cat deps.rls graph-rules.rls > analysis.rls && nmo analysis.rls -e idb
"""

import json
import re
import sys

# Nemo reads a bare name as an IRI and a quoted name as a string, and the two
# never join with each other. Package names contain slashes and dots, so they
# are written as strings here, and every rule that consumes them must quote its
# constants too. Choosing one convention and writing it down is the single
# cheapest thing an extractor can do for whoever reads the rules later.
SAFE = re.compile(r'^[A-Za-z0-9@/._-]+$')


def quote(name: str) -> str:
    """A Nemo string literal, with the two characters that could break out."""
    return '"' + name.replace("\\", "\\\\").replace('"', '\\"') + '"'


def package_name(path: str) -> str:
    """`node_modules/a/node_modules/b` is package b. Take the last segment."""
    return path.split("node_modules/")[-1]


def extract(lockfile: dict):
    """Yield (dependent, dependency) pairs from a lockfile version 2 or 3."""
    packages = lockfile.get("packages")
    if packages is None:
        raise SystemExit("expected a v2 or v3 lockfile with a 'packages' key")

    for path, entry in packages.items():
        # The root package has an empty path and is the one thing here that is
        # not a dependency of anything.
        source = package_name(path) if path else lockfile.get("name", "root")

        for section in ("dependencies", "devDependencies", "optionalDependencies"):
            for target in entry.get(section, {}):
                if SAFE.match(source) and SAFE.match(target):
                    yield source, target


def main() -> None:
    if len(sys.argv) != 2:
        raise SystemExit(f"usage: {sys.argv[0]} package-lock.json")

    with open(sys.argv[1], encoding="utf-8") as handle:
        lockfile = json.load(handle)

    pairs = sorted(set(extract(lockfile)))

    # The schema, written down where the facts are. Every predicate in this
    # book carries one of these, because nothing in the language enforces
    # argument order and a transposed argument produces a program that runs.
    print("%%% depends(dependent, dependency)")
    for source, target in pairs:
        print(f"depends({quote(source)}, {quote(target)}) .")

    # Counts on stderr, so the facts on stdout stay pipeable. An extractor that
    # silently produces nothing is the most expensive failure in this pipeline:
    # every downstream check goes green on an empty world.
    print(f"extracted {len(pairs)} edges", file=sys.stderr)
    if not pairs:
        raise SystemExit("no dependencies found: refusing to emit an empty world")


if __name__ == "__main__":
    main()

There is no cleverness in it, and that is the point. It walks a structure, it picks two fields, and it prints one line per pair. The only interesting decisions are the ones about representation, and they are the ones you cannot change your mind about later without changing every rule downstream.

The four decisions an extractor makes

Strings or bare names

A bare left-pad is the IRI <left-pad>; "left-pad" is a string. They never join with each other, and package names contain slashes and dots, so strings are the right answer here. What matters is not which you pick but that the extractor and every rule agree, which is why the choice belongs in a comment at the top of the facts.
What a row means

depends(dependent, dependency) is a promise nothing enforces. Write it above the facts, in the extractor, so that the schema travels with the data rather than living in the memory of whoever wrote the rules.
What to leave out

Version ranges, resolved URLs, integrity hashes: all present, none needed for reachability. An extractor that emits everything produces a slower program and a harder one to read. Emit what a rule will join on, and go back for more when a rule needs it.
What to do about nothing

The extractor above exits non-zero rather than emitting an empty world. This is the single most important line in it: every check downstream of an empty fact set passes, and a green build from no data is worse than a red one.

Then the rules are the easy part

deps.rls

%! Dependency analysis over facts an extractor produced.
%!
%! Run: python3 extract.py package-lock.json > deps-facts.rls
%!      cat deps-facts.rls deps.rls > analysis.rls && nmo analysis.rls -e idb
%!
%! Verify: cyclic = b | c
%! Verify: blocked = app
%! Verify: orphan = app | d

%%% depends(dependent, dependency)
%%% A handful of facts written out, so this file runs on its own. In use
%%% they arrive from extract.py, quoted the same way: the extractor and
%%% the rules have to agree about strings against bare names, and this
%%% comment is where that agreement is written down.
depends("app", "left-pad") .
depends("app", "b") .
depends("b", "c") .
depends("c", "b") .
depends("d", "left-pad") .

%%% Everything involved, which negation below needs a domain to range over.
package(?p) :- depends(?p, _) .
package(?p) :- depends(_, ?p) .

%%% Reachability, which is the whole of this analysis.
reaches(?a, ?b) :- depends(?a, ?b) .
reaches(?a, ?c) :- reaches(?a, ?b), depends(?b, ?c) .

%%% A cycle is a package that reaches itself. On a dependency graph this is
%%% the finding that stops a build, and it is one rule.
cyclic(?p) :- reaches(?p, ?p) .

%%% Not itself circular, but cannot be built without something that is.
%%% This is the query nobody writes by hand, and the one that explains why
%%% a build breaks in a package whose own dependencies look fine.
blocked(?p) :- reaches(?p, ?q), cyclic(?q), ~cyclic(?p) .

%%% Nothing depends on it: an entry point, or dead weight.
orphan(?p) :- package(?p), ~depends(_, ?p) .

%%% How many things would break if this package broke. Distinct dependents
%%% is exactly the question here, so a single argument is right: reaches is
%%% already a set, and counting it twice per package would be the bug.
% checker: expected
blastRadius(?p, #count(?dependent)) :- reaches(?dependent, ?p) .

@export cyclic :- csv{resource = "cyclic.csv"} .
@export blocked :- csv{resource = "blocked.csv"} .
@export blastRadius :- csv{resource = "blast-radius.csv"} .

Four questions, one rule each, over facts that came out of a file nobody wrote for this purpose. cyclic is the build breaker. blocked is the one nobody writes by hand: a package that is not itself circular but cannot be built without something that is, which is why a failure shows up somewhere that looks innocent. orphan finds entry points and dead weight with the same rule, because they are the same shape and only you know which one you are looking at.

compilers

From an AST

One visitor, one atom per node type: assigns, calls, reads. This is exactly what Doop does to Java bytecode, and the taint rules from the analysis chapter run unchanged on top of it.

databases

From SQL

One query per predicate, rendering rows straight into fact strings. Scope the extraction deliberately, or leftover rows from an unrelated test will fail a run that had nothing to do with them.

infrastructure

From config

Terraform state, Kubernetes manifests and IAM policies are already trees of relations. grants(role, permission) and assumes(role, role) turn a permissions audit into the reachability query it always was.

logs

From events

An append-only log is a fact table that needs no extraction at all, only a projection. The temporal patterns are the same joins with a timestamp column carried through them.

Smell	What it usually means
The fact file is enormous	You emitted columns no rule joins on
Every rule needs a conversion	The extractor picked the wrong representation once, and everything pays for it
A join is empty and the rules look right	Bare name against quoted string. It is nearly always this
The analysis passes on a broken system	The extraction ran, found nothing, and nothing said so
Two extractors, one schema	They have already drifted. Only one of them is right, and nobody knows which

Try it yourself

Run the extractor over a lockfile from a project you actually work on, and answer one question with it: which package has the largest blast radius. Then look at whether that package is one you would have guessed.

Hint: blastRadius is already in deps.rls. The answer is usually not the biggest dependency but a small one that everything transitively pulls in, which is the argument for computing it rather than estimating it.

Show one solution

deps.rls

%! Dependency analysis over facts an extractor produced.
%!
%! Run: python3 extract.py package-lock.json > deps-facts.rls
%!      cat deps-facts.rls deps.rls > analysis.rls && nmo analysis.rls -e idb
%!
%! Verify: cyclic = b | c
%! Verify: blocked = app
%! Verify: orphan = app | d

%%% depends(dependent, dependency)
%%% A handful of facts written out, so this file runs on its own. In use
%%% they arrive from extract.py, quoted the same way: the extractor and
%%% the rules have to agree about strings against bare names, and this
%%% comment is where that agreement is written down.
depends("app", "left-pad") .
depends("app", "b") .
depends("b", "c") .
depends("c", "b") .
depends("d", "left-pad") .

%%% Everything involved, which negation below needs a domain to range over.
package(?p) :- depends(?p, _) .
package(?p) :- depends(_, ?p) .

%%% Reachability, which is the whole of this analysis.
reaches(?a, ?b) :- depends(?a, ?b) .
reaches(?a, ?c) :- reaches(?a, ?b), depends(?b, ?c) .

%%% A cycle is a package that reaches itself. On a dependency graph this is
%%% the finding that stops a build, and it is one rule.
cyclic(?p) :- reaches(?p, ?p) .

%%% Not itself circular, but cannot be built without something that is.
%%% This is the query nobody writes by hand, and the one that explains why
%%% a build breaks in a package whose own dependencies look fine.
blocked(?p) :- reaches(?p, ?q), cyclic(?q), ~cyclic(?p) .

%%% Nothing depends on it: an entry point, or dead weight.
orphan(?p) :- package(?p), ~depends(_, ?p) .

%%% How many things would break if this package broke. Distinct dependents
%%% is exactly the question here, so a single argument is right: reaches is
%%% already a set, and counting it twice per package would be the bug.
% checker: expected
blastRadius(?p, #count(?dependent)) :- reaches(?dependent, ?p) .

@export cyclic :- csv{resource = "cyclic.csv"} .
@export blocked :- csv{resource = "blocked.csv"} .
@export blastRadius :- csv{resource = "blast-radius.csv"} .

tainted(?to) :- assign(?to, ?from), tainted(?from) .

Static analysis

The application Datalog quietly won. Taint tracking, points-to and dead code are all reachability, and reachability is three lines.

A compiler front end turns a program into facts: this statement assigns that variable, this function calls that one, this value comes from a request parameter. The extraction chapter walked that step end to end for a dependency tree; a compiler front end is the same twenty lines pointed at an AST. Once the program is facts, most of what a static analyser does is a query.

This is not a curiosity. Doop analyses Java bytecode this way and remains one of the most precise points-to analyses available. Semmle, which became CodeQL and now runs on a large share of the world's repositories, started as a Datalog dialect over the same idea.

taint.rls

%! Taint analysis, which is what Datalog was quietly winning at all along.
%!
%! Facts here would come from a compiler front end. The rules are the whole
%! analysis, and they are the same three lines whether the program has ten
%! statements or ten million.
%! Verify: vulnerability = query userInput
%! Verify: unprotected = query

%%% assign(target, source): a value flows from source into target.
assign(x, userInput) .
assign(y, x) .
assign(z, constant) .
assign(query, y) .
assign(safeQuery, sanitised) .
assign(sanitised, x) .

%%% Where untrusted data enters, and where it must not arrive.
source(userInput) .
sink(query) .
sink(safeQuery) .

%%% A sanitiser makes a value safe no matter where it came from.
sanitiser(sanitised) .

%%% Taint flows along assignments, and stops at a sanitiser.
tainted(?v) :- source(?v) .
tainted(?to) :- assign(?to, ?from), tainted(?from), ~sanitiser(?to) .

%%% The finding, with enough context to be actionable.
vulnerability(?sink, ?origin) :- sink(?sink), tainted(?sink), source(?origin) .

%%% The dual check, which is the one people forget: a sink that no sanitiser
%%% protects and no source reaches today is one refactor away from a bug.
unprotected(?sink) :- sink(?sink), ~reachesSanitiser(?sink) .
reachesSanitiser(?v) :- sanitiser(?v) .
reachesSanitiser(?to) :- assign(?to, ?from), reachesSanitiser(?from) .

@export vulnerability :- csv{resource = "vulnerabilities.csv"} .

Why this shape suits the problem

The analysis is recursive by nature

Taint flows through assignments, through function calls, through fields, and back out again. Every one of those is a transitive closure, and writing them as rules is writing the definition down rather than implementing it.
Sensitivity is a parameter, not a rewrite

Context sensitivity means adding a context argument to the predicates. Field sensitivity means adding a field. The rules keep the same shape and the precision changes, which is why research in this area is largely conducted in Datalog.
The engine handles the scale

A real program produces millions of facts. Semi-naive evaluation, indexing and join ordering are the engine's problem, and they are the parts a hand written analyser gets wrong.
Both directions of the check are cheap

Finding what is tainted is one rule. Finding sinks that no sanitiser protects is another. That second query is the one nobody writes by hand, and it is the one that catches the bug before it arrives.

Analysis	In rules
Reachable code	reachability from the entry points; anything not reached is dead
Taint tracking	reachability from sources, cut by sanitisers
Points-to	which allocation sites a variable may hold, closed over assignments and calls
Call graph	direct calls, plus dispatch resolved through the points-to result
Unused imports	imported, and not referenced anywhere
Cyclic dependencies	a module that reaches itself
Privilege escalation	reachability through a permission graph

type(?x, ?super) :- type(?x, ?c), subClass(?c, ?super) .

Ontologies and knowledge graphs

RDFS and OWL EL inference are a page of rules. Nemo reads RDF and SPARQL results directly, which makes this the shortest path from a triple store to an answer.

rdf.rls

%! Ontology reasoning over RDF, which is the other thing Datalog is for.
%! Verify: mortal = http://example.org/socrates

@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix ex: <http://example.org/> .

%%% A handful of triples, written out rather than imported so the program
%%% runs on its own. In practice this is @import triple :- rdf{...} .
triple(ex:socrates, rdf:type, ex:Philosopher) .
triple(ex:Philosopher, rdfs:subClassOf, ex:Human) .
triple(ex:Human, rdfs:subClassOf, ex:Mortal) .
triple(ex:teaches, rdfs:subPropertyOf, ex:knows) .
triple(ex:socrates, ex:teaches, ex:plato) .
triple(ex:knows, rdf:type, owl:TransitiveProperty) .
triple(ex:plato, ex:knows, ex:aristotle) .

%%% Subclasses are transitive.
subClass(?a, ?b) :- triple(?a, rdfs:subClassOf, ?b) .
subClass(?a, ?c) :- subClass(?a, ?b), triple(?b, rdfs:subClassOf, ?c) .

%%% Type inheritance: this is the whole of RDFS class reasoning.
type(?x, ?c) :- triple(?x, rdf:type, ?c) .
type(?x, ?super) :- type(?x, ?c), subClass(?c, ?super) .

%%% Property hierarchies work the same way.
triple(?s, ?super, ?o) :-
    triple(?s, ?p, ?o),
    triple(?p, rdfs:subPropertyOf, ?super) .

%%% A transitive property closes over itself. Nine lines have now
%%% implemented most of what people install a reasoner for.
triple(?s, ?p, ?o2) :-
    triple(?p, rdf:type, owl:TransitiveProperty),
    triple(?s, ?p, ?o),
    triple(?o, ?p, ?o2) .

mortal(?x) :- type(?x, ex:Mortal) .

@export mortal :- csv{resource = "mortals.csv"} .

Those nine rules implement most of what people install a reasoner for: class hierarchies, property hierarchies, type inheritance and transitive properties. The rules are the specification, written out, and you can add your own alongside them without asking whether the reasoner supports it.

What the standards call this

Fragment	What it covers	In rules
RDFS	subclasses, subproperties, domains, ranges	about eight
OWL RL	the rule expressible part of OWL 2	about eighty, all published
OWL EL	large biomedical ontologies such as SNOMED and Galen	a normalisation pass and a dozen rules
SHACL-ish validation	shape constraints over the graph	your own, plus negation

Import the triples

@import triple :- rdf{resource="data.nt.gz"} . reads N-Triples, Turtle or RDF/XML, gzipped or not, local or over HTTP. Quads give a four column predicate.
Or query a live endpoint

A sparql import runs a query against Wikidata or any other endpoint and turns the result rows into facts. That combination, a SPARQL query for the data and rules for the reasoning SPARQL cannot express, is what Nemo is unusually good at.
Normalise before reasoning

Serious OWL reasoning starts by rewriting the ontology into a small set of normal forms, so the reasoning rules stay few and fast. That pass is itself a set of rules, and existential rules are what let it introduce the fresh concepts it needs.
Materialise, then query

Bottom-up evaluation gives you every entailed triple, once. Writing those back into a store means every later query sees the inferences without paying for them again, which is the usual architecture.

violation(leak, T, V) :- impl_visible(T, V), not spec_visible(T, V).

Rules as contracts

Write a business rule once, in a language that can execute it, and check the implementations against it. Seam bugs are the ones this catches.

The worst bugs in a system that has been alive for a while are rarely clever. They are the same rule implemented twice, in two places, drifting apart: a visibility fix applied to one endpoint while the other keeps leaking, a counter that stopped agreeing with the rows it counts, a permission check that an admin path skips.

A solver is unusually good at that shape of problem, because the question is not "what is true" but "can these two possibly disagree", and that is a search over small worlds.

contract.lp

% The spec oracle: one rule, written once, and two implementations that must
% agree with it. Seam bugs live exactly here, where the same rule was
% written twice and one copy drifted.
%
% Run:    clingo contract.lp 0
% Expect: SATISFIABLE, and every model is a world where the implementation
%         and the spec disagree. Each one is a bug report with a witness.
%         Fix impl_visible and it turns UNSATISFIABLE, which is the proof.

% GENERATE a small world. Three users and two threads find the visibility
% bugs that matter; larger worlds mostly find the same ones again, slower.
user(u1; u2; u3).
thread(t1; t2).

{ owner(T, U) : user(U) } = 1 :- thread(T).
{ admin(U) } :- user(U).
{ blocked(U, V) } :- user(U), user(V), U != V.
{ deleted(T) } :- thread(T).

% THE SPEC: one written truth. A thread is visible to a viewer when it is
% not deleted, and the viewer is not blocked by its owner, and the viewer
% owns it or is an admin. Note that the block check wraps the admin check
% rather than the other way round: being an admin does not defeat a block.
spec_visible(T, V) :-
    thread(T), user(V), owner(T, O),
    not deleted(T),
    not blocked(O, V),
    admin_or_owner(V, T).

admin_or_owner(V, T) :- owner(T, V).
admin_or_owner(V, T) :- admin(V), thread(T).

% THE IMPLEMENTATION, translated from what the code actually does rather
% than copied from the spec. A diff is only meaningful between two separate
% derivations. This one checks admin first and never gets to the block.
impl_visible(T, V) :- thread(T), user(V), admin(V), not deleted(T).
impl_visible(T, V) :- thread(T), user(V), owner(T, V), not deleted(T), not blocked(V, V).

% THE CONTRACT: both directions. A leak is a thread shown when it should be
% hidden; an over-filter is one hidden when it should be shown. Both are
% regressions, and a checker that only looks for one of them will pass on
% the day the other happens.
violation(leak, T, V) :- impl_visible(T, V), not spec_visible(T, V).
violation(overfilter, T, V) :- spec_visible(T, V), not impl_visible(T, V).

% Demand a disagreement. UNSAT here would be a proof of parity across every
% world of this size.
:- not violation(_, _, _).

#show violation/3.
#show blocked/2.
#show admin/1.
#show owner/2.

The pattern

One written truth

The spec, as executable rules, commented with the code it mirrors and the bug it guards. Violations are derived atoms carrying enough arguments to be diagnostic. A clean world prints nothing at all.
Independent translations of what the code does

Translate from the SQL and the middleware, never by copying the spec rules. A diff is only meaningful between two separate derivations. Model the composed behaviour: an authorisation layer returning 401 is part of the implementation even though no query expresses it.
Both directions of violation

A leak is something shown that should be hidden. An over-filter is something hidden that should be shown. Both are regressions, and a checker that only looks for one will pass on the day the other happens.
Bounded search instead of extracted facts

Replace the extraction with choice rules that generate every small world, then demand a disagreement. SAT gives a breaking scenario. UNSAT is a proof of parity up to that bound, and worlds of three users and two threads are enough to find real bugs. Be ready for the volume: the program above has several thousand models, every one of them a witness to the same underlying bug, dressed in different irrelevant choices, because every free combination of the atoms the bug does not touch counts as another world. That is not noise, it is the shape of the space, and it is why the minimisation note in the optimisation chapter matters here: minimise the size of the world and the solver hands you the one-user, one-thread version a person can read.
An oracle against the live system

The same rules, with facts extracted from the real database and from calling the real endpoints. Fail CI on any violation atom. This is where the spec stops being a document and starts being a test.

extractors

Temporal predicates drift

A ban with an expiry is only a ban while it is unexpired. An extractor that forgets the WHERE banned_until > now() clause will keep hiding users who were reinstated, and the checker will agree with it. Take every snapshot from the same clock, once.

scope

Facts must be scoped

An extraction that pulls the whole table will fail on leftover data from an unrelated test. Seed and sample deliberately, and make the scope part of the extraction rather than something the test remembers to do.

cardinality

Know how many values an attribute has

1 { val(C, V) : dom(C, V) } 1 assumes one value per entity. Encoding a multi-valued attribute that way fabricates contradictions, and a fabricated contradiction is a false proof, which is the worst thing a verifier can produce.

the meta test

Watch it fail once

Reintroduce a known bug and demand that the checker goes red. A checker you have never seen fail may be validating nothing, and there is no way to tell by reading it.

.decl character(name: symbol, race: symbol, age: number)

Souffle, on one page

The third engine worth knowing, its whole syntax, and the four features it has that neither Nemo nor clingo does.

Souffle came out of Oracle Labs and takes a different route to speed: it compiles your Datalog into parallel C++ and then compiles that. For a large static analysis run repeatedly over the same shape of data, this wins decisively. It is the engine behind Doop, and it is the one to reach for when the program is fixed and the data is enormous.

Everything here is the material from the original guide, corrected and extended into programs that compile.

lotr.dl

// The dataset and rules from the original guide, corrected and extended.
// Run: mkdir -p out && souffle -D out lotr.dl
// souffle will not create the output directory, and the facts here are
// inline, so no -F is needed.

// 1. Declarations. Souffle is typed, and every relation needs one.
.decl character(name: symbol, race: symbol, age: number)
.decl weapon(owner: symbol, item: symbol, dmg: number)
.decl knows(person_a: symbol, person_b: symbol)

// 2. Facts. This is the extensional database, the part you were given.
character("Frodo", "Hobbit", 50).
character("Sam", "Hobbit", 38).
character("Legolas", "Elf", 2931).
character("Gimli", "Dwarf", 139).
character("Aragorn", "Human", 87).

weapon("Frodo", "Sting", 15).
weapon("Legolas", "Bow", 20).
weapon("Gimli", "Axe", 25).
weapon("Aragorn", "Anduril", 30).

knows("Frodo", "Sam").
knows("Sam", "Aragorn").
knows("Legolas", "Gimli").

// 3. Filtering and projection. The underscore is a wildcard that binds
// nothing, so it can appear as often as you like.
.decl is_hobbit(n: symbol)
is_hobbit(N) :- character(N, "Hobbit", _).
.output is_hobbit(IO=stdout)

// 4. A join. Reusing C_Name in both atoms is the join condition, and there
// is nowhere to write it wrong.
.decl ancient_warrior(name: symbol, item: symbol)
ancient_warrior(C_Name, Item) :-
    character(C_Name, _, Age),
    weapon(C_Name, Item, _),
    Age > 100.
.output ancient_warrior(IO=stdout)

// 5. Recursion, which is the reason to be here at all.
.decl in_network(x: symbol, y: symbol)
in_network(X, Y) :- knows(X, Y).
in_network(X, Y) :- knows(X, Z), in_network(Z, Y).
.output in_network(IO=stdout)

// 6. Negation. The variable is bound positively first, because Souffle
// cannot enumerate the things that do not exist.
.decl unarmed(c: symbol)
unarmed(C_Name) :- character(C_Name, _, _), !weapon(C_Name, _, _).
.output unarmed(IO=stdout)

// 7. Aggregates. The syntax is Var = aggregate Expr : { body }.
.decl weapon_count(owner: symbol, n: number)
weapon_count(Owner, C) :-
    character(Owner, _, _),
    C = count : { weapon(Owner, _, _) }.
.output weapon_count(IO=stdout)

.decl total_damage(total: number)
total_damage(T) :- T = sum Dmg : { weapon(_, _, Dmg) }.
.output total_damage(IO=stdout)

.decl strongest(item: symbol, dmg: number)
strongest(Item, Dmg) :-
    weapon(_, Item, Dmg),
    Dmg = max D : { weapon(_, _, D) }.
.output strongest(IO=stdout)

souffle -D out lotr.dl

$ mkdir -p out
$ souffle -D out lotr.dl
---------------
ancient_warrior
===============
Legolas	Bow
Gimli	Axe
===============
---------------
in_network
===============
Frodo	Sam
Frodo	Aragorn
Sam	Aragorn
Legolas	Gimli
===============
---------------
is_hobbit
===============
Frodo
Sam
===============
...

Where it differs from the rest of this book

	Souffle
Variables	capitalised, as in clingo
Declarations	`.decl` for every relation, with named typed columns
Types	`symbol`, `number`, `unsigned`, `float`, plus strict aliases
Negation	`!` before the atom
Comments	`//` and `/* */`. A `%` comment, valid in both other dialects, is a syntax error here
Aggregates	`C = count : { body }`, which reads mathematically
Directives	no terminating full stop, unlike rules
Output	`.output rel(IO=stdout)` or to a file
Execution	interpreted, or compiled to parallel C++

The four features nothing else here has

These are the reasons to choose Souffle over the other two, and each of them solves a problem this book has otherwise had to work around.

advanced.dl

// The parts of Souffle that no other engine here has.
// Run: souffle -D out advanced.dl

// Strict type aliases. A PersonName cannot be passed where a WeaponName
// belongs, and the compiler says so rather than joining the two silently.
.type PersonName <: symbol
.type WeaponName <: symbol

.decl owns(person: PersonName, item: WeaponName)
owns("Frodo", "Sting").
.output owns(IO=stdout)

// Reading real data. In practice facts come from CSV or SQLite, not from
// the program text, and the file lives in the directory given by -F.
.decl edge(a: number, b: number)
.input edge(IO=file, filename="edges.csv", delimiter=",")

.decl reachable(a: number, b: number)
reachable(A, B) :- edge(A, B).
reachable(A, C) :- edge(A, B), reachable(B, C).
.output reachable(IO=file, filename="reachable.csv")

// Subsumption: delete a tuple that another tuple dominates. This is how you
// keep only the shortest distance to each node instead of every path length,
// and it is what makes single source shortest paths practical here.
.decl min_distance(node: number, dist: number)
min_distance(B, 1) :- edge(1, B).
min_distance(C, D + 1) :- min_distance(B, D), edge(B, C), D < 100.
min_distance(Node, D2) <= min_distance(Node, D1) :- D1 <= D2.
.output min_distance(IO=stdout)

// Components: a parameterised module, instantiated as many times as needed.
// Nothing else in this book has an answer to "I need this graph analysis
// four times over four different edge relations".
.comp Graph {
    .decl edge(u: number, v: number)
    .decl reachable(u: number, v: number)
    reachable(U, V) :- edge(U, V).
    reachable(U, W) :- edge(U, V), reachable(V, W).
}

.init callGraph = Graph
.init typeGraph = Graph

callGraph.edge(1, 2).
callGraph.edge(2, 3).
typeGraph.edge(10, 11).

.output callGraph.reachable(IO=stdout)

// User defined functors call out to C++ for the things logic is bad at.
// The signature is declared here; the implementation is compiled alongside.
.functor jaccard(a: symbol, b: symbol): float
.decl similarity(a: symbol, b: symbol, score: float)
similarity(A, B, S) :- owns(A, _), owns(B, _), A != B, S = @jaccard(A, B).
.output similarity(IO=stdout)

What each one buys

Feature	Solves
Typed declarations	The empty result problem from the types chapter, at compile time. A `PersonName` cannot be passed where a `WeaponName` belongs.
Subsumption	Shortest paths. A rule of the form `dominated <= dominating :- condition` deletes tuples another tuple beats, so the relation keeps only the best per key instead of every candidate.
Components	Repeating a graph analysis over four different edge relations. `.comp` defines a parameterised module and `.init` instantiates it, with inheritance if you want it.
User defined functors	The things logic is bad at. A `.functor` declaration maps to a C++ implementation, so string distance, hashing or numeric work happens where it belongs.

nmo program.rls --trace 'fact(a)'

The wider ecosystem, and where to go next

Which engine for which job, what else exists, and what to read once this book runs out.

Engine	Shape	Good for
Nemo	Rust, bottom up, in memory	Data integration across CSV, RDF, SPARQL and JSON. Existential rules. Fast iteration with no build step.
clingo	Ground and solve, ASP	Search, planning, scheduling, configuration, proofs and counterexamples. Anything with the word optimal in it.
Souffle	Compiles to parallel C++	Large static analysis, repeated over the same rules. Typed relations, subsumption, components.
RDFox	Commercial, in memory, incremental	Live knowledge graphs where base facts change constantly and the derived ones must keep up.
DDlog, Differential Datalog	Incremental over streams, no longer maintained	Recomputing a derivation as inputs change, without redoing it. The reference implementation was archived in 2026 and is read-only, so treat it as a design to learn from rather than a dependency to take. The differential dataflow layer underneath it is alive and is what to build on.
Logica	Compiles rules to SQL	Running Datalog logic against BigQuery or Postgres, where the data already lives.
XTDB, Datomic	Databases with Datalog as the query language	Application development, usually from Clojure.
CozoDB, DuckDB	Embedded, with recursive queries	When you want a database first and rules second.

Nemo, day to day

# Run a program. Exports land where the @export directives say.
nmo program.rls

# Choose the output directory and allow overwriting.
nmo program.rls -D out -o

# Ignore the @export directives and dump every derived predicate. This is
# the flag to reach for while writing rules.
nmo program.rls -e idb

# Parse and evaluate without writing anything, which is the fastest way to
# ask "does this program work at all".
nmo program.rls -e none

# Override a @parameter from the command line.
nmo program.rls --param "minAge=21" --param "region=north"

# Ask why a fact was derived. The answer is a proof tree, and it is the
# single most useful debugging tool the engine has.
nmo program.rls --trace 'reaches("a", "d")'

Habits that make this pleasant

Write the schema of every predicate down

One comment giving the columns in order. Nothing in the language enforces argument order, and a transposed argument produces a program that runs and derives nonsense.
Name the intermediate steps

Intermediate predicates cost nothing and make everything else easier: tracing, exporting, testing, and reading the program in six months.
Check types first when the answer is empty

Bare name against quoted string, integer against double, tagged string against plain. It is the answer more often than every other cause put together.
Keep facts and rules in separate files

So the same rules can run against a small hand written world and against a production extraction. That separation is what makes a rule set testable, and testable rules are the whole argument for writing them down.
Watch your checks fail once

Any rule set used as a check should be shown a world it must reject, before it is trusted with one it should accept.

Where to read next

theory

Foundations of Databases

Abiteboul, Hull and Vianu, free online and known universally as the Alice book. Chapters 12 to 15 are the definitive treatment of Datalog, stratification and fixpoint semantics, and they are more readable than their reputation suggests.

asp

The Potassco guide

The clingo team's own guide, and the reference for the language. Answer Set Solving in Practice is the book length version, and it is the one to read if generate-define-test starts to feel like a real tool.

engines

The engine documentation

Nemo, clingo and Souffle all document things this book has only pointed at, and all three are unusually well written.

applied

Doop and CodeQL

The Doop rule sets are worth reading as an example of what a serious Datalog program looks like at scale. CodeQL shows the same idea productised.

You write down what is true. The engine works out the rest.

What you get

Recursion that is not an afterthought

Joins with nowhere to put a mistake

It always finishes

The engine chooses the order

Two engines, two different questions

Running something

The three parts of every program

The same three questions, three ways

How the engine actually evaluates this

Reading a rule out loud

The four operations

Order does not change the answer

Why it stops

Patterns worth knowing

The two conditions

What negation is for

The trap, stated plainly

The rules around them

What a term can be

The rules of equality

Safety

Stratification

Arity

The parts of a file, in order

The formats

format is not optional in practice

The infix restriction

The functions worth knowing

Two ways to mint an identifier

The six things to check, in order

A type mismatch

An aggregate over the wrong thing

Arity

A built-in that quietly failed

A filter applied straight to an import

@output rather than @export

The two tools

Both directions, always

Running it like a test suite

When the output is large

When the answer is hard to write down

The three additions

Grounding, and why it matters

The same shape, on a real problem

Turning questions into constraints

A larger example

Enumeration modes

Four ways to misread a result

Unexpected UNSAT

A model where you wanted a proof

Grounding that never finishes

Bind from the smallest generator

Put the selective atom first

Read --stats before optimising

Know when to leave

Optima that are not

The two that are harder than they look

The four decisions an extractor makes

Then the rules are the easy part

From an AST

From SQL

From config

From events

Why this shape suits the problem

What the standards call this

The pattern

Temporal predicates drift

Facts must be scoped

Know how many values an attribute has

Watch it fail once

Where it differs from the rest of this book

What each one buys

Habits that make this pleasant

Where to read next

Foundations of Databases

The Potassco guide

The engine documentation

Doop and CodeQL