Ontology: Akt-Support-Ontology; Representation Language: ONTOLINGUA; File: basic

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.

;;;Automatically translated from OCML file #P"C:/users/jbd2/code/ocml/library/v5-0/domains/akt-support-ontology/basic.lisp"
(in-package "ONTOLINGUA-USER")

(in-ontology 'akt-support-ontology)


(Define-Relation = (?x ?y) 
"True if ?x and ?y do unify")


(Define-Relation == (?x ?y) 
"True if ?x and ?y do unify and they also have the same structure.
    This means that either they are both atoms, or they are lists with 
    the same structure")


(Define-Frame LIST  

  :own-slots
  (  (Documentation "A  class representing lists.")
  (Subclass-of intangible-thing))

  :axioms
((<=> (or (= ?x nil) (= ?x (?a . ?b))) (list ?x))
))


(Define-Individual NIL (list)
"The empty list"
)


(Define-Relation NULL (?l) 
"True if ?l is the empty list"
  :iff-def (= ?l nil))


(Define-Function FIRST (?l) 
"Takes the first element of a list.  If the list is empty
    the function returns :nothing"
:constraints (list ?l)
:lambda-body (if (== ?l (?a . ?b)) ?a :nothing))


(Define-Function REST (?l) 
"Takes a list as argument, say ?l, removes the first element of ?s
    and returns the resulting list.  If ?l = nil, then :nothing is returned"
:constraints (list ?l)
:lambda-body (if (== ?l (?a . ?b)) ?b :nothing))


(Define-Function LIST-OF (@els) 
"This is the primitive list constructor.  It is implemented in terms of
    the underlying LISP list construction primitive, LIST")


(Define-Function APPEND (?l1 @ls) 
"Appends together a number of lists. I cannot be bothered giving its operational
   spec...so you only get a lisp attachment"
:constraints (and (list ?l1) (every (list-of @ls) list)))


(Define-Function CONS (?el ?l) 
"Adds ?el to the beginning of list ?l.  
   Note that this cons is less generic than the lisp function with the same name.
   Here the 2nd argument must be a list (in lisp, it can also be an atom)."
:constraints (list ?l)
:lambda-body (append (list-of ?el) ?l))


(Define-Function LENGTH (?l) 
"Computes the number of elements in a list"
:constraints (list ?l)
:lambda-body (if (= ?l nil) 0 (if (== ?l (?first . ?rest)) (+ 1 (length ?rest)))))


(Define-Function REMOVE1 (?el ?l) 
"Removes the first occurrence of ?el in ?l and returns the resulting list.
   If ?el is not a member of ?l then the result is ?l"
:constraints (list ?l)
:lambda-body (if (= ?l nil) ?l (if (== ?l (?el . ?rest)) ?rest (if (== ?l (?first . ?rest)) (cons ?first (remove1 ?el ?rest))))))


(Define-Function REMOVE (?el ?l) 
"Removes all occurrences of ?el in ?l and returns the resulting list.
   If ?el is not a member of ?l then the result is ?l"
:constraints (list ?l)
:lambda-body (if (= ?l nil) ?l (if (== ?l (?el . ?rest)) (remove ?el ?rest) (if (== ?l (?first . ?rest)) (cons ?first (remove ?el ?rest))))))


(Define-Relation MEMBER (?el ?list) 
"A relation to check whether something is a member of a list"
  :iff-def (or (== ?list (?el . ?rest)) (and (== ?list (?first . ?rest)) (member ?el ?rest)))
  :constraints (list ?list))


(Define-Relation EVERY (?l ?rel) 
"True if for each term in ?l, say ?term, (holds ?rel ?term) is true.
   For instance, (every '(1 2 3) 'number) is satisfied, while 
   (every '(1 2 pippo) 'number) is not"
  :iff-def (or (= ?l nil) (and (== ?l (?first . ?rest)) (holds ?rel ?first) (every ?rest ?rel)))
  :constraints (unary-relation ?rel))


(Define-Function BUTLAST (?list) 
"Returns all the element of ?list, except the last one.
    If ?list = NIL, then :nothing is returned.  If ?list has
    length 1, then nil is returned"
:constraints (list ?l)
:lambda-body (cond ((null ?list) :nothing) ((null (rest ?list)) nil) ((true) (cons (first ?list) (butlast (rest ?list))))))


(Define-Function LAST (?list) 
"Returns the last element of a list.  If ?list is empty
    then :nothing is returned"
:constraints (list ?list)
:lambda-body (cond ((null ?list) :nothing) ((null (rest ?list)) (first ?list)) ((true) (last (rest ?list)))))


(Define-Function MAP (?fun @ls) 
:constraints (and (function ?fun) (every (list-of @ls) list))
:lambda-body (if (null (first (list-of @ls))) nil (cons (apply ?fun (map1 first (list-of @ls))) (apply map (cons ?fun (map1 rest (list-of @ls)))))))


(Define-Function MAP1 (?fun ?l) 
:constraints (and (function ?fun) (list ?l))
:lambda-body (if (null ?l) ?l (cons (call ?fun (first ?l)) (map1 ?fun (rest ?l)))))


(Define-Frame SET  

  :own-slots
  (  (Documentation "A set is something which is not an individual. In cyc sets are distinguished
   from collections.  Here we just use the term generically to refer to 
   something which denotes a collection of elements, whether abstract or
   concrete.
   Functions and relations represent sets. ")
  (Subclass-of intangible-thing)))


(Define-Axiom BASIC-SET-TYPES-ARE-DISJOINT  
"There are three basic types of sets in our ontology, functions
   relations and enumerated sets and these do not intersect"
:= (subclass-partition set (set-of function relation enumerated-set)))


(Define-Function SET-OF (@args) 
"This is the basic set constructor to create a set by enumerating its elements.
   For instance, (setof 1 2) denotes the set {1 2}.
   We represent such a set as a list whose first item is :set"
:lambda-body (cons :set (list-of @args)))


(Define-Frame ENUMERATED-SET  

  :own-slots
  (  (Documentation "A set represented as (:set-of el1 el_2...el_n), where no el_i is repeated")
  (Subclass-of set))

  :axioms
((<=> (and (= ?x (:set . ?elements)) (not (exists ?el (and (member ?el ?elements) (member ?el (remove1 ?el ?elements)))))) (enumerated-set ?x))
(=> (enumerated-set ?x) (list ?x))
))


(Define-Relation ELEMENT-OF (?el ?set) 
"A relation to check whether something is an element of a set.  
   Note that because functions and relations are sets, we can prove
   whether a tuple satisfies a relation or a function using ELEMENT-OF.
   For instance, (element-of '(1 2 3) '+) is satisfied because 
   1+2=3 - see definitions below for an operationalization of this approach")


(Define-Axiom ELEMENT-OF-ENUMERATED-SET  
  "An operationalization of element-of, which works with sets represented as lists."
  := 
  (=>   (And
   (enumerated-set ?l)
   (member ?el (rest ?l)))
    (element-of ?el ?l)
))


(Define-Axiom ELEMENT-OF-SET-AS-RELATION  
  "A tuple, say  is an element of relation r iff
   (holds r ti t2 t3) is satisfied"
  := 
  (=>   (And
   (relation ?rel)
   (list ?tuple)
   (sentence-holds (cons ?rel ?tuple)))
    (element-of ?tuple ?rel)
))


(Define-Axiom ELEMENT-OF-SET-AS-FUNCTION  
  "A tuple, say  is an element of function f iff
   (= (apply f ti t2) t3) is satisfied"
  := 
  (=>   (And
   (function ?fun)
   (list ?el)
   (= (last ?el) (apply ?fun (butlast ?el))))
    (element-of ?el ?fun)
))


(Define-Function UNION (@sets) 
:constraints (every (list-of @sets) set)
:lambda-body (apply set-of (setofall ?x (exists ?set (and (member ?set (list-of @sets)) (element-of ?x ?set))))))


(Define-Function INTERSECTION (@sets) 
:constraints (every (list-of @sets) set)
:lambda-body (in-environment ((?all apply union (list-of @sets))) (apply set-of (setofall ?x (and (element-of ?x ?all) (not (exists ?set (and (member ?set (list-of @sets)) (not (element-of ?x ?set))))))))))


(Define-Frame NUMBER  

  :own-slots
  (  (Documentation "The class of all numbers")
  (Subclass-of quantity)))


(Define-Frame REAL-NUMBER  

  :own-slots
  (
  (Subclass-of number)))


(Define-Frame INTEGER  

  :own-slots
  (
  (Subclass-of real-number)))


(Define-Relation < (?x ?y) 
"A predicate to test whether a number is less than another"
  :constraints (and (number ?x) (number ?y)))


(Define-Relation > (?x ?y) 
"A predicate to test whether a number is greater than another"
  :constraints (and (number ?x) (number ?y)))


(Define-Frame POSITIVE-NUMBER  

  :own-slots
  (
  (Subclass-of number))

  :axioms
((<=> (and (number ?x) (> ?x 0)) (positive-number ?x))
))


(Define-Frame NEGATIVE-NUMBER  

  :own-slots
  (
  (Subclass-of number))

  :axioms
((<=> (and (number ?x) (< ?x 0)) (negative-number ?x))
))


(Define-Frame NON-NEGATIVE-NUMBER  

  :own-slots
  (
  (Subclass-of number))

  :axioms
((<=> (and (number ?x) (not (negative-number ?x))) (non-negative-number ?x))
))


(Define-Axiom POS-NEG-NUMBERS-EXHAUSTIVE-PARTITION  
:= (exhaustive-subclass-partition number (set-of positive-number negative-number)))


(Define-Frame POSITIVE-INTEGER  

  :own-slots
  (
  (Subclass-of integer))

  :axioms
((<=> (and (integer ?x) (> ?x 0)) (positive-integer ?x))
))


(Define-Frame NEGATIVE-INTEGER  

  :own-slots
  (
  (Subclass-of integer))

  :axioms
((<=> (and (integer ?x) (< ?x 0)) (negative-integer ?x))
))


(Define-Frame NON-NEGATIVE-INTEGER  

  :own-slots
  (
  (Subclass-of integer))

  :axioms
((<=> (and (integer ?x) (not (negative-integer ?x))) (non-negative-integer ?x))
))


(Define-Function + (?x @y) 
"Adds numbers"
:constraints (and (number ?x) (number (list-of @y))))


(Define-Function * (?x ?y) 
"Multiplies numbers"
:constraints (and (number ?x) (number ?y)))


(Define-Function SQUARE (?x) 
:constraints (number ?x)
:lambda-body (* ?x ?x))


(Define-Function - (?x @y) 
"Subtracts numbers"
:constraints (and (number ?x) (number (list-of @y))))


(Define-Function / (?x ?y) 
"Divides numbers"
:constraints (and (number ?x) (number ?y)))


(Define-Function LOG (?number ?base)) 


(Define-Function ROUND (?number) :-> ?int 
:def (integer ?int))


(Define-Frame STRING  

  :own-slots
  (  (Documentation "A primitive class representing strings")
  (Subclass-of individual)
  (Subclass-of intangible-thing)))


(Define-Frame RELATION  

  :own-slots
  (  (Documentation "The class of defined relations.  We assume fixed arity")
  (Subclass-of set)))


(Define-Frame UNARY-RELATION  

  :own-slots
  (
  (Subclass-of relation))

  :axioms
((<=> (and (relation ?r) (= (arity ?r) 1)) (unary-relation ?r))
))


(Define-Frame BINARY-RELATION  

  :own-slots
  (
  (Subclass-of relation))

  :axioms
((<=> (and (relation ?r) (= (arity ?r) 2)) (binary-relation ?r))
))


(Define-Relation TRUE nil 
"This is always satisfied")


(Define-Relation FALSE nil 
"This is never satisfied")


(Define-Function ARITY (?x) 
"The arity of a function or relation.  If a function or relation
   has variable arity, then we treat the last argument as if it were
   a sequence variable.  For instance the argument list for + is
   (?x &rest ?y).  In this case we say that + has arity 2.
   It is important to note that OCML does not support relations with variable
   arity.  The only exception is HOLDS, which has variable arity and is built in
   the OCML proof system"
:constraints (or (function ?x) (relation ?x))
:lambda-body (in-environment ((?l the-schema ?x) (?n length ?l)) (if (every ?l variable) ?n (- ?n 1))))


(Define-Relation VARIABLE (?x) 
"True of an OCML variable")


(Define-Relation VARIABLE-BOUND (?var) 
"True if ?var is  bound in teh current environment")


(Define-Function THE-SCHEMA (?x) 
"The schema of a function or relation"
:constraints (or (function ?x) (relation ?x))
:lambda-body (if (relation ?x) (relation-schema ?x) (if (function ?x) (function-schema ?x) :nothing)))


(Define-Function FUNCTION-SCHEMA (?f) 
:constraints (function ?f))


(Define-Function RELATION-SCHEMA (?rel) 
:constraints (relation ?rel))


(Define-Relation HOLDS (?rel &rest ?args) 
"A meta-level relation which is true iff the sentence (?rel . ?args) is true.
   The length of ?args must be consistent with the arity of the relation"
  :constraints (and (relation ?r) (= (arity ?rel) (length ?args))))


(Define-Relation SENTENCE-HOLDS (?sentence) 
"The same as HOLDS, but takes only one argument, a sentence whose truth
   value is to be checked"
  :constraints (and (== ?sentence (?rel . ?args)) (relation ?rel) (= (arity ?rel) (length ?args))))


(Define-Frame FUNCTION  

  :own-slots
  (  (Documentation "The class of all defined functions")
  (Subclass-of set)))


(Define-Function APPLY (?f ?args) 
"(apply f (arg1 .....argn)) is the same as 
   (f arg1 ....argn)"
:constraints (and (function ?f) (list ?args)))

Contact Point