;;; -*- 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-theory KIF-EXTENSIONS (kif-sets kif-lists kif-numbers kif-relations)
  "Definitions that extend KIF in obvious places.")

(in-theory 'KIF-EXTENSIONS)

(define-relation UNDEFINED (?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-relation DEFINED (?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-function CARDINALITY (?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-class FINITE-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-function IDENTITY (?x)
  "The value of the identity function is just its argument."
  :lambda-body ?x)


(define-class POSITIVE-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-class NON-NEGATIVE-INTEGER (?x)
  "An integer greater than or equal to zero."

  :iff-def (and (integer ?x)
                (>= ?x 0)))

(define-class STRING (?s)
  "A string is a sequence of characters."
  :def (list ?s)
  :issues "STRING is not in the KIF 3.0 spec!")

(define-function LIST-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-function SECOND-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))))