Re: SUO: Starter Ontology Version 2
David,
One style comment I might make is that I'd prefer an InterCaps
style for names but that's purely personal preference. We should
get the consensus of the group.
More substantive comments below:
At 07:04 PM 9/20/2000 -0500, David Whitten wrote:
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
I'd suggest making ?WHO of type Person (or maybe Agent?). That
instance of Person could have a 'name-of' assertion.
(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
I'd prefer something like 'revisionDate' taking a date as an argument,
which I think would be more meaningful than a revision number.
(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
why not 'num-prev' rather than 'num-<' ?
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
I'm not clear on why the position which numbers the place of an argument
in a relation needs to be its own class rather than just an
Integer.
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
Would it be more proper to call this 'Sentence' ? 'Assertion'
seems to imply a form of usage. Just a quibble over a name
though.
We could use this class to associate comments with
statements. That might make things easier for storing in a
knowledge base although it would make commenting a bit more
cumbersome. For example, instead of
R005: ;; There exists something
(exists (?ONE)
(INSTANCE-OF ?ONE TOP))
we could have
(comment "There exists something"
(exists (?ONE)
(INSTANCE-OF ?ONE TOP)))
Rules:
R001:
(forall (?ANY)
(= ?ANY ?ANY))
R002:
(forall (?ANY)
(not (\= ?ANY ?ANY)))
R003:
(forall (?X ?Y)
(not (and
(= ?ANY ?ANY)
(\= ?X
?Y))))
What about instantiating as
(not
(and
(= Chair01
Chair01)
(/= Bob
Sue)))
I'm probably missing something obvious
;;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 "")))
It might be worth having the ability to track multiple authors with
something like
(previousAuthor ?ASSERT ?WHO ?EARLIER-WHO)
You could then have a whole chain of authors.
;(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))))))
-----------------
Adam Pease
Teknowledge
(650) 424-0500 x571