Another way of adding negative information to the program is that proposed by
Clark [1978] and called the completion of a program. His idea was to rein-
terpret the implications within the program as equivalences. In this way one
adds to the program the "only if part which allows us to infer negative con-
sequences.
More formally the completion is defined as follows. (We slightly depart
here from the original definition as we omit the equality axioms which are
automatically satisified in Herbrand models when "=" is interpreted as
identity.)
Let
x
v
...,x
k
,
be some variables not appearing in th
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.