Reasoning with Negation

    Welcome to PowerLoom 3.0.1.beta

Copyright (C) USC Information Sciences Institute, 1997-2003.
PowerLoom is a registered trademark of the University of Southern California.
PowerLoom comes with ABSOLUTELY NO WARRANTY!
Type `(copyright)' for detailed copyright information.
Type `(help)' for a list of available commands.
Type `(demo)' for a list of example applications.
Type `bye', `exit', `halt', `quit', or `stop', to exit.


|= (demo 7)

Now reading from `PL:sources;logic;demos;negation.ste'.
Type `?' at the pause prompt for a list of available commands.

;;; -*- Mode: Lisp; Package: STELLA; Syntax: COMMON-LISP; Base: 10 -*-

;;; Version: negation.ste,v 1.9 2002/04/19 03:04:19 hans Exp

;;; Reasoning with negation
;;; =======================

;;; This file demonstrates some reasoning examples that involve
;;; negation.  Some of the preceding demos did already use negation.
;;; What's new in this demo is the use of negated rule heads.

;;; The best way to view this file is by calling `(demo)' and
;;; selecting it from the menu of example demos.  This demo assumes
;;; familiarity with some basic PowerLoom concepts which are described
;;; in the introductory demo (#1 on the demo menu) and other demos
;;; preceding this one.


;; Standard demo preamble:

|= (in-package "STELLA")
------ pause ------c


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

|MDL|/PL-KERNEL-KB/PL-USER/NEGATION

|= (in-module "NEGATION")


|= (clear-module "NEGATION")


|= (reset-features)

|l|(:EMIT-THINKING-DOTS :JUST-IN-TIME-INFERENCE)

|= (in-dialect :KIF)

:KIF

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

|= (defconcept PERSON (?p)
  :documentation "The class of human beings.")

|c|PERSON

|= (defrelation happy ((?p PERSON)))

|r|HAPPY

|= (defrelation despondent ((?p PERSON)))

|r|DESPONDENT

|= (deffunction boss ((?p PERSON)) :-> (?b PERSON))

|f|BOSS

;; 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|(NOT (HAPPY (BOSS FRED)))

;; 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|(NOT (HAPPY (BOSS FRED)))

;; 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=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=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 (?x)
   (<= (NOT (HAPPY ?x))
       (DESPONDENT ?x)))

|= (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))

UNKNOWN

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

TRUE

;; Negation of a binary relation:

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

|r|HAS-FRIEND

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

|r|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 (?x ?y)
   (<= (NOT (HAS-FRIEND ?x ?y))
       (HAS-ENEMY ?x ?y)))

|= (assert (Person Harry))

|P|(PERSON HARRY)

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

|P|(HAS-ENEMY GREG HARRY)

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

UNKNOWN

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

TRUE

;; Negation of class membership:

|= (defconcept MALE-PERSON (?p PERSON))

|c|MALE-PERSON

|= (defconcept FEMALE-PERSON (?p PERSON))

|c|FEMALE-PERSON

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

|P|(FORALL (?x)
   (<= (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))

FALSE

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

TRUE

|= 

Finished demo `PL:sources;logic;demos;negation.ste'.

|=