Ontology: Akt-Support-Ontology; Representation Language: ONTOLINGUA; File: frames

This ontology was created by the Advanced Knowledge Technologies (AKT) project. AKT is an Interdisciplinary Research Collaboration (IRC), which is sponsored by the UK Engineering and Physical Sciences Research Council under grant number GR/N15764/01. The AKT IRC comprises the Universities of Aberdeen, Edinburgh, Sheffield, Southampton and the Open University.

;;;Automatically translated from OCML file #P"C:/users/jbd2/code/ocml/library/v5-0/domains/akt-support-ontology/frames.lisp"
(in-package "ONTOLINGUA-USER")

(in-ontology 'akt-support-ontology)


(Define-Frame CLASS  

  :own-slots
  (  (Documentation "The class of all classes.  We consider a class as a unary relation, true for all its instances")
  (Subclass-of unary-relation)))


(Define-Frame CLASS-PARTITION  

  :own-slots
  (  (Documentation "A set of mutually disjoint classes.  Disjointness of
   classes is a special case of disjointness of sets.")
  (Subclass-of enumerated-set))

  :axioms
((<=> (and (enumerated-set ?set-of-classes) (forall ?c (=> (element-of ?c ?set-of-classes) (class ?c))) (forall (?c1 ?c2) (=> (and (element-of ?c1 ?set-of-classes) (element-of ?c2 ?set-of-classes) (not (= ?c1 ?c2))) (forall (?i) (=> (instance-of ?i ?c1) (not (instance-of ?i ?c2))))))) (class-partition ?set-of-classes))
(=> (class-partition ?set-of-classes) (enumerated-set ?set-of-classes))
))


(Define-Relation SUBCLASS-PARTITION (?c ?class-partition) 
"A subclass-partition of a class C is a set of
    subclasses of C that are mutually disjoint."
  :iff-def (and (class ?c) (class-partition ?class-partition) (forall ?subclass (=> (element-of ?subclass ?class-partition) (subclass-of ?subclass ?c)))))


(Define-Relation EXHAUSTIVE-SUBCLASS-PARTITION (?c ?class-partition) 
"A subrelation-partition of a class C is a set of
    mutually-disjoint classes (a subclass partition) which covers C.
    Every instance of C is is an instance of exactly one of the subclasses
    in the partition."
  :iff-def (and (subclass-partition ?c ?class-partition) (forall ?instance (=> (instance-of ?instance ?c) (exists ?subclass (and (element-of ?subclass ?class-partition) (instance-of ?instance ?subclass)))))))


(Define-Relation INSTANCE-OF (?x ?c) 
"This definition relates the notion of 'being an instance' to the notion
   of satisfying a relation: ?I is an instance of a class ?c, 
   iff (holds ?I ?c) is true"
  :iff-def (and (class ?c) (holds ?c ?x))
  :constraints (class ?c))


(Define-Relation SUBCLASS-OF (?sub ?c) 
"?sub is a subclass of ?c if every instance of ?sub is also an instance of 
   ?c.  Note that according to this definition every class is a subclass of itself"
  :iff-def (and (class ?sub) (class ?c) (forall ?inst (=> (instance-of ?inst ?sub) (instance-of ?inst ?c))))
  :constraints (and (class ?sub) (class ?c)))


(Define-Function ALL-SUPERCLASSES (?class) :-> ?supers 
"returns all superclasses of a class"
:def (forall ?super (<=> (member ?super ?supers) (subclass-of ?class ?super)))
:constraints (class ?class))


(Define-Function ALL-SUBCLASSES (?class) :-> ?subs 
"returns all subclasses of a class"
:def (forall ?sub (<=> (member ?sub ?subs) (subclass-of ?sub ?class)))
:constraints (class ?class))


(Define-Relation DIRECT-INSTANCE-OF (?x ?c) 

  :iff-def (and (instance-of ?x ?c) (not (exists ?c2 (and (subclass-of ?c2 ?c) (instance-of ?x ?c2)))))
  :constraints (class ?c))


(Define-Function ALL-DIRECT-INSTANCES (?c) :-> ?instances 
:constraints (class ?c))


(Define-Function THE-PARENT (?i) :-> ?class 
:def (direct-instance-of ?i ?class)
:lambda-body (the ?class (direct-instance-of ?i ?class)))


(Define-Relation DIRECT-SUBCLASS-OF (?sub ?super) 

  :iff-def (and (subclass-of ?sub ?super) (not (exists ?c2 (and (subclass-of ?sub ?c2) (subclass-of ?c2 ?super)))))
  :constraints (and (class ?sub) (class ?super)))


(Define-Relation DIRECT-SUPERCLASS-OF (?super ?sub) 

  :iff-def (direct-subclass-of ?sub ?super))


(Define-Function ALL-DIRECT-SUPERCLASSES (?class) :-> ?supers 
:def (= ?supers (setofall ?x (direct-superclass-of ?x ?class)))
:constraints (class ?class))


(Define-Function ALL-DIRECT-SUBCLASSES (?class) :-> ?subs 
:def (= ?subs (setofall ?x (direct-subclass-of ?x ?class)))
:constraints (class ?class))

Contact Point