atomic formulats

Horn goal G (... generated by the grammar)

G ::= T | F | t = s

Horn clause for the predicate p ....

any x1 x2 .. { p(x) === G }

Horn program

noetherian

?- G.

Clark's completion

conjecture.

closed world open world

search.

netural expression

N::= 0 | 1 | t = 2 | N + N | N * N | QxN

linear logic

rewriting neutral expressions

not unifiable

## No comments:

Post a Comment