This is an archive of an inactive wiki and cannot be modified.

This extension introduces two kinds of negation (Naf and Neg) to the RIF Condition Language, initially proposed for Phase 1 queries. Neg denotes classical negation as defined in first-order logic; special uses of it can be shared by FO and all dialects that support a form of classical negation (e.g., certain dialects of LP; perhaps some PR dialects).

Naf denotes negation as failure in one of its incarnations (well-founded or stable-model). The actual flavor of Naf is determined by inspecting the value of a semantic tag associated with the ruleset.

Naf is used in LP (and in queries and constraints over the intended models of LP); it can possibly be relevant to PR and RR.

Alongside negation we can introduce explicit universal quantification.

SYNTAX

This extension introduces two negation symbols over atoms, and one legal nesting, for which we propose to use the notation Naf/Neg, as in RuleML:

  LITFORM ::= Atom | 'Neg' Atom | 'Naf' Atom | 'Naf' 'Neg' Atom

Note that in Phase 1 we are proposing to use negation only in queries. Phase 1 rules will all be Horn and their bodies will not have negation. Phase 2 will extend RIF to allow negation in rules as well.

The next step could be to allow universal quantification:

  QUANTIF ::= 'Exists' Var+ '(' CONDIT ')' |
              'Forall' Var+ '(' CONDIT ')'