Transcript document

Computational Logic: today’s
menu



1
Practicalities
Clause form of first-order logic: syntax and
semantics, clause instance, universe of
discourse, interpretations, resolution, unification,
consistency of a set of clauses. Syntactic
(resolution-based) vs. semantic (reasoning on
interpretations) proofs of (in)consistency.
Logic Programs (based on Horn clause form):
general properties, syntax, declarative
semantics, procedural semantics.
Practicalities



Lab: this Fri @ 3:30 in ASB 9840
Sicstus runs on CSIL; license only covers
installation on SFU owned systems.
However, students can run Sicstus from their
home by ssh into any CSIL workstations via
fraser.sfu.ca. i.e.
1) ssh to fraser.sfu.ca
2) ssh to any of the CSIL Linux workstations, as
shown on
http://www.cs.sfu.ca/CC/CSILPC/CSIL_Layout.pdf
2
Some Definitions
Instance of an expression: a (usually more
specific) form of that expression, obtained by
applying a substitution to the expression(i.e., by
assigning terms to variables). E.g.:
Clause C: ancestor(X,Z):- parent(X,Y),
ancestor(Y,Z).
Substitution : {X=mother(adam),Y=adam}
Instance C:
ancestor(mother(adam)),Z):parent(mother(adam),adam),
ancestor(adam,Z).

