Negation

There are 3 types of negation in Flora:

• \+ - Prolog negation
• \naf - Negation based on the well-founded semantics
• \neg - Explicit negation

For most practical purposes, the first two types are similar. Both types embody a form of “negation-as-failure”, that is, \+ p or \naf p will be true if p itself cannot be proven to be true. One difference occurs when the formula under the operator contains variables. For example, we can define the notion of being a bachelor using \+ as follows:

?Person[bachelor] :-
  ?Person : Man,
  \+ ?Person [spouse -> ?Spouse].

Note that the formula under the \+ operator contains a variable ?Spouse. In this situation, if we want to use \naf instead of \+, we have to introduce an exists operator to quantify the variable:

?Person[bachelor] :-
  ?Person : Man,
  \naf exists(?Spouse)^(?Person [spouse -> ?Spouse]).

See Quantifiers for more on exists (there is also a forall operator). Unlike \+, \naf has a well-defined model theoretic semantics, and its use is recommended over \+.

The \neg operator, on the other hand, is completely different. A goal \neg p only succeeds if \neg p has been explicitly asserted, or can be derived from some rule. We saw an example of \neg in the section on boolean properties, above. Unlike the other negations, \neg can occur in rule heads and facts. \neg represents “classical negation” rather than “negation-as-failure”. However, the Flora reasoning engine does not do the kinds of reasoning that a first-order logic theorem prover does in order to prove such negations. For example, in first-order logic, from p or q, not p, one can derive q, but not in Flora.

Another way to look at it is that \naf p and \+ p mean “p is not known to be true”, whereas \neg p means “p is false”. Thus \neg p is a stronger statement. Consequently, \neg p implies \naf p [1] .

Warning: Somewhat surprisingly, Flora allows both p and \neg p to be true at the same time. In first-order logic, this would cause an inconsistency, which allows you to derive any fact whatsoever. But again, Flora does not have such reasoning power. Still, if using \neg, watch out for this issue.

The section “Negation” in the Flora-2 Manual [2] has more details on the different types of negation.

[1]	But it does not imply \+ p. Of course, neither \naf p nor \+ p imply \neg p, as a weaker statement cannot imply a stronger statement

[2]	Kifer, Michael, Guizhen Yang, Wan Hui, and Chang Zhao. 2014. Flora-2: User’s Manual. 1.0. Stony Brook University, Stony Brook: Department of Computer Science.