Transcript Document

Negation: Declarative Interpretation
- An overview
• First Order Formulas and Logical Truth
• Completion of Programs
• SLDNF-resolution: Soundness and restricted completeness
• Extended Consequence Operator
• Standard Models
[Lloy87] J.W. Lloyd, Foundations of Logic Programming, Second Extended Edition,
Springer, 1987.
[ApBo94] Krzysztof Apt and Roland Bol, Logic Programming and Negation: A Survey,
Journal of Logic Programming, 19/20: 9-71, 1994.
30 October 2005
Foundations of Logic and Constraint Programming
1
First-Order Formulas
Given ranked alphabets F and  for function and predicate symbols,
respectively, and a set V of variables, the set of
(first-order) formulas (over , F and V ) is inductively defined as follows:

If atom A  TB  ,F,V , then A is a formula

If G1 and G2 are formulas, then G1 , G1  G2 (written G1, G2 ), G1  G2,
G1  G2 and G1  G2 are formulas

If G is a formula and x  V, then x G and x G are formulas
30 October 2005
Foundations of Logic and Constraint Programming
2
Extended Notion of Logical Truth (1)
Given a formula G, and interpretation I with domain D, and a state s : V → D:
G is true in I under s , written I |=s G :

I |=s p(t1, ..., tn) : s(t1), ... , s(t1)  pI

I |=s G : I |s G

I |=s G1  G2 : I |=s G1 and I |=s G2

I |=s G1  G2 : I |=s G1 or I |=s G2

I |=s G1 G2 : if I |=s G2 then I |=s G1

I |=s G1 G2 : I |=s G2 iff I |=s G1

I |=s xG : for every d  D: I |=s’ G

I |=s xG : for some d  D: I |=s’ G
where s’ : V → D with s’(x) = d and s’(y) = s (y) for every y  V – {x}
30 October 2005
Foundations of Logic and Constraint Programming
3
Extended Notion of Logical Truth (2)
Given a formula G, sets of formulas S and T, and interpretation I ,
and where x1, ..., xk are the variables occurring in G

 x1, ..., xk G is the universal closure of G (abbreviated to G)

I |= G : I |=s G for every state s

G is true in I (or I is a model of G), written I |= G : I |= G

I is a model of S, written I |= S : I |=G for every G  S
•
T is a semantic (or logical) consequence of S written S |= T :
every model of S is a model of T ( I: I |= S implies I |= T)
30 October 2005
Foundations of Logic and Constraint Programming
4
No Negative Consequences of (Extended) Programs (1)
Consider program Pmem:
member(x,[x|y]) 
member(x,[y|z])  member(x, z)
- Then, e.g
Pmem |= member(a, [a,b]) and Pmem | member(a, [ ]).
- But also, Pmem | member(a, [ ]) since
HB {member},{|, [ ], a} |= Pmem and HB {member},{|, [ ], a} | member(a, [ ]).
Nevertheless, the SLDNF tree of Pmem  {member(a, [ ])} is successful
member(a,[])
□
success
member(a,[])
failure
30 October 2005
Foundations of Logic and Constraint Programming
5
No Negative Consequences of (Extended) Programs (2)
Problem:
For every extended program P, the corresponding Herbrand Base is a model.
-
Hence, there is no negative ground literal A as a logical consequence of P.
-
But SLDNF tree of Pmem  {A }, may be successful ! (?)
Hence, is SLDNF-resolution sound? What does soundness means?
Solution:
Strengthen P by completion (“replace implication by “equivalences”) to
comp(P) and compare SLDNF-resolution and comp(P), instead of P!
30 October 2005
Foundations of Logic and Constraint Programming
6
Completed Definitions (Example 1)
P:
happy  snow, holidays
happy  sun
snow  cold, precipitation
cold 
precipitation 
Whereas P |= precipitation, cold, snow
comp(P):
% the least Herbrand Model
happy  ( snow, holidays )  sun
snow  cold, precipitation
cold  true
precipitation  true
holidays  false
sun  false
comp(P) |= precipitation, cold, snow,  holidays,  sun,  happy
30 October 2005
Foundations of Logic and Constraint Programming
7
Completed Definitions (Example 2)
P: member(x,[x|y]) 
member(x,[y|z])  member(x,z)
disjoint([],x) 
disjoint([x|y],z)   member(x,z), disjoint(y,z)
comp(P): x1 x2 member(x1,x2) 
 x,y (x1 = x, x2 = [x|y]) 
 x,y,z (x1 = x, x2 = [y|z], member(x,z))
