Reasoning with Negation

;; Standard demo preamble:

|= (in-package "STELLA")


|= (defmodule "/PL-USER/NEGATION")

|MDL|/PL-USER/NEGATION

|= (in-module "/PL-USER/NEGATION")


|= (clear-module "/PL-USER/NEGATION")


|= (reset-features)

|i|()

|= (in-dialect :KIF)

:KIF

;; The familiar `Person' class now with a slightly different set of slots:

|= (defclass PERSON (STANDARD-OBJECT)
  :documentation "The class of human beings."
  :slots ((happy :type BOOLEAN)
	  (despondent :type BOOLEAN)
          (boss :type PERSON)))

|C|PERSON

;; Some people and their bosses:

|= (assert (Person Fred))

|P|(PERSON FRED)

|= (assert (Person Edward))

|P|(PERSON EDWARD)

|= (assert (Person Carla))

|P|(PERSON CARLA)

|= (assert (= (boss Fred) Edward))

|P|(= (BOSS FRED) EDWARD)

|= (assert (= (boss Edward) Carla))

|P|(= (BOSS EDWARD) CARLA)

;; Fred's boss is not happy.  Note, that this assertion is treated
;; extensionally, i.e., it is about `Edward', not the intensional
;; individual representing Fred's boss.  Note also, that top-level
;; negated proposition objects are printed with a `|P~|' prefix
;; instead of an explicit `not', since such propositions use FALSE as
;; their truth value:

|= (assert (not (Happy (boss Fred))))

|P~|(HAPPY EDWARD)

;; An alternative way of asserting negated propositions is with help
;; of `deny'.  Note, that the assertion below does not create a new
;; proposition, since an identical proposition already exists:

|= (deny (Happy (boss Fred)))

|P~|(HAPPY EDWARD)

;; Retrieve all people with an unhappy boss (this tests negated atomic
;; formulas containing a function argument):

|= (retrieve all (?x PERSON) (not (Happy (boss ?x))))

There is 1 solution:
  #1: ?X=|i|FRED

;; Note, that the above query is basically a shorthand for this:

|= (retrieve all (?x PERSON)
          (exists (?y PERSON)
            (and (= (boss ?x) ?y)
                 (not (Happy ?y)))))

There is 1 solution:
  #1: ?X=|i|FRED

;; Negation of a unary relation (or property):

;; Below is the first rule with a negated head involving two unary
;; relations defined as slots on the class `Person'.  Remember, that,
;; currently, PowerLoom can only reason with rules that have simple
;; heads (Horn rules).  A negated head is a simple head if its
;; argument is a non-negated simple head (see the `append' demo for
;; more description of simple heads).

|= (assert (forall (?x PERSON)
          (=> (despondent ?x)
              (not (happy ?x)))))

|P|(forall ((?x1 PERSON))
   (<= (not (HAPPY ?x1))
       (DESPONDENT ?x1)))

|= (assert (Person Greg))

|P|(PERSON GREG)

|= (assert (despondent Greg))

|P|(DESPONDENT GREG)

;; Again, note that `ask' only looks for positive answers to the asked query,
;; thus, we have to explicitly ask the negated query to get the result:

|= (ask (happy Greg))


|= (ask (not (happy Greg)))

|L|TRUE

;; Negation of a binary relation:

|= (defrelation has-friend ((?x PERSON) (?y PERSON))
  :documentation "True, if `?x' has `?y' as a friend.")

|T|HAS-FRIEND

|= (defrelation has-enemy ((?x PERSON) (?y PERSON))
  :documentation "True, if `?x' has `?y' as an enemy.")

|T|HAS-ENEMY

;; Another rule with a negated head that involves two binary relations:

|= (assert (forall ((?x PERSON) (?y PERSON))
          (=> (has-enemy ?x ?y)
              (not (has-friend ?x ?y)))))

|P|(forall ((?x1 PERSON) (?x2 PERSON))
   (<= (not (HAS-FRIEND ?x1 ?x2))
       (HAS-ENEMY ?x1 ?x2)))

|= (assert (Person Harry))

|P|(PERSON HARRY)

|= (assert (has-enemy Greg Harry))

|P|(HAS-ENEMY GREG HARRY)

|= (ask (has-friend Greg Harry))


|= (ask (not (has-friend Greg Harry)))

|L|TRUE

;; Negation of class membership:

|= (defclass MALE-PERSON (PERSON))

|C|MALE-PERSON

|= (defclass FEMALE-PERSON (PERSON))

|C|FEMALE-PERSON

|= (assert (forall (?x MALE-PERSON)
          (not (Female-Person ?x))))

|P|(forall ((?x MALE-PERSON))
   (<= (not (FEMALE-PERSON ?x))
       (MALE-PERSON ?x)))

|= (assert (Person Ivan))

|P|(PERSON IVAN)

|= (assert (Male-Person Ivan))

|P|(MALE-PERSON IVAN)

|= (ask (Female-Person Ivan))


|= (ask (not (Female-Person Ivan)))

|L|TRUE

|=