more on RIF entailment regime

"Without appropriate safety conditions, cyclic references can rule out the existence of a single intended Herbrand model of the combination and indeed various stratification and stable model theories [STABLEMODEL] have been defined in the literature that use a dependency graph to determine if a ruleset is stratified and incorporate the restricted use of built-in function symbols that allow the truth of a predicate to be well-defined by an external procedure.  This entailment regime restricts the legal graphs to only those that refer to strongly safe RIF core documents. This excludes the use of negated (non-monotonic) atoms and cyclic references between terms in built-ins."

I think this paragraph might confuse. Stable models, stratification, etc. are only vaguely related to the issue we face here, since they are usually only of interest in the context of rule languages with (non-monotonic) negation. Neither RIF Core nor RIF BLD have negation, so I think it shouldn't be mentioned here.

I think we are (modulo datatypes, which I am afraid is an issue here as well) fine for strongly safe RIF Core.
However, as for finiteness criteria for non-strongly safe core, I find it hard however to think of anything else 
than something operationally defined (as I had sketched it earlier, by e.g. limiting the "levels of recursion" somehow.)

Axel

Received on Thursday, 25 March 2010 08:35:03 UTC