IA: Computational Logic
. Prolog
Achim Blumensath blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Prolog
Prolog
Syntax
A Prolog program consists of a sequence of statements of the form
p(¯s). or p(¯s) ∶− q(¯t), . . . , qn−(¯tn−).
p, qi relation symbols, ¯s, ¯ti tuples of terms.
Semantics
p(¯s) ∶− q(¯t), . . . , qn−(¯tn−).
corresponds to the implication
p(¯s) ← ∃¯y[q(¯t) ∧ ⋅⋅⋅ ∧ qn−(¯tn−)]
where ¯y are all the variables that do not appear in ¯s.
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) ∶− father_of(X, Y).
parent_of(X, Y) ∶− mother_of(X, Y).
sibling_of(X, Y) ∶− parent_of(Z, X), parent_of(Z, Y).
ancestor_of(X, Y) ∶− father_of(X, Z), ancestor_of(Z, Y).
Interpreter
On input
p(¯s), . . . , pn−(¯sn−).
the program finds all values for the variables satisfying the
conjunction
p(¯s) ∧ ⋅⋅⋅ ∧ pn−(¯sn−) .
Example
?- sibling_of(sam, tina).
Yes
?- sibling_of(X, Y).
X = sam, Y = tina
Execution
Input
▸ program Π (set of Horn clauses)
▸ goal φ(¯X) = ψ(¯X) ∧ ⋅⋅⋅ ∧ ψn−(¯X)
Evaluation strategy
▸ transform ¬φ = ¬ψ ∨ ⋅⋅⋅ ∨ ¬ψn− into a clause;
▸ use resolution to check for which values of ¯X the union
Π ∪ {¬φ(¯X)} is unsatisfiable.
Remark
As we are dealing with a set of Horn clauses, we can use linear
resolution. The variant used by Prolog-interpreters is called
SLD-resolution.
SLD-resolution
▸ Current goal: ¬ψ ∨ ⋅⋅⋅ ∨ ¬ψn−
▸ If n = , stop.
▸ Otherwise, find a clause ψ′
→ ϑ, . . . , ϑm− from Π such that ψ
and ψ′
can be unified.
▸ If no such clause exists, backtrack.
▸ Otherwise, resolve them to produce the new goal
σ(¬ϑ) ∨ ⋅⋅⋅ ∨ σ(¬ϑm−) ∨ ¬ψ ∨ ⋅⋅⋅ ∨ ¬ψn− .
(σ is the most general unifier of ψ and ψ′
.)
Implementation
Use a stack machine that keeps the current goal on the stack.
(→ Warren Abstract Machine)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬sibling_of(tina, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬sibling_of(tina, sam)
unify with sibling_of(X, Y) ← parent_of(Z, X) ∧ parent_of(Z, Y)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬sibling_of(tina, sam)
unify with sibling_of(X, Y) ← parent_of(Z, X) ∧ parent_of(Z, Y)
unifier X = tina, Y = sam
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬sibling_of(tina, sam)
unify with sibling_of(X, Y) ← parent_of(Z, X) ∧ parent_of(Z, Y)
unifier X = tina, Y = sam
new goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← mother_of(X, Y)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← mother_of(X, Y)
unifier X = Z, Y = tina
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← mother_of(X, Y)
unifier X = Z, Y = tina
new goal ¬mother_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬mother_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬mother_of(Z, tina), ¬parent_of(Z, sam)
unify with mother_of(sara, john)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬mother_of(Z, tina), ¬parent_of(Z, sam)
unify with mother_of(sara, john)
fails
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬mother_of(Z, tina), ¬parent_of(Z, sam)
unify with mother_of(sara, john)
fails
backtrack to ¬parent_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← father_of(X, Y)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← father_of(X, Y)
unifier X = Z, Y = tina
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(Z, tina), ¬parent_of(Z, sam)
unify with parent_of(X, Y) ← father_of(X, Y)
unifier X = Z, Y = tina
new goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
unify with father_of(peter, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
unify with father_of(peter, sam)
fails
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
unify with father_of(peter, sam)
fails
unify with father_of(peter, tina)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
unify with father_of(peter, sam)
fails
unify with father_of(peter, tina)
unifier Z = peter
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬father_of(Z, tina), ¬parent_of(Z, sam)
unify with father_of(peter, sam)
fails
unify with father_of(peter, tina)
unifier Z = peter
new goal ¬parent_of(peter, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(peter, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(peter, sam)
. . . . . .
goal ¬father_of(peter, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(peter, sam)
. . . . . .
goal ¬father_of(peter, sam)
unify with father_of(peter, sam)
Example
father_of(peter, sam).
father_of(peter, tina).
mother_of(sara, john).
parent_of(X, Y) :- mother_of(X, Y).
parent_of(X, Y) :- father_of(X, Y).
sibling_of(X, Y) :- parent_of(Z, X), parent_of(Z, Y).
Input sibling_of(tina, sam)
goal ¬parent_of(peter, sam)
. . . . . .
goal ¬father_of(peter, sam)
unify with father_of(peter, sam)
new goal empty
Search tree
sibling_of(tina, sam)
parent_of(Z, tina), parent_of(Z, sam)
mother_of(Z, tina), parent_of(Z, sam) father_of(Z, tina), parent_of(Z, sam)
fail parent_of(peter, sam)
success
Caveats
Prolog-interpreters use a simpler (and unsound) form of unification
that ignores multiple occurrences of variables. E.g. they happily unify
p(x, f (x)) with p(f (y), f (y)) (equating x = f (y) for the first x and
x = y for the second one).
Caveats
Prolog-interpreters use a simpler (and unsound) form of unification
that ignores multiple occurrences of variables. E.g. they happily unify
p(x, f (x)) with p(f (y), f (y)) (equating x = f (y) for the first x and
x = y for the second one).
It is also easy to get infinite loops if you are not careful with the
ordering of the clauses:
edge(c,d).
path(X,Y) :- path(X,Z),edge(Z,Y).
path(X,Y) :- edge(X,Y).
produces
?- path(X,Y).
path(X,Z), edge(Z,Y).
path(X,U), edge(U,Z), edge(Z,Y).
path(X,V), edge(V,U), edge(U,Z), edge(Z,Y).
...
Example: List processing
append([], L, L).
append([H|T], L, [H|R]) :- append(T, L, R).
?- append([a,b], [c,d], X).
X = [a,b,c,d]
?- append(X, Y, [a,b,c,d])
X = [], Y = [a,b,c,d]
X = [a], Y = [b,c,d]
X = [a,b], Y = [c,d]
X = [a,b,c], Y = [d]
X = [a,b,c,d], Y = []
Example: List processing
reverse(Xs, Ys) :- reverse_(Xs, [], Ys).
reverse_([], Ys, Ys).
reverse_([X|Xs], Rs, Ys) :- reverse_(Xs, [X|Rs], Ys).
reverse([a,b,c], X)
reverse_([a,b,c], [], X)
reverse_([b,c], [a], X)
reverse_([c], [b,a], X)
reverse_([], [c,b,a], X)
X = [c,b,a]
Example: Natural language recognition
sentence(X,R) :- noun(X, Y), verb(Y, R).
sentence(X,R) :- noun(X, Y), verb(Y, Z), noun(Z, R).
noun_phrase(X, R) :- noun(X, R).
noun_phrase([’a’ | X], R) :- noun(X, R).
noun_phrase([’the’ | X], R) :- noun(X, R).
noun([’cat’ | R], R).
noun([’mouse’ | R], R).
noun([’dog’ | R], R).
verb([’eats’ | R], R).
verb([’hunts’ | R], R).
verb([’plays’ | R], R).
Cuts
Control backtracking using cuts:
p ∶− q, q, !, q, q.
When backtracking across a cut !, direktly jump to the head of the
clause.
Example
s ← p
s ← t
p ← q, q, !, q, q
p ← r
r
q
q
q
s
p t
q, q, !, q, q r fail
q, !, q, q success
!, q, q
q
fail
Negation
Problem
If we allow negation, the formulae are no longer Horn and
SLD-resolution does no longer work.
Possible Solutions
▸ Closed World Assumption
If we cannot derive p, it is false (Negation as Failure).
▸ Completed Database
p ← q, . . . , p ← qn is interpreted as the stronger statement
p ↔ q ∨ ⋅⋅⋅ ∨ qn.
Warning
Negation as Failure, which is implemented in Prolog, does not behave
like real negation. The Completed Database approach is much better
behaved, but harder to implement.
Examples
Being connected by a path of non-edges:
q(X,X).
q(X,Y) :- q(X,Z), not(p(Z,Y)).
Implementing negation using cuts:
not(A) :- A, !, fail.
not(A).
Some cuts can be implemented using negation:
p :- a, !, b. p :- a, b.
p :- c. p :- not(a), c.
Databases
Databases
Definition
A database is a set of relations called tables.
Example
flight from to price
LH Prague Frankfurt 
OA Vienna Warsaw 
UA London Washington 
...
Formal Definitions
We treat a database as a structure A = ⟨A, R, . . . , Rn⟩ with
▸ universe A containing all entries and
▸ one relation Ri ⊆ A × ⋅⋅⋅ × A per table.
The active domain of a database is the set of elements appearing in
some relation.
Example
In the previous table, the active domain contains:
LH, OA, UA, , , ,
Prague, Frankfurt, Vienna, Warsaw, London, Washington
Queries
A query is a function mapping each database to a relation.
Example
Input: database of direct flights
Output: table of all flight connections possibly including stops
In Prolog: database flight, query connection.
flight(’LH8302’, ’Prague’, ’Frankfurt’, 240).
flight(’OA1472’, ’Vienna’, ’Warsaw’, 300).
flight(’UA0870’, ’London’, ’Washington’, 800).
connection(From, To) :- flight(X, From, To, Y).
connection(From, To) :flight(X,
From, T, Y), connection(T, To).
Relational Algebra
Syntax
▸ basic relations
▸ boolean operations ∩, ∪, ∖, All
▸ cartesian product ×
▸ selection σij
▸ projection πu...un−
Examples
▸ π,(R) = {(b, a) (a, b) ∈ R}
▸ π,(σ,(E × E)) = {(a, c) (a, b), (b, c) ∈ E }
Relational Algebra
Syntax
▸ basic relations
▸ boolean operations ∩, ∪, ∖, All
▸ cartesian product ×
▸ selection σij
▸ projection πu...un−
Examples
▸ π,(R) = {(b, a) (a, b) ∈ R}
▸ π,(σ,(E × E)) = {(a, c) (a, b), (b, c) ∈ E }
Join
R ⋈ij S ∶= σij(R × S)
Expressive Power
Theorem
Relational Algebra = First-Order Logic
Expressive Power
Theorem
Relational Algebra = First-Order Logic
Proof
(≤)
R∗
∶= R(x, . . . , xn−)
(s ∩ t)∗
∶= s∗
∧ t∗
(s ∪ t)∗
∶= s∗
∨ t∗
(s ∖ t)∗
∶= s∗
∧ ¬t∗
All∗
∶= true
(s × t)∗
∶= s∗
(x, . . . , xm−) ∧ t∗
(xm, . . . , xm+n−)
σij(s)∗
∶= s∗
∧ xi = xj
πu,...,un− (s)∗
∶= ∃¯y[s∗
(¯y) ∧ ⋀
i<n
xi = yui
]
Expressive Power
Theorem
Relational Algebra = First-Order Logic
Proof
(≥)
R(xu , . . . , xun− )∗
∶= π¯v(R × All) vi ∶=
⎧⎪⎪
⎨
⎪⎪⎩
k if i = uk
n otherwise
(xi = xj)∗
∶= σij(All × ⋅⋅⋅ × All)
(φ ∧ ψ)∗
∶= φ∗
∩ ψ∗
(φ ∨ ψ)∗
∶= φ∗
∪ ψ∗
(¬φ)∗
∶= All × ⋅⋅⋅ × All ∖ φ∗
(∃xiφ)∗
∶= π,...,i−,n,i+,...,n−(φ∗
× All)
Datalog
Simplified version of Prolog developped in database theory:
▸ no function symbols,
▸ no cut, no negation, etc.
A datalog program for a database A = ⟨A, R, . . . , Rn⟩ is a set of Horn
formulae
p(¯X) ← q,(¯X, ¯Y) ∧ ⋅⋅⋅ ∧ q,m (¯X, ¯Y)
⋮
pn(¯X) ← qn,(¯X, ¯Y) ∧ ⋅⋅⋅ ∧ qn,mn (¯X, ¯Y)
where p, . . . , pn are new relation symbols and the qij are either
relation symbols from A, possibly negated, or one of the new
symbols pk (not negated).
Datalog queries
The query defined by a datalog program
p(¯X) ← q,(¯X, ¯Y) ∧ ⋅⋅⋅ ∧ q,m (¯X, ¯Y)
⋮
pn(¯X) ← qn,(¯X, ¯Y) ∧ ⋅⋅⋅ ∧ qn,mn (¯X, ¯Y)
maps a database A to the relations p, . . . , pn defined by these
formulae.
Evaluation strategy
▸ Start with empty relations p = ∅, . . . , pn = ∅.
▸ Apply each rule to add new tuples to the relations.
▸ Repeat until no new tuples are generated.
Note
The relations computed in this way satisfy the Completed Database
assumption.
Example
path(X, Y) ← edge(X, Y)
path(X, Y) ← path(X, Z) ∧ path(Z, Y)
A stage 
Example
path(X, Y) ← edge(X, Y)
path(X, Y) ← path(X, Z) ∧ path(Z, Y)
A stage 
Example
path(X, Y) ← edge(X, Y)
path(X, Y) ← path(X, Z) ∧ path(Z, Y)
A stage 
Example
path(X, Y) ← edge(X, Y)
path(X, Y) ← path(X, Z) ∧ path(Z, Y)
A stage 
Example: Arithmetic
Add(x, y, z) ← y =  ∧ x = z
Add(x, y, z) ← E(y′
, y) ∧ E(z′
, z) ∧ Add(x, y′
, z′
)
Mul(x, y, z) ← y =  ∧ z = 
Mul(x, y, z) ← E(y′
, y) ∧ Add(x, z′
, z) ∧ Mul(x, y′
, z′
)
stage  ∅
Example: Arithmetic
Add(x, y, z) ← y =  ∧ x = z
Add(x, y, z) ← E(y′
, y) ∧ E(z′
, z) ∧ Add(x, y′
, z′
)
Mul(x, y, z) ← y =  ∧ z = 
Mul(x, y, z) ← E(y′
, y) ∧ Add(x, z′
, z) ∧ Mul(x, y′
, z′
)
stage  ∅
stage  (k, , k)
Example: Arithmetic
Add(x, y, z) ← y =  ∧ x = z
Add(x, y, z) ← E(y′
, y) ∧ E(z′
, z) ∧ Add(x, y′
, z′
)
Mul(x, y, z) ← y =  ∧ z = 
Mul(x, y, z) ← E(y′
, y) ∧ Add(x, z′
, z) ∧ Mul(x, y′
, z′
)
stage  ∅
stage  (k, , k)
stage  (k, , k), (k, , k + )
Example: Arithmetic
Add(x, y, z) ← y =  ∧ x = z
Add(x, y, z) ← E(y′
, y) ∧ E(z′
, z) ∧ Add(x, y′
, z′
)
Mul(x, y, z) ← y =  ∧ z = 
Mul(x, y, z) ← E(y′
, y) ∧ Add(x, z′
, z) ∧ Mul(x, y′
, z′
)
stage  ∅
stage  (k, , k)
stage  (k, , k), (k, , k + )
stage  (k, , k), (k, , k + ), (k, , k + )
Example: Arithmetic
Add(x, y, z) ← y =  ∧ x = z
Add(x, y, z) ← E(y′
, y) ∧ E(z′
, z) ∧ Add(x, y′
, z′
)
Mul(x, y, z) ← y =  ∧ z = 
Mul(x, y, z) ← E(y′
, y) ∧ Add(x, z′
, z) ∧ Mul(x, y′
, z′
)
stage  ∅
stage  (k, , k)
stage  (k, , k), (k, , k + )
stage  (k, , k), (k, , k + ), (k, , k + )
⋯
stage n (k, , k), (k, , k + ),..., (k, n − , k + n − )
⋯
Complexity
Theorem
For databases A = ⟨A, ¯R, ≤⟩ equipped with a linear order ≤, a query Q
can be expressed as a Datalog program if, and only if, it can be
evaluated in polynomial type.