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