3
Clause form: Building blocks
Syntax
Semantics
Predicate
p(t1,…,tn), n>=0
states that the relation
called p holds among
the individuals called ti
=====================================
Term: either an
denotes an individual
- atom (constant or #)
in the universe
- variable
- structure f(t1,…,tm)
- (or functional expression)
4
Use of functional expressions
loves(mother(X),X).
?- loves(Who,frankenstein).
Who will UNIFY with mother(frankenstein),
which never evaluates: it simply stands, as is,
for the individual “mother of frankenstein”
MORALE: Only one name is allowed for each
individual (NO SYNONYMS!)
5
General vs. Horn Clause Form
Syntax
Semantics
General Clause Form
h1,…hn:- b1,…,bm.
For all variables
in the clause,
(h1 or…or hn) if (b1 and…bm).
Horn Clause Form (at most one conclusion)
RULE:
For all variables in the clause,
h is T if b1 and…bm are all T
h:- b1,…,bm.
,
6
Horn Clauses: two meanings
Syntax
Semantics
Horn Clause Form (at most one conclusion)
RULE:
h:- b1,…,bm.
Declarative meaning: For all
variables in the clause,
h is T if b1 and…bm are all T
Procedural meaning: To solve
an instance of h, solve b1 and…bm affected by
the same substitutions which gave the instance.
7
Horn clause’s special cases
Syntax
Semantics
(D= declarative interpretation,
P= procedural interpretation)
FACT: Condition-less clause (only a head- no body)
h.
D: For all variables in the clause,
h is unconditionally true
P: All instances of h are trivially solved
QUERY: Conclusion-less clause
?- b1,…,bm.
D: For all variables in the clause,
not(b1 and…bm), or equivalently,
For NO variables in the clause, b1 and…bm
P: Find an instance of the body which
solves all its conjoints, or say “no” if they can’t be solved.
8
Clause Resolution in Prolog
CLAUSE 1:
h:- b1,…,bm.
CLAUSE2:
?- q1, q2 …, qn.
1. Find a substitution that unifies h with q1
2. Apply that same substitution to
?- b1,…,bm,q2, …, qn.
You obtain the resolvent of both clauses.
9
Proof by refutation, or
contradiction- the intuition


PROGRAM:
p(mary).
QUERY:
?- p(X).
(p(mary) is true)
(there is no value of X for which
p(X) is true)
Proof by contradiction: Assume that there is no
value of X for which p(X) is true. If the resulting
set of clauses is inconsistent, conclude there is:
the value of X which makes the set inconsistent.
10
Resolving our fact with our query
1. Find a substitution that unifies the head in one
with a body item in the other:
{X=mary}
2. Generate the resolvent: we get the empty
clause (no conditions, no conclusion). And the
empty clause is inherently contradictory. The
contradiction came from assuming there is no
value for X that satisfies p(X). Therefore our
assumption is wrong, and the counterexample
that proves it wrong is precisely X=mary. In
other words, there exists an X (namely, X=mary)
satisfying p(X).
11
Morale
-
-
That’s why procedurally, a query may be viewed
as a request for Prolog to find values for the
variables(*) (if such exist) that make the body of
a query true (i.e., that make the “query” itself
false- since the query reads not (b1,…bn), or
modulo notation, ?- b1,…,bn).
If we can apply resolution repeatedly on our
query until we generate the empty clause, we’ve
proved that the query’s body does have values
for its variables which makes it true: those that
led to contradiction, or the empty clause.
(*) These values are obtained through composition of all
substitutions used in the process
12
Syntactic proof of inconsistency

13
For the assignment, be sure to provide, as well
as a semantic proof of inconsistency (i.e.,
reasoning on possible interpretations), a
syntactic one (i.e., through resolution): resolve
the query with some clause in the program
whose head matches the first item in the query,
and repeat until the empty clause is generated.
Generating the empty clause through resolution
proves that the set of clauses is inconsistent.
Logic Program= description of
knowledge in terms of:
- Facts:
- Rules:
- Queries:
p.
p:- p1, p2, …, pn.
?- q1, q2 …, qm.
“.”, “:-” and “?-” stand for “if”,
“,” means “and”
p, pi and qi are predicates-- of the form
pred(t1,…,tr).
ti are terms-- either atoms (constants or numbers),
variables, or functional expressions (of the form
f(t1,…,ts))
14
Prolog: based on Horn clauses
Relational
 No explicit types or classes
 High expressiveness: each program line has its
own meaning
 Ideal for prototyping
 Recursiveness, automatic inference, nondeterminism, unification (two-way matching)
---------: features not present in functional
programming

15
Definition: Herbrand Universe

Universe of Discourse, or Herbrand Universe
(given a set of clauses): the set of all variablefree terms that can be built from the predicates
and function symbols occurring in the set of
clauses. Example 1- given the set of clauses S1:
ancestor(X,Z):- parent(X,Y),
ancestor(Y,Z).
ancestor(X,Z):- parent(X,Z).
parent(adam,abel).
parent(adam,cain).
What’s the universe of discourse for S1?
H(S1)= {adam,abel,cain}
16
Example 2- an infinite Herbrand
Universe
S2:
number(0).
number(s(X)):- number(X).
H(S2)= {0, s(0), s(s(0)), …}
N.B.:
 If there are no constants in your set of clauses
(this will in practice rarely happen) you need to
add an arbitrary one into its Herbrand universe
 As soon as you use any functional expression
as an argument of a predicate, the universe
becomes infinite.
17
Definitions

Interpretation: any assignment:


To each term, of an individual in the universe
to each n-ary predicate symbol in the set of
clauses, of an n-ary relation over the
universe.
To specify an interpretation: specify its
effect on the truth or falsity of variable-free
predicates.
18
Example: recall S2
number(0).
number(s(X)):- number(X).
H(S2)= {0,s(0),s(s(0)),…} (Herbrand Universe)
Predicates
I1
number(0)
T
number(s(0))
T
number(s(s(0)))
T
number(s(s(s(0)))) T
…..
…
…..
…
19
I2
F
T
T
T
…
…
I3
T
F
T
T
…
…
I4
T
T
F
T
…
…
…
T
T
T
F
T
…
…
…
…
…
Definitions
A variable-free (ground) clause is true in an
interpretation I  a) whenever all its conditions
are T in I, at least one of its conclusions is T in I,
or equivalently,
 b) at least one of its
conditions is false in I or at least one of its
conclusions is T in I.
Example: mortal(socrates):human(socrates).
is T in any interpretation in which mortal(socrates)
is T, and also in any interpretation in which
human(socrates) is F.

20
Definitions



21
A set of clauses S is inconsistent  it is not
consistent.
A set of clauses S is consistent  all its
clauses are T in some interpretation of S.
A clause is T in an interpretation I of a set of
clauses S  every variable-free instance of the
clause obtained by replacing variables by terms
from H(S) is true in I. Otherwise the clause is F
in I.
Semantic proof of consistency:

