SUO: Starter Ontology Version 2
To one and all,
I include my current draft of this work-in-progress, to let
the group see where it has gone, and determine if the direction
I am going is the way the group wishes to progress.
David (whitten@lynx.eaze.net) (713) 791-1414 ext 6116
Starter Structural Ontology Version 2.
vocabulary of KIF in the ontology
for which no rules have been stated
= equality between two terms
\= inequality between terms
not negation
and conjunction of two conjucts
or disjunction of two disjuncts
=> implication of antecedents and consequent
<= reverse implication of consequent and antecedants
<=> equivalence between two sentences
forall universal quantifier> exists existential quantifier
bottom the value of a partial when that function is applied
to arguments for which the function make no sense
true truth value of assertions that hold
false truth value of assertions that do not hold
Possibly needed Set Relations (but undefined)
intersection, union, partition, complement
Relations in Starter KB:
(INSTANCE-OF ?INS ?TYPE)
- ?INS is an individual which is
a member of class ?TYPE
(SUBCLASS-OF ?SUBTYPE ?TYPE)
- ?SUBTYPE is a class which is a
subclass of class ?TYPE
(NTH-DOMAIN ?REL ?POS ?TYPE)
- the argument in position ?POS
of relation ?REL is a member of class ?TYPE.
?POS=0 is used for the return type
of functional relations.
(NTH-SUBCLASS ?REL ?POS ?TYPE)
- the argument in position ?POS
of relation ?REL is a subclass of class ?TYPE.
?POS=0 is used for the return type
of functional relations
(VALENCE ?REL ?COUNT)
- the COUNT of arguments that the
relation ?REL can take is the number ?COUNT
Note: an assertion is not stated when a
relation can take an arbitrary NUMBER of arguments
(LENGTH ?ASRT ?COUNT)
- the count of arguments that are present
in the assertion ?ASRT is the number ?COUNT.
?COUNT=0 is used for an assertion with
only the relation present.
(NTH-ARGUMENT ?A ?P ?I)
- the argument in position ?P in the
assertion ?A is the individual ?I.
?P=0 is used for the individual
representing the relation of the assertion.
(NTH-ARGUMENT-NAME ?R ?P ?S)
- the documented preferred name of the variable
in position ?P used in expressing assertions
with relation ?R expressed as a string ?S.
(NAME-OF ?INS ?NAME)
- A name of the individual ?INS as a string ?NAME
?NAME cannot be the empty string.
two assertions in the same context cannot
have the same string as a name.
(AUTHOR ?INS ?WHO)
- the name of the person as a string ?WHO who added
the individual ?INS to the Standard Upper Ontology
(REVISION ?INS ?ID)
- the revision identified by the string ?ID is the
initial one in which the individual ?INS was part
of the Standard Upper Ontology
(TRANSITIVE-THROUGH ?REL-BASE ?REL-PIPE)
- the relation ?REL-BASE is transitive through
the relation ?REL-PIPE.
(NUM-SUCC ?NUM-PREV ?NUM-NEXT)
- the number ?NUM-PREV
is immediately followed by
?NUM-NEXT in numerical order
(NUM-< ?NUM-PREV ?NUM-NEXT)
- the number ?NUM-PREV
is eventually followed by
?NUM-NEXT in numerical order
Constants in Starter KB:
TOP
- the uppermost element in the ontology
RELATION
- class of RELATIONs used in an assertion
intuitively, all 'slots' or 'properties' or
'relationships' or 'predicates'
POSITION
- class of positions in an assertion
INDIVIDUAL
- class of individuals in the KB which
are the possible values of variables.
coextensional with TOP
CLASS
- class of individuals which identify
subsets of TOP.
NUMBER
- class of individuals which are
expressed in numeric format
COUNT
- class of numeric individuals
expressing a quantity.
ASSERTION
- class of all assertions
expressing a sentence
Rules:
R001:
(forall (?ANY)
(= ?ANY ?ANY))
R002:
(forall (?ANY)
(not (\= ?ANY ?ANY)))
R003:
(forall (?X ?Y)
(not (and
(= ?ANY ?ANY)
(\= ?X ?Y))))
;;Leibnitz's Rule
R004:
(forall (?X ?Y ?REL ?POS)
(=>
(= ?X ?Y)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT ?POS ?X)
(NTH-ARGUMENT ?ASRT ?POS ?Y))))
R004: ;; Everything is an instance of "TOP"
(forall (?ANY)
(INSTANCE-OF ?ANY TOP))
R005: ;; There exists something
(exists (?ONE)
(INSTANCE-OF ?ONE TOP))
R006: ;;Every class is a subclass of "TOP".
(forall (?TYPE)
(=>
(INSTANCE-OF ?TYPE CLASS)
(SUBCLASS-OF ?TYPE TOP)))
R007: ;; "TOP" must be an instance of CLASS
(INSTANCE-OF TOP CLASS)
;(NTH-DOMAIN ?REL ?POS ?TYPE)
; - the argument in position ?POS
; of relation ?REL is a member of class ?TYPE.
; ?POS=0 is used for the return type
; of functional relations.
;; define signature of "NTH-DOMAIN" relation
R008: (NTH-DOMAIN NTH-DOMAIN 1 RELATION)
R009: (NTH-DOMAIN NTH-DOMAIN 2 POSITION)
R010: (NTH-DOMAIN NTH-DOMAIN 3 CLASS)
R011: (NTH-ARGUMENT-NAME NTH-DOMAIN 1 "?REL")
R012: (NTH-ARGUMENT-NAME NTH-DOMAIN 2 "?POS")
R013: (NTH-ARGUMENT-NAME NTH-DOMAIN 3 "?TYPE")
R014: (VALENCE NTH-DOMAIN 3)
R015: (INSTANCE-OF NTH-DOMAIN RELATION)
R016: ;; define NTH-DOMAIN
(forall (?INS ?TYPE ?REL ?POS ?ASRT)
(=>
(INSTANCE-OF ?INS INDIVIDUAL)
(INSTANCE-OF ?TYPE CLASS)
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?POS POSITION)
(INSTANCE-OF ?ASRT ASSERTION)
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT ?POS ?INS)
(INSTANCE-OF ?INS ?TYPE)
(NTH-DOMAIN ?REL ?POS ?TYPE)
))
;(NTH-ARGUMENT-NAME ?R ?P ?S)
; - the documented preferred name of the variable
; in position ?P used in expressing assertions
; with relation ?R expressed as a string ?S.
;; define signature of "NTH-ARGUMENT-NAME" relation
R017: (NTH-DOMAIN NTH-ARGUMENT-NAME 1 ASSERTION)
R018: (NTH-DOMAIN NTH-ARGUMENT-NAME 2 POSITION)
R019: (NTH-DOMAIN NTH-ARGUMENT-NAME 3 STRING)
R020: (NTH-ARGUMENT-NAME NTH-ARGUMENT-NAME 1 "?ASRT")
R021: (NTH-ARGUMENT-NAME NTH-ARGUMENT-NAME 2 "?POS")
R022: (NTH-ARGUMENT-NAME NTH-ARGUMENT-NAME 3 "?STR")
R023: (VALENCE NTH-ARGUMENT-NAME 3)
R024: (INSTANCE-OF NTH-ARGUMENT-NAME RELATION)
;(AUTHOR ?INS ?WHO)
; - the name of the person as a string ?WHO who added
; the individual ?INS to the Standard Upper Ontology
;; define signature of "AUTHOR" relation
R025: (NTH-DOMAIN AUTHOR 1 ASSERTION)
R026: (NTH-DOMAIN AUTHOR 2 STRING)
R027: (NTH-ARGUMENT-NAME AUTHOR 1 "?INS")
R028: (NTH-ARGUMENT-NAME AUTHOR 2 "?WHO")
R029: (VALENCE AUTHOR 2)
R030: (INSTANCE-OF AUTHOR RELATION)
R031:
(forall (?INS ?STR)
(=> (AUTHOR ?INS ?STR)
(\= ?STR "")))
;(NAME-OF ?INS ?NAME)
; - A name of the individual ?INS as a string ?NAME
; ?NAME cannot be the empty string.
; two assertions in the same context cannot
; have the same string as a name.
;; define signature of "NAME-OF" relation
R032: (NTH-DOMAIN NAME-OF 1 INDIVIDUAL)
R033: (NTH-DOMAIN NAME-OF 2 STRING)
R034: (NTH-ARGUMENT-NAME NAME-OF 1 "?INS")
R035: (NTH-ARGUMENT-NAME NAME-OF 2 "?NAME")
R036: (VALENCE NAME-OF 2)
R037: (INSTANCE-OF NAME-OF RELATION)
R038:
(forall (?INS ?STR)
(=> (NAME-OF ?INS ?STR)
(\= ?STR "")))
R039: two individuals can't have the same name
(forall (?INS-1 ?INS-2 ?STR)
(not
(and
(\= ?INS-1 ?INS-2)
(NAME-OF ?INS-1 STR)
(NAME-OF ?INS-2 STR)
)
)
)
;ASSERTION
; - class of all assertions
; expressing a sentence
R040: (INSTANCE-OF ASSERTION CLASS)
R041: (SUBCLASS-OF ASSERTION INDIVIDUAL)
;(NTH-SUBCLASS ?REL ?POS ?TYPE)
; - the argument in position ?POS
; of relation ?REL is a subclass of class ?TYPE.
; ?POS=0 is used for the return type
; of functional relations
;; define signature of "NTH-SUBCLASS" relation
R041: (NTH-DOMAIN NTH-SUBCLASS 1 RELATION)
R042: (NTH-DOMAIN NTH-SUBCLASS 2 POSITION)
R043: (NTH-DOMAIN NTH-SUBCLASS 3 CLASS)
R044: (NTH-ARGUMENT-NAME NTH-SUBCLASS 1 "?REL")
R045: (NTH-ARGUMENT-NAME NTH-SUBCLASS 2 "?POS")
R046: (NTH-ARGUMENT-NAME NTH-SUBCLASS 3 "?TYPE")
R047: (VALENCE NTH-SUBCLASS 3)
R048: (INSTANCE-OF NTH-SUBCLASS RELATION)
R049: ;;definition
(forall (?SUBTYPE ?TYPE ?REL ?POS ?ASRT)
(=>
(INSTANCE-OF ?SUBTYPE CLASS)
(INSTANCE-OF ?TYPE CLASS)
(INSTANCE-OF ?POS POSITION)
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(/= ?POS 0)
(SUBCLASS-OF ?SUBTYPE ?TYPE)
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT ?POS ?INS)
(NTH-SUBCLASS ?REL ?POS ?TYPE)
))
;(INSTANCE-OF ?INS ?TYPE)
; - ?INS is an individual which is
; a member of class ?TYPE
;; define signature of "INSTANCE-OF" relation
R050: (NTH-DOMAIN INSTANCE-OF 1 INDIVIDUAL)
R051: (NTH-DOMAIN INSTANCE-OF 2 CLASS)
R052: (NTH-ARGUMENT-NAME INSTANCE-OF 1 "?INS")
R053: (NTH-ARGUMENT-NAME INSTANCE-OF 2 "?TYPE")
R054: (VALENCE INSTANCE-OF 2)
R055: (INSTANCE-OF INSTANCE-OF RELATION)
R056: ;; INSTANCE-OF is transitive through SUBCLASS-OF.
(TRANSITIVE-THROUGH INSTANCE-OF SUBCLASS-OF)
;(SUBCLASS-OF ?SUBTYPE ?SUPERTYPE)
; - ?SUBTYPE is a class which is a
; subclass of class ?SUPERTYPE
;; define signature of "SUBCLASS-OF" relation
R057: (NTH-DOMAIN SUBCLASS-OF 1 CLASS)
R058: (NTH-DOMAIN SUBCLASS-OF 2 CLASS)
R059: (NTH-ARGUMENT-NAME SUBCLASS-OF 1 "?SUBTYPE")
R060: (NTH-ARGUMENT-NAME SUBCLASS-OF 2 "?SUPERTYPE")
R061: (VALENCE SUBCLASS-OF 2)
R062: (INSTANCE-OF SUBCLASS-OF RELATION)
R063: ;; SUBCLASS-OF is transitive through SUBCLASS-OF.
(TRANSITIVE-THROUGH INSTANCE-OF SUBCLASS-OF)
R064: ;definition
(forall (?SUBTYPE ?SUPERTYPE)
(=>
(INSTANCE-OF ?SUBTYPE CLASS)
(INSTANCE-OF ?SUPERTYPE CLASS)
(<=>
(SUBCLASS-OF ?SUB ?SUPER)
(forall (?INS)
(=>
(INSTANCE-OF ?INS ?SUB)
(INSTANCE-OF ?INS ?SUPER)
)
)
)
)
)
;(TRANSITIVE-THROUGH ?REL-BASE ?REL-PIPE)
; - the relation ?REL-BASE is transitive through
; the relation ?REL-PIPE
R065: (NTH-DOMAIN TRANSITIVE-THROUGH 1 RELATION)
R066: (NTH-DOMAIN TRANSITIVE-THROUGH 2 RELATION)
R067: (NTH-ARGUMENT-NAME TRANSITIVE-THROUGH 1 "?REL-BASE")
R068: (NTH-ARGUMENT-NAME TRANSITIVE-THROUGH 2 "?REL-PIPE")
R069: (VALENCE TRANSITIVE-THROUGH 2)
R070: (INSTANCE-OF TRANSITIVE-THROUGH RELATION)
R071:
(forall (?REL-BASE ?REL-PIPE ?X ?Y ?TBASE ?TPIPE-1 ?TPIPE-2 ?TSUPER)
(<=> (TRANSITIVE-THROUGH ?REL-BASE ?REL-PIPE)
(=>
(INSTANCE-OF ?RBASE RELATION)
(INSTANCE-OF ?RPIPE RELATION)
(NTH-DOMAIN ?RBASE 1 ?TBASE)
(NTH-DOMAIN ?RBASE 2 ?TPIPE1)
(NTH-DOMAIN ?RPIPE 1 ?TPIPE2)
(NTH-DOMAIN ?RPIPE 2 ?TSUPER)
(INSTANCE-OF ?X ?TBASE)
(INSTANCE-OF ?Y ?TPIPE1)
(INSTANCE-OF ?Y ?TPIPE2)
(INSTANCE-OF ?Z ?TSUPER)
(INSTANCE-OF ?Z ?TPIPE1)
(?RBASE ?X ?Y)
(?RPIPE ?Y ?Z)
(?RBASE ?X ?Y)
)
)
)
R072: ;; "CLASS" is an instance of CLASS
(INSTANCE-OF CLASS CLASS)
R073: ;; All Classes are subclasses of themselves
(forall (?TYPE)
(=>
(INSTANCE-OF ?TYPE CLASS)
(SUBCLASS-OF ?TYPE ?TYPE)
)
)
R074: ;; "RELATION" is an instance of CLASS
(INSTANCE-OF RELATION CLASS)
R075: ;; RELATION is the class of individual relations
(SUBCLASS-OF RELATION INDIVIDUAL)
;;The class of individuals is a class
R076: (INSTANCE-OF INDIVIDUAL CLASS)
;; all numbers are individuals
R077:(SUBCLASS-OF NUMBER INDIVIDUAL)
R078: (SUBCLASS-OF NUMBER POSITION)
R079: (INSTANCE-OF POSITION CLASS)
R080: (SUBCLASS-OF NUMBER COUNT)
R081: (INSTANCE-OF COUNT CLASS)
;; the NUMBERs 0 thru 10
R082: (INSTANCE-OF 0 NUMBER)
R083: (INSTANCE-OF 1 NUMBER)
R084: (INSTANCE-OF 2 NUMBER)
R085: (INSTANCE-OF 3 NUMBER)
R086: (INSTANCE-OF 4 NUMBER)
R087: (INSTANCE-OF 5 NUMBER)
R088: (INSTANCE-OF 6 NUMBER)
R089: (INSTANCE-OF 7 NUMBER)
R090: (INSTANCE-OF 8 NUMBER)
R091: (INSTANCE-OF 9 NUMBER)
R092: (INSTANCE-OF 10 NUMBER)
;(NUM-SUCC ?NUM-PREV ?NUM-NEXT)
; - the number ?NUM-PREV
; is immediately followed by
; ?NUM-NEXT in numerical order
;; define signature of "NUM-SUCC" relation
R093: (NTH-DOMAIN NUM-SUCC 1 NUMBER)
R094: (NTH-DOMAIN NUM-SUCC 2 NUMBER)
R095: (NTH-ARGUMENT-NAME NUM-SUCC 1 "?NUM-PREV")
R096: (NTH-ARGUMENT-NAME NUM-SUCC 2 "?NUM-NEXT")
R097: (VALENCE NUM-SUCC 2)
R098: (INSTANCE-OF NUM-SUCC RELATION)
R099: (NUM-SUCC 0 1)
R100: (NUM-SUCC 1 2)
R101: (NUM-SUCC 2 3)
R102: (NUM-SUCC 3 4)
R103: (NUM-SUCC 4 5)
R104: (NUM-SUCC 5 6)
R105: (NUM-SUCC 6 7)
R106: (NUM-SUCC 7 8)
R107: (NUM-SUCC 8 9)
R108: (NUM-SUCC 9 10)
;(NUM-< ?NUM-PREV ?NUM-NEXT)
; - the number ?NUM-PREV
; is eventually followed by
; ?NUM-NEXT in numerical order
;; define signature of "NUM-<" relation
R109: (NTH-DOMAIN NUM-< 1 NUMBER)
R110: (NTH-DOMAIN NUM-< 2 NUMBER)
R111: (NTH-ARGUMENT-NAME NUM-< 1 "?NUM-PREV")
R112: (NTH-ARGUMENT-NAME NUM-< 2 "?NUM-NEXT")
R113: (VALENCE NUM-< 2)
R114: (INSTANCE-OF NUM-< RELATION)
R115: (TRANSITIVE-THROUGH NUM-< NUM-SUCC)
R116: (TRANSITIVE-THROUGH NUM-< NUM-<)
R117:
(forall (?X ?Y)
(=>
(INSTANCE-OF ?X NUMBER)
(INSTANCE-OF ?Y NUMBER)
(NUM-SUCC ?X ?Y)
(NUM-< ?X ?Y)))
;(LENGTH ?ASRT ?COUNT)
; - the count of arguments that are present
; in the assertion ?ASRT is the number ?COUNT.
; ?COUNT=0 is used for an assertion with
; only the relation present.
;; define signature of "LENGTH" relation
R118: (NTH-DOMAIN LENGTH 1 ASSERTION)
R119: (NTH-DOMAIN LENGTH 2 STRING)
R120: (NTH-ARGUMENT-NAME LENGTH 1 "?ASRT")
R121: (NTH-ARGUMENT-NAME LENGTH 2 "?COUNT")
R122: (VALENCE LENGTH 2)
R123: (INSTANCE-OF LENGTH RELATION)
R124:
; the length of all assertions using a relation
; equals the valence of that relation
(forall (?REL ?ASRT ?COUNT)
(and
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?COUNT COUNT)
(NTH-ARGUMENT ?ASRT 0 ?REL)
(LENGTH ?ASRT ?COUNT)
(VALENCE ?REL ?COUNT)
)
)
R125:
;for all assertions with a particular length,
;all arguments of the assertion
;with a position lower than that length
;are also defined.
;
(forall (?ASRT ?LEN)
(=>
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?LEN NUMBER)
(LENGTH ?ASRT ?LEN)
(forall (?X ?INS)
(and
(INSTANCE-OF ?X NUMBER)
(NUM-< ?X ?LEN)
(NTH-ARGUMENT ?ASRT ?X ?INS)
)
)
)
)
;(VALENCE ?REL ?COUNT)
; - the COUNT of arguments that the
; relation ?REL can take is the number ?COUNT
; Note: an assertion is not stated when a
; relation can take an arbitrary NUMBER of arguments
;; define signature of "VALENCE" relation
R126: (NTH-DOMAIN VALENCE 1 ASSERTION)
R127: (NTH-DOMAIN VALENCE 2 COUNT)
R128: (NTH-ARGUMENT-NAME VALENCE 1 "?")
R129: (NTH-ARGUMENT-NAME VALENCE 2 "?COUNT")
R130: (VALENCE VALENCE 2)
R131: (INSTANCE-OF VALENCE RELATION)
R132:
;for all assertions using a given relation,
;all arguments of the assertion
;with a position lower than the valence
;are also defined.
(forall (?REL ?ASRT ?LEN)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?LEN NUMBER)
(VALENCE ?REL ?LEN)
(NTH-ARGUMENT ?ASRT 0 ?REL)
(forall (?X ?INS)
(and
(INSTANCE-OF ?X NUMBER)
(NUM-< ?X ?LEN)
(NTH-ARGUMENT ?ASRT ?X ?INS)
)
)
)
)
;(NTH-ARGUMENT ?A ?P ?I)
; - the argument in position ?P in the
; assertion ?A is the individual ?I.
; ?P=0 is used for the individual
; representing the relation of the assertion.
;; define signature of "NTH-ARGUMENT" relation
R133: (NTH-DOMAIN NTH-ARGUMENT 1 ASSERTION)
R134: (NTH-DOMAIN NTH-ARGUMENT 2 POSITION)
R135: (NTH-DOMAIN NTH-ARGUMENT 3 INDIVIDUAL)
R136: (NTH-ARGUMENT-NAME NTH-ARGUMENT 1 "?ASRT")
R137: (NTH-ARGUMENT-NAME NTH-ARGUMENT 2 "?POS")
R138: (NTH-ARGUMENT-NAME NTH-ARGUMENT 3 "?INS")
R139: (VALENCE NTH-ARGUMENT 3)
R140: (INSTANCE-OF NTH-ARGUMENT RELATION)
R141: ;; define NTH-ARGUMENT for Nilary Assertions
(forall (?REL ?ASRT)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(<=> (?REL)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(VALENCE ?REL 0)
(LENGTH ?REL 0)))))
R142: ;; define NTH-ARGUMENT for Unary Assertions
(forall (?REL ?ASRT ?I1)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?I1 INDIVIDUAL)
(<=> (?REL ?I1)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT 1 ?I1)
(VALENCE ?REL 1)
(LENGTH ?REL 1)))))
R143: ;; define NTH-ARGUMENT for Binary Assertions
(forall (?REL ?ASRT ?I1 ?I2)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?I1 INDIVIDUAL)
(INSTANCE-OF ?I2 INDIVIDUAL)
(<=> (?REL ?I1 ?I2)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT 1 ?I1)
(NTH-ARGUMENT ?ASRT 2 ?I2)
(VALENCE ?REL 2)
(LENGTH ?REL 2)))))
R144: ;; define NTH-ARGUMENT for Trinary Assertions
(forall (?REL ?ASRT ?I1 ?I2 ?I3)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?I1 INDIVIDUAL)
(INSTANCE-OF ?I2 INDIVIDUAL)
(INSTANCE-OF ?I3 INDIVIDUAL)
(<=> (?REL ?I1 ?I2 ?I3)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT 1 ?I1)
(NTH-ARGUMENT ?ASRT 2 ?I2)
(NTH-ARGUMENT ?ASRT 3 ?I3)
(VALENCE ?REL 3)
(LENGTH ?REL 3)))))
R145: ;; define NTH-ARGUMENT for Quaternary Assertions
(forall (?REL ?ASRT ?I1 ?I2 ?I3 ?I4)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?I1 INDIVIDUAL)
(INSTANCE-OF ?I2 INDIVIDUAL)
(INSTANCE-OF ?I3 INDIVIDUAL)
(INSTANCE-OF ?I4 INDIVIDUAL)
(<=> (?REL ?I1 ?I2 ?I3 ?I4)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT 1 ?I1)
(NTH-ARGUMENT ?ASRT 2 ?I2)
(NTH-ARGUMENT ?ASRT 3 ?I3)
(NTH-ARGUMENT ?ASRT 4 ?I4)
(VALENCE ?REL 4)
(LENGTH ?REL 4)))))
R146: ;; define NTH-ARGUMENT for Quintary Assertions
(forall (?REL ?ASRT ?I1 ?I2 ?I3 ?I4 ?I5)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?I1 INDIVIDUAL)
(INSTANCE-OF ?I2 INDIVIDUAL)
(INSTANCE-OF ?I3 INDIVIDUAL)
(INSTANCE-OF ?I4 INDIVIDUAL)
(INSTANCE-OF ?I5 INDIVIDUAL)
(<=> (?REL ?I1 ?I2 ?I3 ?I4 ?I5)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT 1 ?I1)
(NTH-ARGUMENT ?ASRT 2 ?I2)
(NTH-ARGUMENT ?ASRT 3 ?I3)
(NTH-ARGUMENT ?ASRT 4 ?I3)
(NTH-ARGUMENT ?ASRT 5 ?I5)
(VALENCE ?REL 5)
(LENGTH ?REL 5)))))
R147: ;; define NTH-ARGUMENT for 6-ary Assertions
(forall (?REL ?ASRT ?I1 ?I2 ?I3 ?I4 ?I5 ?I6)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?I1 INDIVIDUAL)
(INSTANCE-OF ?I2 INDIVIDUAL)
(INSTANCE-OF ?I3 INDIVIDUAL)
(INSTANCE-OF ?I4 INDIVIDUAL)
(INSTANCE-OF ?I5 INDIVIDUAL)
(INSTANCE-OF ?I6 INDIVIDUAL)
(<=> (?REL ?I1 ?I2 ?I3 ?I4 ?I5 ?I6)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT 1 ?I1)
(NTH-ARGUMENT ?ASRT 2 ?I2)
(NTH-ARGUMENT ?ASRT 3 ?I3)
(NTH-ARGUMENT ?ASRT 4 ?I4)
(NTH-ARGUMENT ?ASRT 5 ?I5)
(NTH-ARGUMENT ?ASRT 6 ?I6)
(VALENCE ?REL 6)
(LENGTH ?REL 6)))))
R148: ;; define NTH-ARGUMENT for 7-ary Assertions
(forall (?REL ?ASRT ?I1 ?I2 ?I3 ?I4 ?I5 ?I6 ?I7)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?I1 INDIVIDUAL)
(INSTANCE-OF ?I2 INDIVIDUAL)
(INSTANCE-OF ?I3 INDIVIDUAL)
(INSTANCE-OF ?I4 INDIVIDUAL)
(INSTANCE-OF ?I5 INDIVIDUAL)
(INSTANCE-OF ?I6 INDIVIDUAL)
(INSTANCE-OF ?I7 INDIVIDUAL)
(<=> (?REL ?I1 ?I2 ?I3 ?I4 ?I5 ?I6 ?I7)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT 1 ?I1)
(NTH-ARGUMENT ?ASRT 2 ?I2)
(NTH-ARGUMENT ?ASRT 3 ?I3)
(NTH-ARGUMENT ?ASRT 4 ?I4)
(NTH-ARGUMENT ?ASRT 5 ?I5)
(NTH-ARGUMENT ?ASRT 6 ?I6)
(NTH-ARGUMENT ?ASRT 7 ?I7)
(VALENCE ?REL 7)
(LENGTH ?REL 7)))))
R149: ;; define NTH-ARGUMENT for 8-ary Assertions
(forall (?REL ?ASRT ?I1 ?I2 ?I3 ?I4 ?I5 ?I6 ?I7 ?I8)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?I1 INDIVIDUAL)
(INSTANCE-OF ?I2 INDIVIDUAL)
(INSTANCE-OF ?I3 INDIVIDUAL)
(INSTANCE-OF ?I4 INDIVIDUAL)
(INSTANCE-OF ?I5 INDIVIDUAL)
(INSTANCE-OF ?I6 INDIVIDUAL)
(INSTANCE-OF ?I7 INDIVIDUAL)
(INSTANCE-OF ?I8 INDIVIDUAL)
(<=> (?REL ?I1 ?I2 ?I3 ?I4 ?I5 ?I6 ?I7 ?I8)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT 1 ?I1)
(NTH-ARGUMENT ?ASRT 2 ?I2)
(NTH-ARGUMENT ?ASRT 3 ?I3)
(NTH-ARGUMENT ?ASRT 4 ?I4)
(NTH-ARGUMENT ?ASRT 5 ?I5)
(NTH-ARGUMENT ?ASRT 6 ?I6)
(NTH-ARGUMENT ?ASRT 7 ?I7)
(NTH-ARGUMENT ?ASRT 8 ?I8)
(VALENCE ?REL 8)
(LENGTH ?REL 8)))))
R150: ;; define NTH-ARGUMENT for 9-ary Assertions
(forall (?REL ?ASRT ?I1 ?I2 ?I3 ?I4 ?I5 ?I6 ?I7 ?I8 ?I9)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?ASRT ASSERTION)
(INSTANCE-OF ?I1 INDIVIDUAL)
(INSTANCE-OF ?I2 INDIVIDUAL)
(INSTANCE-OF ?I3 INDIVIDUAL)
(INSTANCE-OF ?I4 INDIVIDUAL)
(INSTANCE-OF ?I5 INDIVIDUAL)
(INSTANCE-OF ?I6 INDIVIDUAL)
(INSTANCE-OF ?I7 INDIVIDUAL)
(INSTANCE-OF ?I8 INDIVIDUAL)
(INSTANCE-OF ?I9 INDIVIDUAL)
(<=> (?REL ?I1 ?I2 ?I3 ?I4 ?I5 ?I6 ?I7 ?I8 ?I9)
(and
(NTH-ARGUMENT ?ASRT 0 ?REL)
(NTH-ARGUMENT ?ASRT 1 ?I1)
(NTH-ARGUMENT ?ASRT 2 ?I2)
(NTH-ARGUMENT ?ASRT 3 ?I3)
(NTH-ARGUMENT ?ASRT 4 ?I4)
(NTH-ARGUMENT ?ASRT 5 ?I5)
(NTH-ARGUMENT ?ASRT 6 ?I6)
(NTH-ARGUMENT ?ASRT 7 ?I7)
(NTH-ARGUMENT ?ASRT 8 ?I8)
(NTH-ARGUMENT ?ASRT 9 ?I9)
(VALENCE ?REL 9)
(LENGTH ?REL 9)))))
;(REVISION ?INS ?ID)
; - the revision identified by the string ?ID is the
; initial one in which the individual ?INS was part
; of the Standard Upper Ontology
R151: (NTH-DOMAIN REVISION 1 INDIVIDUAL)
R152: (NTH-DOMAIN REVISION 2 STRING)
R153: (NTH-ARGUMENT-NAME REVISION 1 "?INS")
R154: (NTH-ARGUMENT-NAME REVISION 2 "?ID")
R155: (VALENCE REVISION 2)
R156: (INSTANCE-OF REVISION RELATION)
R157:
(forall (?INS ?STR)
(=> (REVISION ?INS ?ID)
(\= ?ID "")))
I include the beginning of this relation, but I don't
know how to state it.
;exists-at-least-3 is a
R158: (NTH-DOMAIN EXISTS-AT-LEAST-3 1 VARIABLE-LIST)
R159: (NTH-DOMAIN EXISTS-AT-LEAST-3 2 ASSERTION)
R160: (NTH-ARGUMENT-NAME EXISTS-AT-LEAST-3 1 "?VARL")
R161: (NTH-ARGUMENT-NAME EXISTS-AT-LEAST-3 2 "?ASRT")
R162: (VALENCE EXISTS-AT-LEAST-3 2)
R163: (INSTANCE-OF EXISTS-AT-LEAST-3 RELATION)
(exists-at-least-3 (?x) (P ?x))
can be defined as
(exists (?x1 ?x2 ?x3)
(and (P x1?) (P ?x2) (P ?x3)
(not (or (= ?x1 ?x2) (= ?x1 ?x3) (= ?x2 ?x3))))).
Similarly,
(exists-at-most-3 (?x) (P ?x))
can be defined as
(forall (?x1 ?x2 ?x3 ?x4)
(=> (and (P ?x1) (P ?x2) (P ?x3) (P ?x4))
(or (= ?y ?x1) (= ?y ?x2) (= ?y ?x3) (= ?y ?x4))))
and
(exists-exactly-3 (?x) (P ?x))
can be defined as the conjunction of the above two or, somewhat more
pleasingly, as
(exists (?x1 ?x2 ?x3)
(and (not (or (= ?x1 ?x2) (= ?x1 ?x3) (= ?x2 ?x3)))
(forall (?y)
(<=> (P ?y)
(or (= ?y ?x1) (= ?y ?x2) (= ?y ?x3))))))