A pure Prolog rule
are atoms, can be viewed as a syntactic variant of the monotonic rule
except for two important details. First, the declarative semantics of Prolog applies the unique names assumption to its ground terms. If, for example, the program contains no function constants, then this assumption can be expressed by the sentences
for all distinct object constants
in the language of the program. Second, this semantics applies the closed world assumption to each relation. For a relation constant
, this assumption can be expressed by the following rule.
A pure Prolog program can be translated into KIF by appending to it (i) the sentences expressing the unique names assumption, and (ii) the default rules expressing the closed world assumption.
This method can be easily extended to programs with negation as failure. A negative subgoal not
is represented in KIF by the premise (consis (not
)). (Adding consis is necessary because, in KIF, not represents classical negation, rather than negation as failure.)