Transcript Document

Section 9.2 Logic Programming
A logic program is a set of clauses with the restriction that there is exactly one positive
literal in each clause. Such clauses are often called definite clauses.
Example. Let p(x, y) mean x is a parent of y and let g(x, y) mean x is a grandparent of y.
Here are some ways to represent a definition of the grandparent relation.
First-order logic:
x y z (p(x, z)  p(z, y)  g(x, y)).
First-order clause:
g(x, y)  ¬ p(x, z)  ¬ p(z, y).
Logic programming:
g(x, y)  p(x, z), p(z, y).
Prolog:
g(X, Y) :- p(X, Z), p(Z, Y).
A query or goal is a question that asks whether the program infers something.
The something is a sequence of one or more atoms and the question is whether there is a
substitution that can be applied to the atoms so that the resulting atoms are inferred by the
program.
Example. Suppose we have the following little logic program.
p(a, b).
p(b, d).
g(x, y)  p(x, z), p(z, y).
Let g(a, w) be a query. It asks whether a has a grandchild.
If we let q = {w/d}, then g(a, w)q = g(a, d), which says a has a grandchild d.
This follows from the two program facts p(a, b) and p(b, d) and the definition of g.
So g(a, d) is inferred by the program.
1
Formal Representation of a Query
From a formal viewpoint (i.e., first-order predicate calculus) a query is the existential closure
of a conjunction of one or more atoms.
Example. The query g(a, w) is formally represented by w g(a, w). We saw that the
example program infers g(a, w)q = g(a, d) for q = {w/d}. But EG can be applied to g(a, d) to
infer w g(a, w). Therefore the program infers w g(a, w).
Example. The query g(a, w), p(u, w) is formally represented by w u (g(a, w)  p(u, w)). If
we let q = {w/d, u/b}, then (g(a, w)  p(u, w))q = g(a, d)  p(b, d), which follows from the
two example program facts p(a, b) and p(b, d) and the definition of g. So g(a, d)  p(b, d) is
inferred by the program. Now apply EG twice to infer w u (g(a, w)  p(u, w)). Therefore
the program infers w u (g(a, w)  p(u, w)).
Logic Programming Representation of a Query
To see whether a query can be inferred from a program, a resolution proof is attempted.
The premises are the program clauses together with the negation of the query, which can be
written as a clause with only negative literals.
Example. Given the query g(a, w), p(u, w). Its formal meaning is w u (g(a, w)  p(u, w)).
So we negate it and convert it to a clause.
Here are some ways to represent the negation of the query.
First-order logic:
¬ w u (g(a, w)  p(u, w))  w u ¬ (g(a, w)  p(u, w)).
First-order clause:
¬ g(a, w)  ¬ p(u, w).
Logic programming:
 g(a, w), p(u, w).
2
Prolog:
|?- g(a, W), p(U, W).
SLD-resolution is a form of resolution used to execute logic programs. SLD means
selective linear resolution of definite clauses. Select the leftmost atom of goal; Linear (each
resolvant depends of the previous resolvant); and Definite clauses are the clauses of a logic
program.
Example. Given the following little logic program and query, where the clauses are also
listed in first-order form.
Logic Programming Syntax
First-Order Clauses
p(a, b).
p(a, b).
p(b, d).
p(b, d).
g(x, y)  p(x, z), p(z, y). g(x, y)  ¬ p(x, z)  ¬ p(z, y).
The query:
 g(a, w), p(u, w).
¬ g(a, w)  ¬ p(u, w).
The resolution proof:
1. p(a, b)
p(a, b)
P
2. p(b, d)
p(b, d)
P
3. g(x, y)  p(x, z), p(z, y)
g(x, y)  ¬ p(x, z)  ¬ p(z, y)
P
4.  g(a, w), p(u, w)
¬ g(a, w)  ¬ p(u, w)
P
5.  p(a, z), p(z, y), p(u, y)
¬ p(a, z)  ¬ p(z, y)  ¬ p(u, y)
3, 4, R, {x/a, w/y}
6.  p(b, y), p(u, y)
¬ p(b, y)  ¬ p(u, y)
1, 5, R, {z/b}
7.  p(u, d)
¬ p(u, d)
2, 6, R, {y/d}
8. []
[]
2, 7, R, {u/b}
3
QED.
Computation Trees
A computation tree for a query represents all possible ways to satisfy the query. i.e., it
represents all possible refutations by resolution.
The root is the query and a child of a node is a resolvant of the node with a program clause.
The mgus are listed along each branch of the tree.
Computed answers are listed below the leaf of each successful refutation.
Example. Given the following logic
program and query:
p(a, b)
p(c, b)
p(b, d)
g(x, y)  p(x, z), p(z, y)
Query:
 g(w, d)
The computation tree for the query is
pictured.
 g(w, d)
{x/w, y/d}
 p(w, z), p(z, d)
{w/a, z/b}
 p(b, d)
{}
[]
success
w=a
{w/c, z/b}
 p(b, d)
{}
{w/b, z/d}
 p(d, d)
failure
[]
success
w=c
4
Example/Quiz. Given the following logic program and query.
p(a)
p(x)  p(ƒ(x))
p(ƒ(b)).
The query:
 p(y).
Draw several levels of the computation tree for the query.
 p(y)
Solution:
{y/a}
{y/x1}
{y/ƒ(b)}
[]
 p(ƒ(x1))
success
y = a {x2/ƒ(x1)}
{x1/b}
 p(ƒ(ƒ(x1)))
{x3/ƒ(ƒ(x1))}
[]
success
y = ƒ(b)
[]
success
y=b
 p(ƒ3(x1))
infinite branch
5
Logic Programming Examples
Example. Let ex(n, m) mean the execution of p(n), p(n + 1), …, p(m). Write a program for
the predicate ex.
Solution:
ex(n, n)  p(n).
ex(n, m)  n < m, p(n), k is n + 1, ex(k, m).
Example. Suppose we need to construct the set
L = {n | (1 ≤ n ≤ 50) and p(n) is true}.
With Prolog’s setof predicate, we could find the answer with the query
|?- setof(N, (1 =< N, N =< 50, p(N)), L).
Without the setof predicate we need to define a predicate to do the job.
Solution: Assume that the the following query will construct the set L.
|?- set(1, 50, [ ], L).
The third argument, initilized to [ ], will accumulate the set of n for which p(n) is true.
Then we can define the predicate set as follows.
set(Lower, Upper, L, L) :- Lower > Upper.
set(Lower, Upper, L, X) :- p(Lower), N is Lower + 1, set(N, Upper, [Lower | L], X).
set(Lower, Upper, L, X) :- N is Lower + 1, set(N, Upper, L, X).
6