|
Generated by diff2html © Yves Bailly, MandrakeSoft S.A. 2001 diff2html is licensed under the GNU GPL. |
| support-v2.1/frames.lisp | support-v2.2/frames.lisp | ||||
|---|---|---|---|---|---|
|
114 lines 4651 bytes Last modified : Wed Jun 29 13:32:30 2005 |
114 lines 4684 bytes Last modified : Wed Jun 29 13:34:04 2005 |
||||
| 1 | ;;; -*- Mode: LISP; Syntax: Common-lisp; Base: 10; Package: OCML; -*- | 1 | ;;; -*- Mode: LISP; Syntax: Common-lisp; Base: 10; Package: OCML; -*- | ||
| 2 | 2 | ||||
| 3 | (in-package "OCML") | 3 | (in-package "OCML") | ||
| 4 | 4 | ||||
| 5 | (in-ontology akt-support-ontology) | 5 | (in-ontology akt-support-ontology) | ||
| 6 | 6 | ||||
| 7 | ;;;here I have defined a few basic notions we need to have to talk about frame-based models | 7 | ;;;here I have defined a few basic notions we need to have to talk about frame-based models | ||
| 8 | 8 | ||||
| 9 | (def-class CLASS (unary-relation) | 9 | (def-class CLASS (unary-relation) | ||
| 10 | "The class of all classes. We consider a class as a unary relation, true for all its instances" | 10 | "The class of all classes. We consider a class as a unary relation, true for all its instances" | ||
| 11 | :lisp-fun #'(lambda (x env) | 11 | :lisp-fun #'(lambda (x env) | ||
| 12 | (let ((y (unbound-variable? x env))) | 12 | (let ((y (unbound-variable? x env))) | ||
| 13 | (if y | 13 | (if y | ||
| 14 | (mapcar #'(lambda (rel) | 14 | (mapcar #'(lambda (rel) | ||
| 15 | (cons (cons y rel) env)) | 15 | (cons (cons y rel) env)) | ||
| 16 | (all-ocml-classes)) | 16 | (all-ocml-classes)) | ||
| 17 | (if (get-ocml-class | 17 | (if (get-ocml-class | ||
| 18 | (instantiate x env)) | 18 | (instantiate x env)) | ||
| 19 | (list env) | 19 | (list env) | ||
| 20 | :fail))))) | 20 | :fail))))) | ||
| 21 | 21 | ||||
| 22 | (def-class CLASS-PARTITION (enumerated-set) ?set-of-classes | 22 | (def-class CLASS-PARTITION (enumerated-set) ?set-of-classes | ||
| 23 | "A set of mutually disjoint classes. Disjointness of | 23 | "A set of mutually disjoint classes. Disjointness of | ||
| 24 | classes is a special case of disjointness of sets." | 24 | classes is a special case of disjointness of sets." | ||
| 25 | :constraint (enumerated-set ?set-of-classes) | 25 | :constraint (enumerated-set ?set-of-classes) | ||
| 26 | :iff-def (and (enumerated-set ?set-of-classes) | 26 | :iff-def (and (enumerated-set ?set-of-classes) | ||
| 27 | (forall ?C | 27 | (forall ?C | ||
| 28 | (=> (element-of ?C ?set-of-classes) | 28 | (=> (element-of ?C ?set-of-classes) | ||
| 29 | (class ?C))) | 29 | (class ?C))) | ||
| 30 | (forall (?C1 ?C2) | 30 | (forall (?C1 ?C2) | ||
| 31 | (=> (and (element-of ?C1 ?set-of-classes) | 31 | (=> (and (element-of ?C1 ?set-of-classes) | ||
| 32 | (element-of ?C2 ?set-of-classes) | 32 | (element-of ?C2 ?set-of-classes) | ||
| 33 | (not (= ?C1 ?C2))) | 33 | (not (= ?C1 ?C2))) | ||
| 34 | (forall (?i) | 34 | (forall (?i) | ||
| 35 | (=> (instance-of ?i ?C1) | 35 | (=> (instance-of ?i ?C1) | ||
| 36 | (not (instance-of ?i ?C2))))))) | 36 | (not (instance-of ?i ?C2))))))) | ||
| 37 | :avoid-infinite-loop t) | 37 | :avoid-infinite-loop t) | ||
| 38 | 38 | ||||
| 39 | 39 | ||||
| 40 | (def-relation SUBCLASS-PARTITION (?C ?class-partition) | 40 | (def-relation SUBCLASS-PARTITION (?C ?class-partition) | ||
| 41 | "A subclass-partition of a class C is a set of | 41 | "A subclass-partition of a class C is a set of | ||
| 42 | subclasses of C that are mutually disjoint." | 42 | subclasses of C that are mutually disjoint." | ||
| 43 | :iff-def (and (class ?C) | 43 | :iff-def (and (class ?C) | ||
| 44 | (class-partition ?class-partition) | 44 | (class-partition ?class-partition) | ||
| 45 | (forall ?subclass | 45 | (forall ?subclass | ||
| 46 | (=> (element-of ?subclass ?class-partition) | 46 | (=> (element-of ?subclass ?class-partition) | ||
| 47 | (subclass-of ?subclass ?C))))) | 47 | (subclass-of ?subclass ?C))))) | ||
| 48 | 48 | ||||
| 49 | (def-relation EXHAUSTIVE-SUBCLASS-PARTITION (?C ?class-partition) | 49 | (def-relation EXHAUSTIVE-SUBCLASS-PARTITION (?C ?class-partition) | ||
| 50 | "A subrelation-partition of a class C is a set of | 50 | "A subrelation-partition of a class C is a set of | ||
| 51 | mutually-disjoint classes (a subclass partition) which covers C. | 51 | mutually-disjoint classes (a subclass partition) which covers C. | ||
| 52 | Every instance of C is is an instance of exactly one of the subclasses | 52 | Every instance of C is is an instance of exactly one of the subclasses | ||
| 53 | in the partition." | 53 | in the partition." | ||
| 54 | :iff-def (and (subclass-partition ?C ?class-partition) | 54 | :iff-def (and (subclass-partition ?C ?class-partition) | ||
| 55 | (forall ?instance | 55 | (forall ?instance | ||
| 56 | (=> (instance-of ?instance ?C) | 56 | (=> (instance-of ?instance ?C) | ||
| 57 | (exists ?subclass | 57 | (exists ?subclass | ||
| 58 | (and (element-of ?subclass ?class-partition) | 58 | (and (element-of ?subclass ?class-partition) | ||
| 59 | (instance-of ?instance ?subclass))))))) | 59 | (instance-of ?instance ?subclass))))))) | ||
| 60 | 60 | ||||
| 61 | (def-relation INSTANCE-OF (?x ?c) | 61 | (def-relation INSTANCE-OF (?x ?c) | ||
| 62 | "This definition relates the notion of 'being an instance' to the notion | 62 | "This definition relates the notion of 'being an instance' to the notion | ||
| 63 | of satisfying a relation: ?I is an instance of a class ?c, | 63 | of satisfying a relation: ?I is an instance of a class ?c, | ||
| 64 | iff (holds ?I ?c) is true" | 64 | iff (holds ?I ?c) is true" | ||
| 65 | :constraint (class ?c) | 65 | :constraint (class ?c) | ||
| 66 | :iff-def (and (class ?c) | 66 | :iff-def (and (class ?c) | ||
| 67 | (holds ?c ?x))) | 67 | (holds ?c ?x))) | ||
| 68 | 68 | ||||
| 69 | (def-relation SUBCLASS-OF (?sub ?c) | 69 | (def-relation SUBCLASS-OF (?sub ?c) | ||
| 70 | "?sub is a subclass of ?c if every instance of ?sub is also an instance of | 70 | "?sub is a subclass of ?c if every instance of ?sub is also an instance of | ||
| 71 | ?c. Note that according to this definition every class is a subclass of itself" | 71 | ?c. Note that according to this definition every class is a subclass of itself" | ||
| 72 | 72 | ||||
| 73 | :constraint (and (class ?sub)(class ?c)) | 73 | :constraint (and (class ?sub)(class ?c)) | ||
| 74 | 74 | ||||
| 75 | :prove-by (or (and (variable-bound ?sub) | 75 | :prove-by (or (and (variable-bound ?sub) | ||
| 76 | (member ?c (all-superclasses ?sub))) | 76 | (member ?c (all-superclasses ?sub))) | ||
| 77 | (and (variable-bound ?c) | 77 | (and (variable-bound ?c) | ||
| 78 | (member ?sub (all-subclasses ?c))) | 78 | (member ?sub (all-subclasses ?c))) | ||
| 79 | (and | 79 | (and | ||
| 80 | (not (variable-bound ?c)) | 80 | (not (variable-bound ?c)) | ||
| 81 | (not (variable-bound ?sub)) | 81 | (not (variable-bound ?sub)) | ||
| 82 | (class ?sub1)(class ?super1) | 82 | (class ?sub1)(class ?super1) | ||
| 83 | (subclass-of ?sub1 ?super1))) | 83 | (subclass-of ?sub1 ?super1))) | ||
| 84 | 84 | ||||
| 85 | :iff-def (and (class ?sub) (class ?c) | 85 | :iff-def (and (class ?sub) (class ?c) | ||
| 86 | (forall ?inst | 86 | (forall ?inst | ||
| 87 | (=> (instance-of ?inst ?sub) | 87 | (=> (instance-of ?inst ?sub) | ||
| 88 | (instance-of ?inst ?c)))) | 88 | (instance-of ?inst ?c)))) | ||
| 89 | :no-proofs-by (:iff-def)) | 89 | :no-proofs-by (:iff-def)) | ||
| 90 | 90 | ||||
| 91 | (def-function ALL-SUPERCLASSES (?class) -> ?supers | 91 | (def-function ALL-SUPERCLASSES (?class) -> ?supers | ||
| 92 | "returns all superclasses of a class" | 92 | "returns all superclasses of a class" | ||
| 93 | :constraint (class ?class) | 93 | :constraint (class ?class) | ||
| 94 | :def (forall ?super (<=> (member ?super ?supers) | 94 | :def (forall ?super (<=> (member ?super ?supers) | ||
| 95 | (subclass-of ?class ?super))) | 95 | (subclass-of ?class ?super))) | ||
| 96 | :lisp-fun #'(lambda (class) | 96 | :lisp-fun #'(lambda (class) | ||
| 97 | (let ((class-s (get-ocml-class class))) | 97 | (let ((class-s (get-ocml-class class))) | ||
| 98 | (if class-s | 98 | (if class-s | ||
| 99 | (mapcar #'name (domain-superclasses class-s)))))) | 3d) | 99 | (cons class-s (mapcar #'name (domain-superclasses class-s))))))) | |
| 100 | 100 | ||||
| 101 | (def-function ALL-SUBCLASSES (?class) -> ?subs | 101 | (def-function ALL-SUBCLASSES (?class) -> ?subs | ||
| 102 | "returns all subclasses of a class" | 102 | "returns all subclasses of a class" | ||
| 103 | :constraint (class ?class) | 103 | :constraint (class ?class) | ||
| 104 | :def (forall ?sub (<=> (member ?sub ?subs) | 104 | :def (forall ?sub (<=> (member ?sub ?subs) | ||
| 105 | (subclass-of ?sub ?class))) | 105 | (subclass-of ?sub ?class))) | ||
| 106 | :lisp-fun #'(lambda (class) | 106 | :lisp-fun #'(lambda (class) | ||
| 107 | (let ((class-s (get-ocml-class class))) | 107 | (let ((class-s (get-ocml-class class))) | ||
| 108 | (if class-s | 108 | (if class-s | ||
| 109 | (mapcar #'name (current-subclasses class-s)))))) | 3d) | 109 | (cons class-s (mapcar #'name (current-subclasses class-s))))))) | |
| 110 | 110 | ||||
| 111 | 111 | ||||
| 112 | 112 | ||||
| 113 | 113 | ||||
| 114 | 114 |