Given a set of clauses, e.g.
S3:
(1) human(socrates).
(2) snores(X):- human(X).
Is there an interpretation in which all its clauses
are true? (If there is at least one, the set is
consistent; if there are none, it is inconsistent)
22
Answer
YES, there is: the one that assigns the value T
both to human(socrates) and to
snores(socrates). This interpretation satisfies
clause 1) (which is already ground) and also the
only possible ground instance of 2), namely:
snores(socrates):- human(socrates).
Therefore, in this interpretation, all ground
instances of the set of clauses are T, and
therefore, all its clauses are T. S3 is consistent.
23
The same semantic proof, in stepby-step detail, for finite universes
1. Determine the Herbrand universe of your set of
clauses. In our example, H(S3)={socrates}
2. List all ground instances (i.e., instances with NO
variables) of the predicates. We have only two
predicates (human/1, snores/1), and H has only
one element , so all ground instances of the
predicates are, in our case:
human(socrates), snores(socrates).
3. List all posible interpretations of these ground
instances.
24
Result of step 3 for our example
All possible interpretations (I1, I2, I3, I4):
I1
I2
I3
I4
25
human(socrates)
T
T
F
F
snores(socrates)
T
F
T
F
Intuitively
A set of clauses represents our knowledge about
some world- usually what we intend to represent
is the “real” world, or some subset thereof.
The possible interpretations of that knowledge are
the possible worlds in which we can reason
about that knowledge.
In our example, we have four possible worlds: in
one of these worlds, Socrates is both human
and snores, in another one he is human but
does not snore, etc.
26
Steps of the semantic proof
(cont.)
4. List all ground instances of each clause.
In our example, we have:
human(socrates).
snores(socrates):- human(socrates).
5. Add these to your table, and calculate their truth
values in each of the interpretations listed:
27
Result for step 5 in our example:
( We now note human=hu, socrates=s, snores=sn)
INTERPRETs.
I1
I2
I3
I4
28
hu(s) sn(s)
T
T
T
F
F
T
F
F
TRUTH VALUE OF CLAUSE
INSTANCES IN EACH INTER.
hu(s). sn(s):- hu(s).
T
T
T
F
F
T
F
T
Detailed steps of the semantic
proof (cont.)
6. Interpret these results in the light of the definitions
given:
S3 is consistent, since there is an interpretation
(namely, I1) satisfying all variable-free instances of
its clauses-- i.e., satisfying all its clauses
N.B. For proving consistency, we just need to provide
one interpretation that makes all clauses true. For
proving inconsistency, we have to show that NO
interpretation does. Either we list them all (if small
enough) or we reason about truth values , as we
exemplify next.
29
If the universe is infinite or too big
A proof by enumeration becomes impossible for
clauses with infinite or huge Herbrand
universes. In this case, just show one
interpretation that satisfies all clauses (N.B. this
is also always an option for clauses with small
universes- we just went through detailed stepby-step for studying purposes).
E.g. to prove that S2 is consistent (transparency
19), we show that in interpretation I1, in which all
elements of H(S2) are T, both clauses of S2 are
T. Therefore there is an interpretation (I1) in
which all clauses of S2 are T.

30
Semantic proof of inconsistency:
S4: (1) human(bob).
(2) snores(X):- human(X).
(3) ?-snores(bob).
In any interpretation satisfying (1),
human(bob) must be T (4).
In any interpretation satisfying (1) and (2), all
instances of (2) must be T; in particular the
instance with X=bob:
snores(bob):- human(bob) must be T (5). And
snores(bob) must be T (6), because of (4) and (5).
In any interpretation satisfying (3),
snores(bob) must be F (7).

31
Semantic proof of inconsistency
(cont.)
If an interpretation existed satisfying (1), (2)
and (3) simultaneously, it would have to
satisfy both (6) and (7). But this is
impossible: snores(bob) cannot be both T
and F.
Therefore, no interpretation exists which can
simultaneously satisfy all three clauses in
S4. This set is inconsistent.
32
More detail about matching
(unifying) two terms:
-
-
-
-
33
If both are constants or numbers: they match
<=> they are the same constant or the same
number
If one is a variable: they always match, by
instantiating the variable to the other term.
If they are complex terms, they match <=> they
have the same functor and all their
corresponding arguments match
Two terms match <=> it follows from the above
that they do.
Remember to study one chapter
per night of the online notes:
http://www.learnprolognow.org/
(Learn Prolog now! By Blackburn et al.)

(you should have done four chapters by
now)
Do all exercises as you go along, and run
them.
34
Today’s question
1) Show an instance of the clause:
grandparent(X,Y):- parent(X,Z),
parent(Z,Y).
which can be used to resolve this clause with the
query
 ?- grandparent(mary,W).
2) Show the substitution used to obtain your
instance
3) Show the resolvent of both clauses.
35