Ontology: Akt-Support-Ontology; Representation Language: OCML; 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.
;;; -*- Mode: LISP; Syntax: Common-lisp; Base: 10; Package: OCML; -*-
(in-package "OCML")
(in-ontology akt-support-ontology)
;;;here I have defined a few basic notions we need to have to talk about frame-based models
(def-class CLASS (unary-relation) 
"The class of all classes. We consider a class as a unary relation, true for all its instances"
:lisp-fun #'(lambda (x env)
(let ((y (unbound-variable? x env)))
(if y
(mapcar #'(lambda (rel)
(cons (cons y rel) env))
(all-ocml-classes))
(if (get-ocml-class
(instantiate x env))
(list env)
:fail)))))
(def-class CLASS-PARTITION (enumerated-set) ?set-of-classes
"A set of mutually disjoint classes. Disjointness of
classes is a special case of disjointness of sets."
:constraint (enumerated-set ?set-of-classes)
:iff-def (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)))))))
:avoid-infinite-loop t)
(def-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)))))
(def-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)))))))
(def-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"
:constraint (class ?c)
:iff-def (and (class ?c)
(holds ?c ?x)))
(def-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"
:constraint (and (class ?sub)(class ?c))
:prove-by (or (and (variable-bound ?sub)
(member ?c (all-superclasses ?sub)))
(and (variable-bound ?c)
(not (variable-bound ?sub))
(member ?sub (all-subclasses ?c)))
(and
(not (variable-bound ?c))
(not (variable-bound ?sub))
(class ?sub1)(class ?super1)
(subclass-of ?sub1 ?super1)))
:iff-def (and (class ?sub) (class ?c)
(forall ?inst
(=> (instance-of ?inst ?sub)
(instance-of ?inst ?c))))
:no-proofs-by (:iff-def))
(def-function ALL-SUPERCLASSES (?class) -> ?supers
"returns all superclasses of a class"
:constraint (class ?class)
:def (forall ?super (<=> (member ?super ?supers)
(subclass-of ?class ?super)))
:lisp-fun #'(lambda (class)
(let ((class-s (get-ocml-class class)))
(if class-s
(cons class-s (mapcar #'name (domain-superclasses class-s)))))))
(def-function ALL-SUBCLASSES (?class) -> ?subs
"returns all subclasses of a class"
:constraint (class ?class)
:def (forall ?sub (<=> (member ?sub ?subs)
(subclass-of ?sub ?class)))
:lisp-fun #'(lambda (class)
(let ((class-s (get-ocml-class class)))
(if class-s
(cons class-s (mapcar #'name (current-subclasses class-s)))))))
(def-relation direct-instance-of (?x ?C)
:constraint (class ?c)
:iff-def (and (instance-of ?x ?c)
(not (exists ?c2
(and (subclass-of ?c2 ?c)
(instance-of ?x ?c2)))))
:prove-by (or (and (variable-bound ?c)
(class ?c)
(member ?x (all-direct-instances ?c)))
(and (not (variable-bound ?c))
(variable-bound ?x)
(= (the-parent ?x) ?c)
(not (= ?c :nothing)))
(and (not (variable-bound ?c))
(not (variable-bound ?x))
(exec (output "Trying to prove direct-instance-of with 2 unbound variables....you will definitively lose..."))
(class ?c)
(direct-instance-of ?x ?c)))
:no-proofs-by (:iff-def))
(def-function all-direct-instances (?c) -> ?instances
:constraint (class ?c)
:lisp-fun #'(lambda (c)
(mapcar #'name (all-current-direct-instances c))))
(def-function the-parent (?i) -> ?class
:def (direct-instance-of ?i ?class)
:body (the ?class (direct-instance-of ?i ?class))
:lisp-fun #'(lambda (i)
(if (find-current-instance i)
(name (parent-class (find-current-instance i)))
:nothing)))
(def-relation direct-subclass-of (?sub ?super)
:constraint (and (class ?sub)(class ?super))
:iff-def (and (subclass-of ?sub ?super)
(not (exists ?c2
(and (subclass-of ?sub ?c2)
(subclass-of ?c2 ?super)))))
:prove-by (or (and (variable-bound ?sub)
(class ?sub)
(member ?super (all-direct-superclasses ?sub)))
(and (not (variable-bound ?sub))
(variable-bound ?super)
(member ?sub (all-direct-subclasses ?super)))
(and (not (variable-bound ?sub))
(not (variable-bound ?super))
(exec (output
"Trying to prove direct-subclass-of with 2 unbound variables....you will definitively lose..."))
(class ?sub)
(member ?super (all-direct-superclasses ?sub))))
:no-proofs-by (:iff-def))
(def-relation DIRECT-SUPERCLASS-OF (?super ?sub)
:iff-def (direct-subclass-of ?sub ?super))
(def-function ALL-DIRECT-SUPERCLASSES (?class) -> ?supers
:constraint (class ?class)
:def (= ?supers (setofall ?x (direct-superclass-of ?x ?class)))
:lisp-fun #'(lambda (class)
(let ((class-s (get-ocml-class class)))
(if class-s
(mapcar #'name (direct-domain-superclasses class-s))))))
(def-function ALL-DIRECT-SUBCLASSES (?class) -> ?subs
:constraint (class ?class)
:def (= ?subs (setofall ?x (direct-subclass-of ?x ?class)))
:lisp-fun #'(lambda (class)
(let ((class-s (get-ocml-class class)))
(if class-s
(mapcar #'name (current-direct-subclasses class-s))))))
Contact Point
Email: John Domingue (j.b.domingue@open.ac.uk)