x1 x2 disjoint(x1,x2) 
 x (x1 = [], x2 = x) 
 x,y,z (x1 = [x|y], x2 = z,
member(x,z), disjoint(y,z))
( plus the standard axioms for equality and inequality)
Then, e.g. comp(p) |= member(a,[a,b]), member(a,[ ]), member(a,[b,c])
30 October 2005
Foundations of Logic and Constraint Programming
8
Completion (1)
-
The completion of extended program P (denoted by comp(P)), is the set of
formulas constructed from P by the following 6 steps:
1.
Associate with every n-ary predicate symbol p a sequence of pairwise distinct
variables x1, ... , xn which do not occur in P.
2.
Transform each clause c = p(t1, ... , tn)  B into
p(x1, ... , xn)  x1, = t1, ... , xn, = tn, B
3.
Transform each resulting formula p(x1, ... , xn)  G into
p(x1, ... , xn)   z G
where z is a sequence of the elements of Vars(c).
30 October 2005
Foundations of Logic and Constraint Programming
9
Completion (2)
4.
For every n-ary predicate symbol p, let
p(x1, ... , xn)   z1 G1 ,
...
, p(x1, ... , xn)   zm Gm
be all implications obtained in step 3 (m  0).
4.a) If m >0, then replace these by the formula
 x1, ... , xn p(x1, ... , xn)   z1 G1  . . .   zm Gm
(if some Gi is empty, replace it by true.)
4.b) If m = 0, i.e predicate p had no defining clause, then add the formula
 x1, ... , xn p(x1, ... , xn)  false.
30 October 2005
Foundations of Logic and Constraint Programming
10
Completion (3)
5.
Add the standard axioms of equality
5.1  [ x = x]
% reflexivity
5.2  [ x = y → y = x ]
% simetry
5.3  [ x = y , y = z → x = z ]
% transitivity
5.4  [ xi = y → f(x1, ..., xi, ... , xn) = f(x1, ..., y, ... , xn) ]
% substitutivity
5.5  [ xi = y → p(x1, ..., xi, ... , xn)  p(x1, ..., y, ... , xn) ] % substitutivity
6.
Add the standard axioms of inequality
6.1  [ x1  y1 ...  xm  ym → f(x1, ..., xi, ... , xn)  f(y1, ..., yi, ... , yn) ]
6.2  [ f(x1, ..., xi, ... , xn)  g(y1, ..., yi, ... , yn) ]
(when f  g )
6.3  [ x  t ] (when x is a proper subterm of t)
–
Notice that axioms 6.1 to 6.3 are a restriction of FO equality to the UNA
(Unique Names Assumptiom) – “different names denote different entities”
30 October 2005
Foundations of Logic and Constraint Programming
11
Soundness of SLDNF-Resolution
Given extended program P, extended query Q and substitution q:

q | var(Q) is a correct answer substitution of Q : comp(P) |= Q q

Qq is a correct instance of Q : comp(P) |= Q q
Theorem (Lloyd, 1987)
If there exists a successful SLDNF-derivation of P  {Q} with CAS q, then
comp(P) |= Q q.
Corollary (Lloyd, 1987)
If there exists a successful SLDNF-derivation of P  {Q}, then
comp(P) |= Q.
30 October 2005
Foundations of Logic and Constraint Programming
12
Incompleteness of SLDNF (Inconsistency)
P:
p  p
Thus, comp(P)  { p  p } “=“ { false }
Hence,

