;;; -*- Mode:Lisp; Syntax:Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-;;; If you load this file (with translation into the "KIF" implementation;;; -- the default ), then the definitions are saved on property lists;;; and can be used for online documentation and in cross-reference reports.(in-package "ONTOLINGUA-USER") ;inherits from the KIF package;all constants defined here are exported;from the KIF package.(define-theoryKIF-RELATIONS(kif-sets kif-lists) "The KIF vocabulary concerning relations and functions.") (in-theory 'kif-relations);;; Functions and relations are defined in the frame ontology.;;; Inserted here for completeness.(define-classRELATION(?r);;; REDEFINED-IN-FRAME-ONTOLOGY!:iff-def (and (set ?r) (forall ?x (=> (member ?x ?r) (list ?x))))) (define-classFUNCTION(?f);;; REDEFINED-IN-FRAME-ONTOLOGY!:iff-def (and (relation ?f) (forall (?l ?m) (=> (member ?l ?f) (member ?m ?f) (= (butlast ?l) (butlast ?m)) (= (last ?l) (last ?m)))))) (define-instanceBOTTOM(undefined) "The unique object which is the value of functions when applied to arguments on which they are not defined.") (define-relationHOLDS(?r @args) "If $\tau$ denotes a relation, then the sentence {\tt (holds $\tau$ $\tau_1$ ... $\tau_k$)} is true if and only if the list of objects denoted by $\tau_1$,...,$\tau_k$ is a member of that relation." :iff-def (and (relation ?r) (member (listof @args) ?r))) (define-functionVALUE(?f @args) "If $\tau$ denotes a function with a value for the objects denoted by $\tau_1$,..., $\tau_k$, then the term {\tt (value $\tau$ $\tau_1$ ... $\tau_k$)} denotes the value of applying that function to the objects denoted by $\tau_1$,...,$\tau_k$. Otherwise, the value is undefined." :lambda-body (if (and (function ?f) (member ?list ?f) (= (butlast ?list) (listof @args))) (last ?list))) (define-functionAPPLY(?f ?list) :lambda-body (if (and (function ?f) (= ?list (listof @args))) (value ?f @args))) (define-functionMAP(?f ?list) :lambda-body (if (null ?list) (listof) (cons (value ?f (first ?list)) (map ?f (rest ?list))))) (define-functionUNIVERSE(?r) :-> ?set "The universe of a relation is the set of all objects occurring in some list contained in that relation." :lambda-body (if (relation ?r) (setofall ?x (exists (?list) (and (member ?list ?r) (item ?x ?list)))))) (define-relationUNARY-RELATION(?r);;; REDEFINED-IN-FRAME-ONTOLOGY!"A unary relation is a non-empty relation in which all lists have exactly one item." :iff-def (and (relation ?r) (not (empty ?r)) (forall (?list) (=> (member ?list ?r) (single ?list))))) (define-relationBINARY-RELATION(?r);;; REDEFINED-IN-FRAME-ONTOLOGY!"A binary relation is a non-empty relation in which all lists have exactly two items." :iff-def (and (relation ?r) (not (empty ?r)) (forall (?list) (=> (member ?list ?r) (double ?list))))) (define-functionINVERSE(?r) :-> ?relation;;; REDEFINED-IN-FRAME-ONTOLOGY!"The inverse of a binary relation is a binary relation with all tuples reversed." :lambda-body (if (binary-relation ?r) (setofall (listof ?y ?x) (holds ?r ?x ?y)))) (define-functionCOMPOSITION(?r1 ?r2) :-> ?relation;;; REDEFINED-IN-FRAME-ONTOLOGY!"The composition of a binary relation $r_1$ and a binary relation $r_2$ is a binary relation in which an object $x$ is related to an object $z$ if and only if there is an object $y$ such that $x$ is related to $y$ by $r_1$ and $y$ is related to $z$ by $r_2$." :lambda-body (if (and (binary-relation ?r1) (binary-relation ?r2)) (setofall (listof ?x ?z) (exists (?y) (and (holds ?r1 ?x ?y) (holds ?r2 ?y ?z)))))) (define-relationONE-ONE(?r) :iff-def (and (binary-relation ?r) (function ?r) (function (inverse ?r)))) (define-relationMANY-ONE(?r) :iff-def (and (binary-relation ?r) (function ?r))) (define-relationONE-MANY(?r) :iff-def (and (binary-relation ?r) (function (inverse ?r)))) (define-relationMANY-MANY(?r) :iff-def (and (binary-relation ?r) (not (function ?r)) (not (function (inverse ?r))))) (define-relationUNARY-FUNCTION(?f) "A unary function is a function with a single argument and a single value. Hence, it is also a binary relation." :iff-def (and (function ?f) (binary-relation ?f))) (define-relationBINARY-FUNCTION(?f) "A binary function is a function with two arguments and one value. Hence, it is a relation with three arguments." :iff-def (and (function ?f) (not (empty ?f)) (forall (?list) (=> (member ?list ?f) (triple ?list)))))