isDatalog

Whether this Theory belongs to the (function-free, safely-negated, non-recursive) Datalog subset of Prolog recognised by this module, i.e. whether every one of its Theory.rules satisfies hasNoCompound, allHeadVariablesInNonNegatedLiterals and allNegatedLiteralsVariablesInNonNegatedLiteralsToo, and the theory as a whole is isNonRecursive.

Restricting a theory to this subset matters because, unlike a general Prolog theory, a Datalog theory is guaranteed to terminate and to admit a unique minimal model when evaluated bottom-up: it cannot construct arbitrarily large new terms (no compound arguments) and it cannot loop through recursive predicate calls, so every derivable fact is built from the — finitely many — constants already occurring in the theory. Note this module's notion of Datalog is slightly stricter than some textbook definitions on two points: compound arguments are forbidden outright (not just newly-constructed ones), and recursion is forbidden outright (not just recursion through negation).

Example — using the :dsl-core builders, a clause accepted as Datalog, and one rejected for each reason:

// accepted: only constants/variables as arguments, head vars covered by a positive goal, no recursion
rule { "ancestor"(X, Y) impliedBy "parent"(X, Y) }

// rejected by hasNoCompound: `f(X)` is a compound argument
rule { "p"(X) impliedBy "q"("f"(X)) }

// rejected by allHeadVariablesInNonNegatedLiterals: `Y` occurs in the head only
rule { "p"(X, Y) impliedBy "q"(X) }

// rejected by allNegatedLiteralsVariablesInNonNegatedLiteralsToo: `Y` occurs only inside `not(...)`
rule { "p"(X).impliedBy("q"(X), "not"("r"(Y))) }

// rejected by isNonRecursive: `p` calls itself (directly)
rule { "p"(X) impliedBy "p"(X) }

See also