comp(p) |= p and comp(p) |=  p
In this case comp(P) is inconsistent, as it has no model, since for
every I, I | comp(P)
In this case of inconsistency, SLDNF-resolution is incomplete, since there is
neither a successful SLDNF-derivation for P  {p}, nor for P  { p},
30 October 2005
Foundations of Logic and Constraint Programming
13
Incompleteness of SLDNF (Non Strictness)
P:
p  q
p  q
q  q
Thus, comp(P)  { p  q   q, q q } “=“ { p  true }
Hence,
comp(p) |= p.
In this case, of non-strictness (p depends on q both evenly and oddly, see later),
SLDNF-resolution is incomplete, since there is no successful SLDNF-derivation for
P  {p}.
Notice that in the absence of one of the first two clauses, there would be no
incompleteness, since p  true would not be in comp(P).
30 October 2005
Foundations of Logic and Constraint Programming
14
Incompleteness of SLDNF (Floundering)
P:
p(x)   q(x)
Thus, comp(P)  { x1 p(x1)   x (x1 = x,  q(x)) ,  x1 q(x1)  false } “=“
{ x1 p(x1)  true ,  x1 q(x1)  false }
Hence,
comp(p) |=  x1 p(x1) .
In this case, of floundering, SLDNF-resolution is incomplete, since there is no
successful SLDNF-derivation for P  {p(x1)}
Note: SLDNF blocks query  q(x), contrary to Prolog. Prolog is not incomplete in
this case, but for the wrong reasons!
30 October 2005
Foundations of Logic and Constraint Programming
15
Incompleteness of SLDNF (Unfairness)
P:
r  p, q
p  p
Thus, comp(P)  { r  p, q , p  p, q  false } “=“
{r  false , q  false }
Hence,
comp(P) |=  r .
In this case, SLDNF-resolution might be incomplete, since there is no successful
SLDNF-derivation for P  { r} when the leftmost selection rule (as in Prolog) is
adopted (unfairness of the selection rule).
30 October 2005
Foundations of Logic and Constraint Programming
16
Dependency Graphs
A dependency graph Dp of an extended program P
:
directed graph with labelled edges, where

The nodes are the predicate symbols of P

The edges are either positive (labelled +) or negative (labelled -);

p →+ q edge in Dp :
P contains a clause p(s1, ..., sm)  L, q( t1, .., tn), R

p →- q edge in Dp :
P contains a clause p(s1, ..., sm)  L,  q( t1, .., tn), R
30 October 2005
Foundations of Logic and Constraint Programming
17
Strict, Hierarchical and Stratified Programs
Given an extended program P, with dependency graph Dp, with predicate
symbols p, q, and an extended query Q:

p depends evenly / oddly on q :
There is a path in Dp from p to q with an even (including 0) / odd
number of negative edges.

P is strict wrt. Q :
No predicate symbol occurring in Q depends both evenly and oddly on
a predicate symbol in the head of a clause in P.

P is hierarchical :
No cycle exists in Dp

