|
|
Depth of Terms
| Description: |
The depth of a term in a definite clause is inductively defined as follows:
- All terms t occuring in the head of the clause have depth d(t) := 0.
- For all other terms t occuring in the clause the depth is defined as
d(t) := min { d(u) | There is a literal containing t and u. } + 1.
So in the clause P(u, v) ← Q(w, v) ⋀ P(w, x) the terms
u and v would have depth 0, w depth 1 and x would have depth 2, for
example. |
|
|
