Subsumption

;;; Under construction.

|= (in-package "STELLA")


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

|MDL|/PL-USER/SUBSUMPTION

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


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


|= (reset-features)

|i|()

|= (in-dialect :KIF)

:KIF

|= (defclass PERSON (STANDARD-OBJECT)
  :slots ((friends :type (LIST OF PERSON))))

|C|PERSON

|= (defrelation has-parent ((?x PERSON) (?y PERSON)))

|T|HAS-PARENT

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

|S|PERSON.MALE

|= (defrelation has-father ((?p PERSON) (?f PERSON))
  :definition (kappa ((?p PERSON) (?f PERSON))
                 (and (has-parent ?p ?f) (male ?p))))

|T|HAS-FATHER

|= (ask (subset PERSON.has-father PERSON.has-parent))

|L|TRUE

;;; Harder problems for the subsumption test:

|= (defmethod (cardinality INTEGER) ((self COLLECTION))
  (return (length (collection-members self :CLOSED))) )

|M|COLLECTION.CARDINALITY

|= (assert (forall ((?x NUMBER) (?y NUMBER)) (<= (>= ?x ?y) (> ?x ?y))))

|P|(forall ((?x1 NUMBER) (?x2 NUMBER))
   (<= (>= ?x1 ?x2)
       (> ?x1 ?x2)))

|= (defclass Person-with-Friends (PERSON)
  :definition (kappa ((?x PERSON)) (>= (cardinality (friends ?x)) 1)))

|C|PERSON-WITH-FRIENDS

|= (defclass Person-with-Atleast-2-Friends (PERSON)
  :definition (kappa ((?x PERSON)) (>= (cardinality (friends ?x)) 2)))

|C|PERSON-WITH-ATLEAST-2-FRIENDS

|= (defclass Person-with-Exactly-2-Friends (PERSON)
  :definition (kappa ((?x PERSON)) (= (cardinality (friends ?x)) 2)))

|C|PERSON-WITH-EXACTLY-2-FRIENDS

|= (defclass Person-with-More-Than-2-Friends (PERSON)
  :definition (kappa ((?x PERSON)) (> (cardinality (friends ?x)) 2)))

|C|PERSON-WITH-MORE-THAN-2-FRIENDS

|= (ask (subset Person-with-Exactly-2-Friends Person-with-Atleast-2-Friends))

|L|TRUE

|= (ask (subset Person-with-Atleast-2-Friends Person-with-Exactly-2-Friends))


|= (ask (subset Person-with-More-Than-2-Friends Person-with-Atleast-2-Friends))

|L|TRUE

|= (ask (subset Person-with-Atleast-2-Friends Person-with-More-Than-2-Friends))


|= (ask (subset Person-with-Atleast-2-Friends Person-with-Friends))


|= (assert
  (forall ((?x INTEGER) (?z INTEGER))
	   (<= (> ?x ?z)
	       (exists ((?y INTEGER))
		 (and (>= ?x ?y) (>= ?y ?z))))))

|P|(forall ((?x INTEGER) (?z INTEGER))
   (<= (> ?x ?z)
       (exists ((?y INTEGER))
          (and (>= ?x ?y)
               (>= ?y ?z)))))

|= (ask (subset Person-with-Atleast-2-Friends Person-with-Friends))

|L|TRUE

|=