P is stratified :
No cycle with a negative edge exists in Dp
30 October 2005
Foundations of Logic and Constraint Programming
18
Strict, Hierarchical and Stratified Examples (1)
P1:
p   p
p
-
• p depends on itself (oddly)
• P1 is strict (no even and odd dependency of p on any predicate)
• P1 is not hierarchical (there is a cycle in P1)
• P1 is not stratified (there is a cycle with a negative edge in P1)
P2:
p  q
p  q
q  q
q
p
+
+
• p depends evenly (0) and oddly (1) on q, which depends on itself (evenly)
• P2 is not strict (there is an even and an odd dependency of p on q
• P2 is not hierarchical (there is a cycle in P2,, as q depends on itself)
• P2 is stratified (there is no cycle with a negative edge in P2)
30 October 2005
Foundations of Logic and Constraint Programming
19
Strict, Hierarchical and Stratified Examples (1)
P3:
p(x)   q(x)
p/1
q/1
• p depends oddly on q
• P3 is strict (no even and odd dependency of predicate p/1 on any predicate)
• P1 is hierarchical (there is no cycle in P3)
• P1 is stratified (there is no cycle with a negative edge in P3)
P4:
+
r  p, q
p  p
p
+
r
+
q
• r depends evenly on q and p, that depends evenly on itself
• P4 is strict (no predicate depends evenly and oddly on another predicate)
• P2 is not hierarchical (there is a cycle in P4, the self dependency of p)
• P2 is stratified (there is no cycle with a negative edge in P1)
30 October 2005
Foundations of Logic and Constraint Programming
20
Restricted Completeness of SLDNF-resolution (1)
Theorem (Lloyd, 1987)
Let P be a hierarchical and allowed program and Q an allowed query.
If comp(P) |= Qq for some q such that Qq is ground, then there is a
successful SLDNF-derivation of P  {Q} with CAS q.
Note 1: A SLDNF-derivation might not be found by an interpreter with an
arbitrary selection rule (due to trapping in infinite derivations).
Note 2: The theorem applies to safe interpreters that adopt selection rules that
are safe (do not select negative literals that are not ground), unlike most
Prolog interpreters.
30 October 2005
Foundations of Logic and Constraint Programming
21
Restricted Completeness of SLDNF-resolution (2)
Theorem (Lloyd, 1987)
Let P be a stratified and allowed program and Q an allowed query, such that
P is strict wrt. Q
If comp(P) |= Qq for some q such that Qq is ground, then there is a
successful SLDNF-derivation of P  {Q} with CAS q.
Notes: Theorem does not hold if an arbitrary selection rule is fixed.

The selection rule must be safe and fair (not trapped in infinite
derivations).
30 October 2005
Foundations of Logic and Constraint Programming
22
Fair Selection Rule
An extended selection rule R is fair :
for every SLDNF-tree F via R and for every branch x in F:

Either x is failed; or

For every literal L occurring in a query of x, (some further instantiated
version of ) L is selected within a finite number of derivation steps
Examples:

Selection rule “select leftmost literal” is unfair (depth-first search)

Selection rule “select leftmost literal to the right of the literals introduced
in the previous derivation step, if it exists, otherwise select leftmost literal”
is fair (breadth-first search)
30 October 2005
Foundations of Logic and Constraint Programming
23
Extended Consequence Operator
Let P be an extended program and I a Herbrand interpretation. Then
TP(I) : { H | H  B  ground(P), I |= B}
When P is a definite program, then
-

TP is monotonic

TP is continuous

TP has the least fixpoint M(P)

M(P) = TP  w
In case of extended programs all these properties are lost, since TP is not
monotonic.
30 October 2005
Foundations of Logic and Constraint Programming
24
Extended Consequence Operator is Not Continuous
Pa:
p  q
Let I = {q }
-
Then TP(I) = { },
-
Hence, it is not the case that I  TP(I).
-
Therefore, TP is not monotonic (nor continuous) for Pa (due to negation).
Pb:
p p
Let I1 = { } and I2 = {p }
-
Then TP(I1) = I1 = { }, and TP(I2) = I2 = {p},
-
Therefore, TP is monotonic (and continuous) for Pb. (and all with no negation)
30 October 2005
Foundations of Logic and Constraint Programming
25
Extended TP-Characterization (1)
Lemma 4.3 ([ApBo94]):
Let P be an extended program and I a Herbrand interpretation. Then
I |= P iff TP (I)  I
Proof.
I |= P
iff for every H  B  ground(P) : I |= B implies I |= H
iff for every H  B  ground(P) : I |= B implies H  I
iff for every ground atom H : H  TP (I) implies H  I
iff TP (I)  I
30 October 2005
Foundations of Logic and Constraint Programming
26
Extended TP-Characterization (2)
Definition
Let F and  be ranked alphabets of function and predicate symbols,
respectively, let =   be a binary predicate symbol (for “equality”), and let I
be a Herbrand interpretation for F and  .
Then I= : I  { t = t | t  HUF} is called a standardized Herbrand
interpretation for F and   {=}
Lemma 4.4 ([ApBo94]):
Let P be an extended program and I a Herbrand interpretation. Then
I |= comp(P) iff TP (I) = I
30 October 2005
Foundations of Logic and Constraint Programming
27
Extended TP-Characterization (3)
Proof sketch of Lemma 4.4:
I= |= comp(P)
iff for every ground atom H:
I |= H   (H  B  ground(P)) B )
(since I= is a model for standard axioms of equality and inequality)
iff for every ground atom H:
H  I  I |= B for some H  B  ground(P)
iff for every ground atom H :
H  I implies H  TP (I)
iff TP (I) = I
30 October 2005
Foundations of Logic and Constraint Programming
28
Extended TP-Characterization: Example (1)
Pa:
p  q
Let
I0 = { },
I1 = {p },
Then
TP(I0) = { p }, TP(I1) = { p },
comp(Pa) = {p,  q}
I2 = {q },
I3 = {p, q },
TP(I2) = { },
TP(I3) = { }.

