This certainly satisfies { —iA: Ρ ){= A} so we have only to check that it
satisfies P. Each ground instance
Β — A
lf
. . .
,
A
r
(or — A
lf
. . .
,
A
r
)
of a clause of Ρ is true in M, because if M |=
A,,...,A
r
then Ρ \=
A,,...,A
r
so
Ρ (= Β (or Ρ (= f, which is ruled out by the consistency of P), so M |= B. •
Since every set of definite Horn clauses is consistent (the whole Herbrand
base is a model for it) we have:
THEOREM 8
If Ρ is a set of definite Horn clauses and S is any set of ground atoms (possibly
involving new constants and function symbols) then cwa(P U S) is consistent
relative to any extension of the Herbrand universe
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month, and much more.