;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-;;; Proposed new vocabulary for KIF.;;; They are merged into the appropriate parts of the KIF-ONTOLOGY;;; file.(in-package "ONTOLINGUA-USER") (define-theoryKIF-EXTENSIONS(kif-sets kif-lists kif-numbers kif-relations) "Definitions that extend KIF in obvious places.") (in-theory 'KIF-EXTENSIONS) (define-relationUNDEFINED(?value) "True of terms denoting the bottom object, usually meaning that a function is undefined on given arguments. There is exactly one object in the universe of discourse that is undefined, called BOTTOM. Functional terms that are undefined are equal to this special element." :iff-def (= ?value BOTTOM) :issues ("UNDEFINED is not in the KIF 3.0 spec, but is implicitly there.")) (define-relationDEFINED(?x) "A term is defined if it does not denote the undefined object, called bottom. (defined (F x)) means that the function F is defined for the object x. (F x) denotes its value. In relational terminology, (defined (F x)) means (exists ?y (F x ?y))." :iff-def (not (undefined ?x)) :issues ("DEFINED is not in the KIF 3.0 spec.")) (define-functionCARDINALITY(?set) :-> ?integer "Returns the number of elements in a set." :iff-def (and (set ?set) (exists @elements (and (= ?set (setof @elements)) (= ?integer (length (listof @elements)))))) :constraints (integer ?integer) :issues ("not explicitly defined in the KIF 3.0 spec")) (define-classFINITE-SET(?f-set) "A set that has only finite elements" :iff-def (and (set ?f-set) (exists @elements (= ?f-set (setof @elements)))) :issues ("not explicitly defined in the KIF 3.0 spec")) (define-functionIDENTITY(?x) "The value of the identity function is just its argument." :lambda-body ?x) (define-classPOSITIVE-INTEGER(?x) "An integer greater than zero, not including zero. A less ambiguous name for KIF's NATURAL." :iff-def (and (integer ?x) (> ?x 0))) (define-classNON-NEGATIVE-INTEGER(?x) "An integer greater than or equal to zero." :iff-def (and (integer ?x) (>= ?x 0))) (define-classSTRING(?s) "A string is a sequence of characters." :def (list ?s) :issues "STRING is not in the KIF 3.0 spec!") (define-functionLIST-TO-SET(?list) "denotes the set consisting of the elements of the list. Essentially removes duplicates and order information from the list." := (setofall ?x (item ?x ?list))) (define-functionSECOND-ITEM(?list) "returns the second item in the specified list. If the length of the list is 0 or 1, this function is undefined. This is different from Lisp's SECOND function, which returns NIL, which means both false and null list." := (if (and (list ?list) (not (null (rest ?list)))) (first (rest ?list))))