TP (I1 ) = I1 .
Hence, I1 |= comp(Pa) and I1 |= Pa

TP (I2 )  I2. but TP (I2 )  I2.
Hence, I2 |= Pa, but I2 |  comp(Pa)

TP (I3 )  I3. but TP (I3 )  I3.
Hence, I3 |= Pa, but I3 |  comp(Pa)

TP (I0)  I0 .
Hence, I0 | Pa
30 October 2005
Foundations of Logic and Constraint Programming
29
Extended TP-Characterization: Example (2)
Pb:
p  q
q  q
Let
I0 = { },
I1 = {p },
Then
TP(I0) = { p }, TP(I1) = { p },
comp(Pb) = {p   q}
I2 = {q },
I3 = {p, q },
TP(I2) = { q },
TP(I3) = { q }.

TP (I1 ) = I1 .
Hence, I1 |= comp(Pb) and I1 |= Pb

TP (I2 ) = I2 .
Hence, I2 |= comp(Pb) and I1 |= Pb

TP (I3 )  I3. but TP (I3 )  I3.
Hence, I3 |= Pb, but I3 |  comp(Pb)

TP (I0)  I0 .
Hence, I0 | Pa
30 October 2005
Foundations of Logic and Constraint Programming
30
Completion may be Inadequate
ill   ill, infection
infection 
Thus, comp(P)  { ill   ill, infection , infection  true } “=“
{ill   ill, infection  true }
is inconsistent (it has no models).
Hence,
comp(P) |= healthy
But, I = { ill, infection } is the only Herbrand model of P.
Hence,
30 October 2005
P | healthy
Foundations of Logic and Constraint Programming
31
Non-Intended Herbrand Models
Because Tp is not monotonic nor continuous, it is not possible, in general to get a
fixpoint, nor a least model from an extended program. Nevertheless, there are
minimal models, although not necessarily unique.
P1:
p  q
P1 has three Herbrand models
M1 = {p},
M2 = {q},
and
M3 = {p, q}
P1 has no least, but two minimal models: M1 and M2.
However: M1 and not M2 , is the “intended“ model of P1
30 October 2005
Foundations of Logic and Constraint Programming
32
Supported Herbrand Interpretations
A Herbrand interpretation I is supported
:
For every H  I there exists some H  B  ground(P) such that I |= B
( intuitively: B is an explanation for H )
P1:
Example:
M1 = {p, q },
p  q
M2 = {p ,q},
and
M3 = {p, q}

M1 is a supported model of P1 ( q is the explanation for p)

