Definite Logic Programs: Models

Recall:

F is a logical consequence of P
Since there are (in general) infinitely many possible interpretations, how can we check if F is a logical consequence of P?
- Solution:
  
  choose one ‘canonical‘ model I such that

A formula of the form $p(t_1, t_2, …, t_n)$ , where $p/n$ is an $n$-ary predicate symbol and $t_i$ are all terms is said to be atomic.

Given an alphabet A, the set of all ground terms constructed from the constant and function symbols of A is called the Herbrand Universe of A (denoted by $U_A$).
Consider the program:
1
2
p(zero).
p(s(s(X))) <- p(X).
The Herbrand Universe of the program’s alphabet is:

$U_A={zero, s(zero), s(s(sero)),…}$

Consider the ‘relations’ program:

parent(pam, bob).

parent(bob, ann).

parent(tom, bob).

parent(bob, pat).

parent(tom, liz).

parent(pat, jim).

grandparent(X, Y):-

parent(X, Z), parent(Z, Y).
The Herbrand Universe of the program’s alphabet is:

$U_A={pam, bob, tom, liz, ann, pat, jim}$

Given an alphabet A, the set of all ground atomic formulas over A is called the Herbrand Base of A (denoted by $B_A$).
Consider the program:
1
2
p(zero).
p(s(s(X))) <- p(X).
The Herbrand Base of the program’s alphabet is:

$B_A={p(zero), p(s(zero)), p(s(s(zero))),…}$

All Herbrand interpretations of a program give the same ‘meaning’ to the constant and function symbols.
- Different Herbrand interpretations differ only in the ‘meaning’ they give to the predicate symbols.
We often write a Herbrand model simply by listing the subset of the Herbrand base that is true in the model
- Example: Consider our numbers program, where {p(zero), p(s(s(zero))), p(s(s(s(s(zero))))), …} represents the Herbrand model that treats {…}

Let P be a definite program. If I’ is a model of P then I = {} is a Herbrand model of P.
(Update lecture slide)

Let P be a definite program. If I’ is a model of P then I = {$A\in B_P | I’ \imply A$} is a Herbrand model of P.
This property holds only for definite programs.
- Consider P = …
  - There are two Herbrand interpretations:
    - The first is not a model of P since
    - The second is not a model of P since
  - But there are non-Herbrand models, such as I:
    - |I| = N (the set of natural numbers)
    - $a_I = 0$
    - $p_I=$”is odd”

If M is a set of Herbrand Models of a definite program P, then $\cap$M is also a Herbrand Model of P.
For every definite program P there is a unique least model $M_P$ such that:
- $M_P$ is a Herbrand Model of P and,
- for every Herbrand Model M, $M_P$
For any definite program, if every Herbrand Model of P is also a Herbrand Model of F, then …
$M_P=$ the set of all ground logical consequences of P.

The least Herbrand model $M_P$of a definite program P is the set of all ground logical consequences of the program.
First,
- By definition of logical consequence, means that has to be in every model of P and hence also in the least Herbrand model.
Second,:
- If … then A is in every Herbrand model of P.
- But assume there is some model I’
- By sufficiency of Herbrand models, there is some Herbrand model I such that…
- Hence A is not in some Herbrand model, and hence is not in $M_P$.

Immediate consequence operator:
- Given
- I’ is said to be the immediate consequence of I.
- Written as $I’ = T_P(I), T_P$ is called the immediate consequence operator.
- Consider the sequence: