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 ')'