M2 is no supported model of P1 ( there is no explanation for q)
Note that TP(M2) = { }  M1
30 October 2005
and that TP(M1) = M1.
Foundations of Logic and Constraint Programming
33
Extended TP-Characterization (4)
Lemma 6.2 ([ApBo94]):
Let P be an extended program and I a Herbrand interpretation. Then
I |= P and I supported iff TP (I) = I
Proof (sketch):
I |= P and I supported
-
iff for every H  B  ground(P) : I |= B implies I |= H and
for every H  I: I |=  (H  B  ground(P)) B
-
iff for every ground atom H : I |= ( H   (H  B  ground(P)) B )
and I |= (H →  (H  B  ground(P)) B )
-
iff for every ground atom H : I |= ( H   (H  B  ground(P)) B )
-
iff I= is a model of comp(P)
-
iff TP (I) = I (cf. Lemma 4.4)
30 October 2005
Foundations of Logic and Constraint Programming
34
Non-Intended Supported Models
P2:
p  q
q  q
- P2 has three Herbrand models
M1 = {p},
M2 = {q},
and
M3 = {p, q}
- P2 has two supported Herbrand models : M1 and M2.
In fact, both M1 and M2 are minimal models for comp(P2) = {p   q}
- However: M1 and not M2 , is the “intended“ model of P2.
M1 is called the standard model of P2 ( cf. later slide)
- In general, it is not possible to define standard models, unless the programs
are stratified!
30 October 2005
Foundations of Logic and Constraint Programming
35
Stratifications
Let P be an extended program and Dp its dependency graph,

Predicate symbol p is defined in P : P contains a clause p(t1, ..., tm)  B

P1  ...  Pn = P is a stratification of P :

Pi   for every i  1.. n

Pi  Pj =  for every i,j  1.. n, with i  j

for every p defined in Pi and edge p →+ q in Dp :
q is not defined in  n j = i+1 Pj

for every p defined in Pi and edge p →- q in Dp :
q is not defined in  n j = i Pj
Lemma 6.5 ([ApBo94]):
An extended program is stratified iff it admits a (not necessarily unique)
stratification.
30 October 2005
Foundations of Logic and Constraint Programming
36
Stratifications Example (1)
zero(0) 
positive(x)  num(x), zero(x)
num(0) 
num(s(x))  num(x)

P1  P2  P3 is a stratification of P , where

P1 = { num(0) 

P2 = { zero(0)  }

P3 = { positive(x)  num(x) ,  zero(x) }
30 October 2005
,
num(s(x))  num(x) }
Foundations of Logic and Constraint Programming
37
Stratifications Example (2)
even(0) 
even(x)  odd(x), num(x)
odd(s(x))  even(x)
num(0) 
num(s(x))  num(x)
P admits no stratification
since
strat(even) > strat(odd)
30 October 2005
but strat(odd)  strat(even)
Foundations of Logic and Constraint Programming
38
Standard Models (Stratified Programs)
Let
-
I be an Herbrand interpretation and  a set of predicate symbols:
-
I |  : I  { p(t1, ..., tm) | p  P, t1, ..., tm ground terms)
-
P1  ...  Pn be a stratification of a stratification of extended program P,
Then

M1 : least Herbrand model of P1 such that
M1 | { p | p not defined in P } = 

M2 : least Herbrand model of P2 such that
M2 | { p | p defined nowhere or in P1 } = M1
...

Mn : least Herbrand model of Pn such that
Mn | { p | p defined nowhere or in P1  ...  Pn-1 } = Mn-1
We call MP = Mn the standard model of P
30 October 2005
Foundations of Logic and Constraint Programming
39
Standard Models: Example
zero(0) 
positive(x)  num(x), zero(x)
num(0) 
num(s(x))  num(x)
Let P1  P2  P3 with
- P1 = { num(0)  , num(s(x))  num(x) }
- P2 = { zero(0)  }
- P3 = { positive(x)  num(x) ,  zero(x) }
be a stratification of P. Then
 M1 = { num(t) | t  HU{s,0} }
 M2 = { num(t) | t  HU{s,0} }  {zero(0)}
 M3 = { num(t) | t  HU{s,0} }  {zero(0)}  {positive(t) | t  HU{s,0} – {0} }
Hence MP = M3 is the standard model of P
30 October 2005
Foundations of Logic and Constraint Programming
40
Properties of Standard Models
Theorem 6.7 ([ApBo94]):
Consider a stratified program P. Then

MP does not depend on the chosen stratification of P,

MP is a minimal model of P,

MP is a supported model of P,
Corollary:
For a stratified program P, comp(P) admits a Herbrand Model.
30 October 2005
Foundations of Logic and Constraint Programming
41