equal
(=>
(
and
(
equal
(
LeastCommonMultipleFn
@ROW) ?NUMBER)
(
not
(
equal
?NUMBER 0)))
(
not
(
exists
(?LESS)
(
and
(
lessThan
?LESS ?NUMBER)
(
forall
(?ELEMENT)
(=>
(
inList
?ELEMENT
(
ListFn
@ROW))
(
equal
(
RemainderFn
?LESS ?ELEMENT) 0)))))))
Merge.kif 4986-5000
If
equal
the
least
common multiple of @ROW and
an integer
and
equal
the integer
and 0,
then there doesn't exist
another integer
such that
the other integer
is
less
than
the integer
and for all
a third integer
if
the third integer
is a
member
of (@ROW),
then
equal
the other integer
mod
the third integer
and 0
(=>
(
and
(
equal
(
ListLengthFn
?LIST) ?NUMBER)
(
equal
(
ListOrderFn
?LIST ?NUMBER) ?ITEM))
(
equal
(
LastFn
?LIST) ?ITEM))
Merge.kif 3232-3236
If
equal
length
of
a list
and
a positive integer
and
equal
the positive integer
th
element
of
the list
and
another entity
,
then
equal
the
last
of
the list
and
the other entity
(=>
(
and
(
equal
(
MaximalWeightedPathFn
?NODE1 ?NODE2) ?PATH)
(
equal
(
PathWeightFn
?PATH) ?NUMBER1)
(
instance
?PATH2
(
GraphPathFn
?NODE1 ?NODE2))
(
equal
(
PathWeightFn
?PATH2) ?NUMBER2))
(
lessThanOrEqualTo
?NUMBER2 ?NUMBER1))
Merge.kif 6069-6075
If
equal
the
highest
cost
path
between
a graph node
and
another graph node
and
a graph path
and
equal
the
value
of
the graph path
and
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
equal
the
value
of
the graph path
2 and
another real number
,
then
the other real number
is
less
than or equal to
the real number
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfAngularMeasure
))
(
instance
?QUANT
AngleMeasure
))
Merge.kif 6419-6423
If
equal
a real number
an unit of measure
(s) and
a physical quantity
and
the unit of measure
is an
instance
of
unit of angular measure
,
then
the physical quantity
is an
instance
of
angle measure
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfArea
))
(
instance
?QUANT
AreaMeasure
))
Merge.kif 6395-6399
If
equal
a real number
an unit of measure
(s) and
a physical quantity
and
the unit of measure
is an
instance
of
unit of area
,
then
the physical quantity
is an
instance
of
area measure
(=>
(
and
(
equal
(
MeasureFn
?NUMBER ?UNIT) ?QUANT)
(
instance
?UNIT
UnitOfCurrency
))
(
instance
?QUANT
CurrencyMeasure
))
Merge.kif 6413-6417
If
equal
a real number
an unit of measure
(s) and
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 6425-6429
If
equal
a real number
an unit of measure
(s) and
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 6871-6875
If
equal
a real number
an unit of measure
(s) and
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 6431-6435
If
equal
a real number
an unit of measure
(s) and
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 6383-6387
If
equal
a real number
an unit of measure
(s) and
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 6389-6393
If
equal
a real number
an unit of measure
(s) and
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 6407-6411
If
equal
a real number
an unit of measure
(s) and
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 6401-6405
If
equal
a real number
an unit of measure
(s) and
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
equal
a real number
micrograms per kilogram
(s) and the
per
of
a mass measure
and
another mass measure
and
equal
the mass measure
and
another real number
one
millionth
of a
gram
(s) and
equal
the other mass measure
and
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 6047-6053
If
equal
the
lowest
cost
path
between
a graph node
and
another graph node
and
a graph path
and
equal
the
value
of
the graph path
and
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
equal
the
value
of
the graph path
2 and
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 6018-6031
If
equal
the
value
of
a graph path
and
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
equal
the graph element
and
the graph arc
or
equal
the graph element
and
the other graph arc
,
then
equal
the
value
of
the graph path
and (
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 6004-6016
If
equal
the
value
of
a graph path
and
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
equal
the graph element
and
the graph arc
,
then
equal
the real number
and (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 5158-5170
If
equal
an integer
mod
another integer
and
a third integer
and
equal
the third integer
and 0 and
equal
the integer
and 0 and
equal
the other integer
and 0,
then
equal
the
sign
of
the other integer
and 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 5132-5143
If
equal
an integer
mod
another integer
and
a third integer
and
equal
the other integer
and 0,
then
equal
(the
largest
integer less than or equal to
the integer
and
the other integer
and
the other integer
and
the third integer
) and
the integer
(=>
(
and
(
equal
?A
(
AverageFn
?L))
(
greaterThan
(
ListLengthFn
?L) 0))
(
equal
?A
(
DivisionFn
(
ListSumFn
?L)
(
ListLengthFn
?L))))
Merge.kif 3290-3297
If
equal
a real number
and the
average
of the numbers in
a list
and
length
of
the list
is
greater
than 0,
then
equal
the real number
and the
sum
of
the list
and
length
of
the list
(=>
(
and
(
equal
?A
(
AverageFn
?L))
(
inList
?N ?L))
(
instance
?N
Number
))
Merge.kif 3299-3303
If
equal
a real number
and 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 3265-3269
If
equal
a real number
and the
sum
of
a list
and
equal
1 and
length
of
the list
,
then
equal
the real number
and 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 3271-3281
If
equal
a real number
and the
sum
of
a list
and
length
of
the list
is
greater
than 1,
then
equal
the real number
and (the
first
of
the list
and the
sum
of the sub-list from 2 to
length
of
the list
of
the list
)
(=>
(
and
(
equal
?A
AcuteAngle
)
(
angularMeasure
?A
(
MeasureFn
?N
AngularDegree
)))
(
lessThan
?N 90.0))
Mid-level-ontology.kif 5493-5498
If
equal
a two dimensional angle
and
acute angle
and
a real number
angular degree
(s) is an
angular
measure of
the two dimensional angle
,
then
the real number
is
less
than 90.0
(=>
(
and
(
equal
?A
CircularArc
)
(
pointOfFigure
?P ?A))
(
exists
(?C ?P2)
(
and
(
geometricPart
?A ?C)
(
equal
?C
Circle
)
(
pointOfFigure
?P2 ?C)
(
equal
?P ?P2))))
Mid-level-ontology.kif 5658-5667
If
equal
a geometric figure
and
circular arc
and
a geometric point
is a
vertex
of
the geometric figure
,
then there exist
another geometric figure
and
the geometric point
2 such that
the other geometric figure
is a
geometric
part of
the geometric figure
and
equal
the other geometric figure
and
circle
and
the geometric point
2 is a
vertex
of
the other geometric figure
and
equal
the geometric point
and
the geometric point
2
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