equal
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfCurrency
))
(
instance
?QUANT
CurrencyMeasure
))
Merge.kif 6388-6392
If
a real number
an unit of measure
(s) is
equal
to
a physical quantity
and
the unit of measure
is an
instance
of
unit of currency
,
then
the physical quantity
is an
instance
of
currency measure
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfDuration
))
(
instance
?QUANT
TimeDuration
))
Merge.kif 6400-6404
If
a real number
an unit of measure
(s) is
equal
to
a physical quantity
and
the unit of measure
is an
instance
of
unit of duration
,
then
the physical quantity
is an
instance
of
time duration
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfFrequency
))
(
instance
?QUANT
FrequencyMeasure
))
Merge.kif 6846-6850
If
a real number
an unit of measure
(s) is
equal
to
a physical quantity
and
the unit of measure
is an
instance
of
unit of frequency
,
then
the physical quantity
is an
instance
of
frequency measure
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfInformation
))
(
instance
?QUANT
InformationMeasure
))
Merge.kif 6406-6410
If
a real number
an unit of measure
(s) is
equal
to
a physical quantity
and
the unit of measure
is an
instance
of
unit of information
,
then
the physical quantity
is an
instance
of
information measure
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfLength
))
(
instance
?QUANT
LengthMeasure
))
Merge.kif 6358-6362
If
a real number
an unit of measure
(s) is
equal
to
a physical quantity
and
the unit of measure
is an
instance
of
unit of length
,
then
the physical quantity
is an
instance
of
length measure
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfMass
))
(
instance
?QUANT
MassMeasure
))
Merge.kif 6364-6368
If
a real number
an unit of measure
(s) is
equal
to
a physical quantity
and
the unit of measure
is an
instance
of
unit of mass
,
then
the physical quantity
is an
instance
of
mass measure
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfTemperature
))
(
instance
?QUANT
TemperatureMeasure
))
Merge.kif 6382-6386
If
a real number
an unit of measure
(s) is
equal
to
a physical quantity
and
the unit of measure
is an
instance
of
unit of temperature
,
then
the physical quantity
is an
instance
of
temperature measure
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfVolume
))
(
instance
?QUANT
VolumeMeasure
))
Merge.kif 6376-6380
If
a real number
an unit of measure
(s) is
equal
to
a physical quantity
and
the unit of measure
is an
instance
of
unit of volume
,
then
the physical quantity
is an
instance
of
volume measure
(=>
(
and
(
equal
(
MeasureFn
?Y
McgPerKg
)
(
PerFn
?M1 ?M2))
(
equal
?M1
(
MeasureFn
?NUM1
(
MicroFn
Gram
)))
(
equal
?M2
(
MeasureFn
?NUM2
(
KiloFn
Gram
))))
(
exists
(?I ?B ?A)
(
and
(
instance
?I
Ingesting
)
(
instance
?B
BiologicallyActiveSubstance
)
(
instance
?A
Organism
)
(
patient
?I ?B)
(
agent
?I ?A)
(
weight
?B ?M1)
(
weight
?A ?M2))))
WMD.kif 823-840
If
a real number
micrograms per kilogram
(s) is
equal
to the
per
of
a mass measure
and
another mass measure
and
the mass measure
is
equal
to
another real number
one
millionth
of a
gram
(s) and
the other mass measure
is
equal
to
a third real number
1
thousand
gram
s(s),
then there exist
a process
,
a self connected object
and
another self connected object
such that
the process
is an
instance
of
ingesting
and
the self connected object
is an
instance
of
biologically active substance
and
the other self connected object
is an
instance
of
organism
and
the self connected object
is a
patient
of
the process
and
the other self connected object
is an
agent
of
the process
and
the mass measure
is a
weight
of
the self connected object
and
the other mass measure
is a
weight
of
the other self connected object
(=>
(
and
(
equal
(
MinimalWeightedPathFn
?NODE1 ?NODE2) ?PATH)
(
equal
(
PathWeightFn
?PATH) ?NUMBER1)
(
instance
?PATH2
(
GraphPathFn
?NODE1 ?NODE2))
(
equal
(
PathWeightFn
?PATH2) ?NUMBER2))
(
greaterThanOrEqualTo
?NUMBER2 ?NUMBER1))
Merge.kif 6022-6028
If the
lowest
cost
path
between
a graph node
and
another graph node
is
equal
to
a graph path
and the
value
of
the graph path
is
equal
to
a real number
and
the graph path
2 is an
instance
of the
set
of paths between
the graph node
and
the other graph node
and the
value
of
the graph path
2 is
equal
to
another real number
,
then
the other real number
is
greater
than or equal to
the real number
(=>
(
and
(
equal
(
PathWeightFn
?PATH) ?SUM)
(
graphPart
?ARC1 ?PATH)
(
graphPart
?ARC2 ?PATH)
(
arcWeight
?ARC1 ?NUMBER1)
(
arcWeight
?ARC2 ?NUMBER2)
(
forall
(?ARC3)
(=>
(
graphPart
?ARC3 ?PATH)
(
or
(
equal
?ARC3 ?ARC1)
(
equal
?ARC3 ?ARC2)))))
(
equal
(
PathWeightFn
?PATH)
(
AdditionFn
?NUMBER1 ?NUMBER2)))
Merge.kif 5993-6006
If the
value
of
a graph path
is
equal
to
a real number
and
a graph arc
is a
part
of
the graph path
and
another graph arc
is a
part
of
the graph path
and the
value
of
the graph arc
is
another real number
and the
value
of
the other graph arc
is
a third real number
and for all
a graph element
if
the graph element
is a
part
of
the graph path
,
then
the graph element
is
equal
to
the graph arc
or
the graph element
is
equal
to
the other graph arc
,
then the
value
of
the graph path
is
equal
to (
the other real number
and
the third real number
)
(=>
(
and
(
equal
(
PathWeightFn
?PATH) ?SUM)
(
subGraph
?SUBPATH ?PATH)
(
graphPart
?ARC1 ?PATH)
(
arcWeight
?ARC1 ?NUMBER1)
(
forall
(?ARC2)
(=>
(
graphPart
?ARC2 ?PATH)
(
or
(
graphPart
?ARC2 ?SUBPATH)
(
equal
?ARC2 ?ARC1)))))
(
equal
?SUM
(
AdditionFn
(
PathWeightFn
?SUBPATH) ?NUMBER1)))
Merge.kif 5979-5991
If the
value
of
a graph path
is
equal
to
a real number
and
another graph path
is a
subgraph
of
the graph path
and
a graph arc
is a
part
of
the graph path
and the
value
of
the graph arc
is
another real number
and for all
a graph element
if
the graph element
is a
part
of
the graph path
,
then
the graph element
is a
part
of
the other graph path
or
the graph element
is
equal
to
the graph arc
,
then
the real number
is
equal
to (the
value
of
the other graph path
and
the other real number
)
(=>
(
and
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER)
(
not
(
equal
?NUMBER 0))
(
not
(
equal
?NUMBER1 0))
(
not
(
equal
?NUMBER2 0)))
(
equal
(
SignumFn
?NUMBER2)
(
SignumFn
?NUMBER)))
Merge.kif 5130-5142
If
an integer
mod
another integer
is
equal
to
a third integer
and
the third integer
is not
equal
to 0 and
the integer
is not
equal
to 0 and
the other integer
is not
equal
to 0,
then the
sign
of
the other integer
is
equal
to the
sign
of
the third integer
(=>
(
and
(
equal
(
RemainderFn
?NUMBER1 ?NUMBER2) ?NUMBER)
(
not
(
equal
?NUMBER2 0)))
(
equal
(
AdditionFn
(
MultiplicationFn
(
FloorFn
(
DivisionFn
?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
Merge.kif 5104-5115
If
an integer
mod
another integer
is
equal
to
a third integer
and
the other integer
is not
equal
to 0,
then (the
largest
integer less than or equal to
the integer
and
the other integer
and
the other integer
and
the third integer
) is
equal
to
the integer
(=>
(
and
(
equal
?A
(
AverageFn
?L))
(
greaterThan
(
ListLengthFn
?L) 0))
(
equal
?A
(
DivisionFn
(
ListSumFn
?L)
(
ListLengthFn
?L))))
Merge.kif 3277-3284
If
a real number
is
equal
to the
average
of the numbers in
a list
and
length
of
the list
is
greater
than 0,
then
the real number
is
equal
to the
sum
of
the list
and
length
of
the list
(=>
(
and
(
equal
?A
(
AverageFn
?L))
(
inList
?N ?L))
(
instance
?N
Number
))
Merge.kif 3286-3290
If
a real number
is
equal
to the
average
of the numbers in
a list
and
an entity
is a
member
of
the list
,
then
the entity
is an
instance
of
number
(=>
(
and
(
equal
?A
(
ListSumFn
?L))
(
equal
1
(
ListLengthFn
?L)))
(
equal
?A
(
ListOrderFn
?L 1)))
Merge.kif 3252-3256
If
a real number
is
equal
to the
sum
of
a list
and 1 is
equal
to
length
of
the list
,
then
the real number
is
equal
to 1th
element
of
the list
(=>
(
and
(
equal
?A
(
ListSumFn
?L))
(
greaterThan
(
ListLengthFn
?L) 1))
(
equal
?A
(
AdditionFn
(
FirstFn
?L)
(
ListSumFn
(
SubListFn
2
(
ListLengthFn
?L) ?L)))))
Merge.kif 3258-3268
If
a real number
is
equal
to the
sum
of
a list
and
length
of
the list
is
greater
than 1,
then
the real number
is
equal
to (the
first
of
the list
and the
sum
of the sub-list from 2 to
length
of
the list
of
the list
)
(=>
(
and
(
equal
?AF
(
OrganicObjectFn
?F))
(
subclass
?AF
AnimalFat
)
(
subclass
?F
FatTissue
))
(
initialPart
?F
Animal
))
Food.kif 2876-2882
If
a kind of object
is
equal
to
Object
made from
another kind of object
and
a kind of object
is a
subclass
of
animal fat
and
another kind of object
is a
subclass
of
fat tissue
,
then every
the other kind of object
is
initially
part
of a
animal
(=>
(
and
(
equal
?B
(
OrganicObjectFn
?P))
(
subclass
?B
CoffeeBean
)
(
subclass
?P
Seed
))
(
initialPart
?P
CoffeePlant
))
Economy.kif 4629-4634
If
a kind of object
is
equal
to
Object
made from
another kind of object
and
a kind of object
is a
subclass
of
coffee bean
and
another kind of object
is a
subclass
of
seed
,
then every
the other kind of object
is
initially
part
of a
coffee plant
(=>
(
and
(
equal
?C
(
OrganicObjectFn
?S))
(
subclass
?C
CocoaBean
)
(
subclass
?S
Seed
))
(
initialPart
?S
CocoaTree
))
Economy.kif 4693-4699
If
a kind of object
is
equal
to
Object
made from
another kind of object
and
a kind of object
is a
subclass
of
cocoa bean
and
another kind of object
is a
subclass
of
seed
,
then every
the other kind of object
is
initially
part
of a
cocoa tree
(=>
(
and
(
equal
?CLASS1
(
ReceivingAnObjectFn
?OBJCLASS1))
(
equal
?CLASS2
(
ReceivingAnObjectFn
?OBJCLASS2))
(
subclass
?OBJCLASS1 ?OBJCLASS2))
(
subclass
?CLASS1 ?CLASS2))
Media.kif 195-200
If
a kind of getting
is
equal
to
receiving
a
a kind of object
and
another kind of getting
is
equal
to
receiving
a
another kind of object
and
a kind of object
is a
subclass
of
another kind of object
,
then
a kind of getting
is a
subclass
of
another kind of getting
(=>
(
and
(
equal
?D
(
AlbumCopiesFn
?A ?DS))
(
instance
?X ?D))
(
forall
(?S)
(=>
(
inList
?S ?A)
(
exists
(?C)
(
and
(
copy
?C ?S)
(
stored
?C ?X))))))
Music.kif 936-946
If
a kind of data storage device
is
equal
to the
set
of copies on
a kind of data storage device
S of
an album
and
a third data storage device
is an
instance
of
the kind of data storage device
,
then for all
an object
if
the object
is a
member
of
the album
,
then there exists
a content bearing object
such that
the content bearing object
is a
copy
of
the object
and
the content bearing object
is
stored
on
the third data storage device
(=>
(
and
(
equal
?DEP
(
DepartmentOfFn
?COMP ?PHYS))
(
subOrganization
?DEP2 ?COMP)
(
not
(
equal
?DEP ?DEP2))
(
instance
?I ?PHYS)
(
inScopeOfInterest
?DEP ?I)
(
equal
?P1
(
ProbabilityFn
(
agent
?P ?DEP)))
(
equal
?P2
(
ProbabilityFn
(
agent
?P ?DEP2))))
(
greaterThan
?P1 ?P2))
Mid-level-ontology.kif 18343-18358
If
an organization
is
equal
to the
department
of
a kind of physical
in
another organization
and
the organization
2 is a part of the organization
the other organization
and
the organization
is not
equal
to
the organization
2 and
an entity
is an
instance
of
a kind of physical
and
the organization
is
interested
in
the entity
and
a real number
is
equal
to the
probability
of
the organization
is an
agent
of
another entity
and
the other entity
2 is
equal
to the
probability
of
the organization
2 is an
agent
of
the other entity
,
then
the real number
is
greater
than
the other entity
2
(=>
(
and
(
equal
?DEP
(
DepartmentOfPreventingFn
?COMP ?PHYS))
(
subclass
?PHYS
Process
)
(
subOrganization
?DEP ?COMP))
(
inhibits
?DEP ?PHYS))
Mid-level-ontology.kif 18401-18406
If
an organization
is
equal
to
another organization
is
preventing
a kind of physical
and
a kind of physical
is a
subclass
of
process
and
the organization
is a part of the organization
the other organization
,
then
the organization
inhibit
s
the kind of physical
Display limited to 25 items.
Show next 25
Display limited to 25 items.
Show next 25
Sigma web home
Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is
open source software
produced by
Articulate Software
and its partners