not
(=>
(
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
(
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
?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 19914-19929
If
equal
an organization
and the
department
of
a kind of physical
in
another organization
and
the organization
2 is a part of the organization
the other organization
and
equal
the organization
and
the organization
2 and
an entity
is an
instance
of
a kind of physical
and
the organization
is
interested
in
the entity
and
equal
a real number
and the
probability
of
the organization
is an
agent
of
another entity
and
equal
the other entity
2 and 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
?L
(
LineFn
?P1 ?P2))
(
part
?OP1 ?L)
(
part
?OP2 ?L)
(
not
(
equal
?OP1 ?OP2))
(
equal
?L2
(
LineFn
?OP1 ?OP2)))
(
part
?L2 ?L))
ComputingBrands.kif 2636-2644
If
equal
an object
and the line between
another object
and
a third object
and
a fourth object
is a
part
of
the object
and
a fifth object
is a
part
of
the object
and
equal
the fourth object
and
the fifth object
and
equal
the object
2 and the line between
the fourth object
and
the fifth object
,
then
the object
2 is a
part
of
the object
(=>
(
and
(
equal
?LIST3
(
ListConcatenateFn
?LIST1 ?LIST2))
(
not
(
equal
?LIST1
NullList
))
(
not
(
equal
?LIST2
NullList
))
(
lessThanOrEqualTo
?NUMBER1
(
ListLengthFn
?LIST1))
(
lessThanOrEqualTo
?NUMBER2
(
ListLengthFn
?LIST2))
(
instance
?NUMBER1
PositiveInteger
)
(
instance
?NUMBER2
PositiveInteger
))
(
and
(
equal
(
ListOrderFn
?LIST3 ?NUMBER1)
(
ListOrderFn
?LIST1 ?NUMBER1))
(
equal
(
ListOrderFn
?LIST3
(
AdditionFn
(
ListLengthFn
?LIST1) ?NUMBER2))
(
ListOrderFn
?LIST2 ?NUMBER2))))
Merge.kif 3096-3115
If
equal
a list
and the
list
composed of
another list
and
a third list
and
equal
the other list
and
null list
and
equal
the third list
and
null list
and
a positive integer
is
less
than or equal to
length
of
the other list
and
another positive integer
is
less
than or equal to
length
of
the third list
and
the positive integer
is an
instance
of
positive integer
and
the other positive integer
is an
instance
of
positive integer
,
then
equal
the positive integer
th
element
of
the list
and
the positive integer
th
element
of
the other list
and
equal
(
length
of
the other list
and
the other positive integer
)th
element
of
the list
and
the other positive integer
th
element
of
the third list
(=>
(
and
(
equal
?S
SecantLine
)
(
pointOfFigure
?P1 ?S)
(
pointOfFigure
?P2 ?S)
(
not
(
equal
?P1 ?P2))
(
equal
?C
Circle
)
(
pointOfFigure
?P1 ?C)
(
pointOfFigure
?P2 ?C))
(
exists
(?CHORD)
(
and
(
equal
?CHORD
ChordOfACircle
)
(
endPointsOfLine
?P1 ?P2 ?CHORD)
(
geometricPart
?CHORD ?S))))
Mid-level-ontology.kif 5867-5881
If
equal
a geometric figure
and
secant line
and
a geometric point
is a
vertex
of
the geometric figure
and
another geometric point
is a
vertex
of
the geometric figure
and
equal
the geometric point
and
the other geometric point
and
equal
another geometric figure
and
circle
and
the geometric point
is a
vertex
of
the other geometric figure
and
the other geometric point
is a
vertex
of
the other geometric figure
,
then there exists
the other geometric figure
HORD such that
equal
the other geometric figure
HORD and
chord of a circle
and
the geometric point
and
the other geometric point
are
endPointsOfLine
of
the other geometric figure
HORD and
the geometric figure
is a
geometric
part of
the other geometric figure
HORD
(=>
(
and
(
graphPart
?ARC1 ?GRAPH)
(
graphPart
?ARC2 ?GRAPH)
(
graphPart
?NODE1 ?GRAPH)
(
graphPart
?NODE2 ?GRAPH)
(
links
?NODE1 ?NODE2 ?ARC1)
(
links
?NODE1 ?NODE2 ?ARC2)
(
not
(
equal
?ARC1 ?ARC2)))
(
instance
?GRAPH
MultiGraph
))
Merge.kif 5815-5824
If
a graph arc
is a
part
of
a graph
and
another graph arc
is a
part
of
the graph
and
a graph node
is a
part
of
the graph
and
another graph node
is a
part
of
the graph
and
the graph arc
link
s
the graph node
and
the other graph node
and
the other graph arc
link
s
the graph node
and
the other graph node
and
equal
the graph arc
and
the other graph arc
,
then
the graph
is an
instance
of
multi graph
(=>
(
and
(
graphPart
?PATH ?GRAPH)
(
not
(
instance
?GRAPH
DirectedGraph
)))
(<=>
(
instance
?PATH
(
GraphPathFn
?NODE1 ?NODE2))
(
instance
?PATH
(
GraphPathFn
?NODE2 ?NODE1))))
Merge.kif 6087-6093
If
a graph element
is a
part
of
a graph
and
the graph
is not an
instance
of
directed graph
,
then
the graph element
is an
instance
of the
set
of paths between
a graph node
and
another graph node
if and only if
the graph element
is an
instance
of the
set
of paths between
the other graph node
and
the graph node
(=>
(
and
(
hasAccount
?U ?AC)
(
password
?P ?AC)
(
deviceAccount
?AC ?D)
(
not
(
knows
?U
(
password
?P ?AC)))
(
knows
?U
(
recoveryKey
?S ?AC))
(
possesses
?U ?D))
(
modalAttribute
(
exists
(?C)
(
and
(
instance
?C
ChangingPassword
)
(
patient
?C ?AC)
(
agent
?C ?U)))
Possibility
))
ComputingBrands.kif 4422-4439
If
a cognitive agent
has
account
an user account
and
the user account
has
password
a computer password
and
device account
the user account
and
a computer
and
the cognitive agent
doesn't
know
the user account
has
password
the computer password
and
the cognitive agent
know
s the account
the user account
has
recovery
key
an entity
and
the cognitive agent
possess
es
the computer
,
then the statement there exists
another entity
such that
the other entity
is an
instance
of
change password
and
the user account
is a
patient
of
the other entity
and
the cognitive agent
is an
agent
of
the other entity
has the
modal
force
of
possibility
(=>
(
and
(
hasGUEState
?WIN1
GUE_UncoveredState
)
(
hasGUEState
?WIN1
GUE_MaximizedWindowState
)
(
screenOfGUIE
?WIN1 ?SCREEN)
(
instance
?WIN2
InterfaceWindow
)
(
screenOfGUIE
?WIN2 ?SCREEN)
(
not
(
equal
?WIN1 ?WIN2)))
(
or
(
hasGUEState
?WIN2
GUE_CoveredState
)
(
hasGUEState
?WIN2
GUE_PartiallyCoveredState
)
(
hasGUEState
?WIN2
GUE_OffscreenState
)))
ComputerInput.kif 2120-2131
If
a GUI element
has
state
GUE uncovered state
and
the GUI element
has
state
GUE maximized window state
and
the GUI element
is
displayed
on
a computer screen
and
another GUI element
is an
instance
of
interface window
and
the other GUI element
is
displayed
on
the computer screen
and
equal
the GUI element
and
the other GUI element
,
then
the other GUI element
has
state
GUE covered state
or
the other GUI element
has
state
GUE partially covered state
or
the other GUI element
has
state
GUE offscreen state
(=>
(
and
(
holdsDuring
?T1
(
attribute
?H
Dieting
))
(
holdsDuring
?T2
(
not
(
attribute
?H
Dieting
)))
(
instance
?M1
Meal
)
(
instance
?E1
Eating
)
(
agent
?E1 ?H)
(
resource
?E1 ?M1)
(
during
(
WhenFn
?E1) ?T1)
(
measure
?M1
(
MeasureFn
?C1
Calorie
))
(
instance
?M2
Meal
)
(
instance
?E2
Eating
)
(
agent
?E2 ?H)
(
resource
?E2 ?M2)
(
during
(
WhenFn
?E2) ?T2)
(
measure
?M2
(
MeasureFn
?C2
Calorie
)))
(
modalAttribute
(
greaterThan
?C2 ?C1)
Likely
))
Mid-level-ontology.kif 32596-32617
If
dieting
is an
attribute
of
an agent
holds
during
a time interval
and
dieting
is not an
attribute
of
the agent
holds
during
another time interval
and
an object
is an
instance
of
meal
and
a process
is an
instance
of
eating
and
the agent
is an
agent
of
the process
and
the object
is a
resource
for
the process
and the
time
of existence of
the process
takes place
during
the time interval
and the
measure
of
the object
is
a real number
calorie
(s) and
another object
is an
instance
of
meal
and
another process
is an
instance
of
eating
and
the agent
is an
agent
of
the other process
and
the other object
is a
resource
for
the other process
and the
time
of existence of
the other process
takes place
during
the other time interval
and the
measure
of
the other object
is
another real number
calorie
(s),
then the statement
the other real number
is
greater
than
the real number
has the
modal
force
of
likely
(=>
(
and
(
instance
?A
Ambulating
)
(
subProcess
?S1 ?A)
(
instance
?S1
Stepping
)
(
subProcess
?S2 ?A)
(
instance
?S2
Stepping
)
(
equal
?S1START
(
BeginFn
(
WhenFn
?S1)))
(
equal
?S2START
(
BeginFn
(
WhenFn
?S2)))
(
not
(
or
(
before
?S1START ?S2START)
(
before
?S2START ?S1START))))
(
equal
?S1 ?S2))
Mid-level-ontology.kif 494-507
If
a process
is an
instance
of
ambulating
and
another process
is a
subprocess
of
the process
and
the other process
is an
instance
of
stepping
and
a third process
is a
subprocess
of
the process
and
the third process
is an
instance
of
stepping
and
equal
the other process
START and the
beginning
of the
time
of existence of
the other process
and
equal
the third process
START and the
beginning
of the
time
of existence of
the third process
and
the other process
START happens
before
the third process
START and
the third process
START happens
before
the other process
START,
then
equal
the other process
and
the third process
(=>
(
and
(
instance
?A
Attaching
)
(
patient
?A ?O1)
(
patient
?A ?O2)
(
holdsDuring
(
BeginFn
(
WhenFn
?A))
(
not
(
connected
?O1 ?O2)))
(
holdsDuring
(
EndFn
(
WhenFn
?A))
(
connected
?O1 ?O2)))
(
and
(
objectAttached
?A ?O1)
(
objectAttached
?A ?O2)))
Merge.kif 12535-12549
If
a process
is an
instance
of
attaching
and
an entity
is a
patient
of
the process
and
another entity
is a
patient
of
the process
and
the entity
is not
connected
to
the other entity
holds
during
the
beginning
of the
time
of existence of
the process
and
the entity
is
connected
to
the other entity
holds
during
the
end
of the
time
of existence of
the process
,
then
the process
attaches
the entity
to another object and
the process
attaches
the other entity
to another object
(=>
(
and
(
instance
?A1
Automobile
)
(
instance
?A2
Automobile
)
(
instance
?S1
AutomobileShock
)
(
part
?S1 ?A1)
(
not
(
exists
(?S2)
(
and
(
instance
?S2
AutomobileShock
)
(
part
?S2 ?A2))))
(
dampingRatio
?A1 ?R1)
(
dampingRatio
?A2 ?R2))
(
greaterThan
?R2 ?R1))
Cars.kif 853-866
If
a physical system
is an
instance
of
automobile
and
another physical system
is an
instance
of
automobile
and
an object
is an
instance
of
shock
and
the object
is a
part
of
the physical system
and there doesn't exist
another object
such that
the other object
is an
instance
of
shock
and
the other object
is a
part
of
the other physical system
and the damping ratio of
the physical system
is
a real number
and the damping ratio of
the other physical system
is
another real number
,
then
the other real number
is
greater
than
the real number
(=>
(
and
(
instance
?AGENT
AutonomousAgent
)
(
potentialCustomer
?CUST ?AGENT)
(
modalAttribute
(
and
(
instance
?R
Reserving
)
(
destination
?R ?AGENT))
Necessity
)
(
conditionalProbability
(
exists
(?RES1)
(
and
(
instance
?RES1
Reservation
)
(
reservingEntity
?CUST ?RES1)
(
fulfillingEntity
?AGENT ?RES1)))
(
customer
?CUST ?AGENT) ?NUM1)
(
conditionalProbability
(
not
(
exists
(?RES2)
(
and
(
instance
?RES2
Reservation
)
(
reservingEntity
?CUST ?RES2)
(
fulfillingEntity
?AGENT ?RES2))))
(
customer
?CUST ?AGENT) ?NUM2))
(
lessThan
?NUM2 ?NUM1))
Dining.kif 772-795
If
an agent
is an
instance
of
agent
and
a cognitive agent
is a
potential
customer
for
the agent
and the statement
an entity
is an
instance
of
reserving
and
the entity
end
s up at
the agent
has the
modal
force
of
necessity
and
probability
of there exists
the entity
ES1 such that
the entity
ES1 is an
instance
of
reservation
and
the cognitive agent
reserves
the entity
ES1 and
the agent
fulfills
the entity
ES1 provided that
the agent
is a
customer
of
the cognitive agent
holds is
a real number
and
probability
of there doesn't exist
the entity
ES2 such that
the entity
ES2 is an
instance
of
reservation
and
the cognitive agent
reserves
the entity
ES2 and
the agent
fulfills
the entity
ES2 provided that
the agent
is a
customer
of
the cognitive agent
holds is
another real number
,
then
the other real number
is
less
than
the real number
(=>
(
and
(
instance
?ANI
Animal
)
(
instance
?D
DiseaseOrSyndrome
)
(
not
(
attribute
?ANI ?D)))
(
exists
(?P ?W)
(
and
(
instance
?P
BiologicalProcess
)
(
instance
?P
Removing
)
(
origin
?P ?ANI)
(
instance
?W
Sewage
)
(
agent
?P ?ANI)
(
objectTransferred
?P ?W))))
Mid-level-ontology.kif 2625-2638
If
an agent
is an
instance
of
animal
and
an attribute
is an
instance
of
disease or syndrome
and
the attribute
is not an
attribute
of
the agent
,
then there exist
a transfer
and
an object
such that
the transfer
is an
instance
of
biological process
and
the transfer
is an
instance
of
removing
and
the transfer
originate
s at
the agent
and
the object
is an
instance
of
sewage
and
the agent
is an
agent
of
the transfer
and the object transferred in
the transfer
is
the object
(=>
(
and
(
instance
?B
Bubble
)
(
not
(
exists
(?X ?S)
(
and
(
attribute
?X ?S)
(
not
(
equal
?X
Gas
))
(
meetsSpatially
?X ?B)))))
(
attribute
?B
ConvexRoundShape
))
Mid-level-ontology.kif 5953-5962
If
an object
is an
instance
of
bubble
and there don't exist
another object
and
an attribute
such that
the attribute
is an
attribute
of
the other object
and
equal
the other object
and
gas
and
the other object
meet
s
the object
,
then
convex round shape
is an
attribute
of
the object
(=>
(
and
(
instance
?BTS
BimetalTemperatureSensor
)
(
instance
?M1
Metal
)
(
instance
?M2
Metal
)
(
not
(
equal
?M1 ?M2))
(
part
?M1 ?BTS)
(
part
?M2 ?BTS)
(
instance
?T1
TemperatureMeasure
)
(
instance
?T2
TemperatureMeasure
)
(
instance
?L1
LengthMeasure
)
(
instance
?L2
LengthMeasure
)
(
instance
?L3
LengthMeasure
)
(
instance
?L4
LengthMeasure
)
(
not
(
equal
?T1 ?T2))
(
not
(
equal
?TM1 ?TM2))
(
holdsDuring
?TM1
(
and
(
measure
?BTS ?T1)
(
measure
?M1 ?L1)
(
measure
?M2 ?L2)))
(
holdsDuring
?TM2
(
and
(
measure
?BTS ?T2)
(
measure
?M1 ?L3)
(
measure
?M2 ?L4))))
(
not
(
equal
(
DivisionFn
?L1 ?L2)
(
DivisionFn
?L3 ?L4))))
Cars.kif 4142-4174
If
an object
is an
instance
of
bi_metal temperature sensor
and
another object
is an
instance
of
metal
and
a third object
is an
instance
of
metal
and
equal
the other object
and
the third object
and
the other object
is a
part
of
the object
and
the third object
is a
part
of
the object
and
an entity
is an
instance
of
temperature measure
and
another entity
is an
instance
of
temperature measure
and
a real number
is an
instance
of
length measure
and
another real number
is an
instance
of
length measure
and
a third real number
is an
instance
of
length measure
and
a fourth real number
is an
instance
of
length measure
and
equal
the entity
and
the other entity
and
equal
a time position
and
another time position
and the
measure
of
the object
is
the entity
and the
measure
of
the other object
is
the real number
and the
measure
of
the third object
is
the other real number
holds
during
the time position
and the
measure
of
the object
is
the other entity
and the
measure
of
the other object
is
the third real number
and the
measure
of
the third object
is
the fourth real number
holds
during
the other time position
,
then
equal
not
the real number
and
the other real number
and not
the third real number
and
the fourth real number
(=>
(
and
(
instance
?C
Convoy
)
(
member
?X1 ?C)
(
member
?X2 ?C)
(
not
(
equal
?X1 ?X2)))
(
exists
(?P1 ?P2 ?D)
(
and
(
instance
?P1
Transportation
)
(
instance
?P2
Transportation
)
(
agent
?P1 ?X1)
(
agent
?P2 ?X2)
(
destination
?P1 ?D)
(
destination
?P2 ?D))))
Military.kif 108-122
If
a collection
is an
instance
of
convoy
and
an agent
is a
member
of
the collection
and
another agent
is a
member
of
the collection
and
equal
the agent
and
the other agent
,
then there exist
a process
,
another process
and
an entity
such that
the process
is an
instance
of
transportation
and
the other process
is an
instance
of
transportation
and
the agent
is an
agent
of
the process
and
the other agent
is an
agent
of
the other process
and
the process
end
s up at
the entity
and
the other process
end
s up at
the entity
(=>
(
and
(
instance
?C
Crystal
)
(
attribute
?C
MonoCrystalline
)
(
instance
?SUB
Substance
)
(
attribute
?SUB
Solid
)
(
attribute
?SUB
PolyCrystalline
)
(
instance
?S
Substance
)
(
surface
?S ?SUB)
(
not
(
part
?C ?S)))
(
exists
(?CLNT ?X ?MBR)
(
and
(
instance
?CLNT
Collection
)
(
memberCount
?CLNT ?X)
(
greaterThanOrEqualTo
?X 4)
(=>
(
member
?MBR ?CLNT)
(
and
(
part
?MBR ?SUB)
(
meetsSpatially
?C ?MBR))))))
Geography.kif 7479-7499
If
an object
is an
instance
of
crystal
and
mono crystalline
is an
attribute
of
the object
and
a self connected object
is an
instance
of
substance
and
solid
is an
attribute
of
the self connected object
and
poly crystalline
is an
attribute
of
the self connected object
and
another self connected object
is an
instance
of
substance
and
the other self connected object
is a
surface
of
the self connected object
and
the object
is not a
part
of
the other self connected object
,
then there exist
the object
LNT,
an integer
and
another object
such that
the object
LNT is an
instance
of
collection
and
the integer
is a
member
count of
the object
LNT and
the integer
is
greater
than or equal to 4 and
if
the other object
is a
member
of
the object
LNT,
then
the other object
is a
part
of
the self connected object
and
the object
meet
s
the other object
(=>
(
and
(
instance
?C
InPersonCommunication
)
(
agent
?C ?A1)
(
agent
?C ?A2)
(
not
(
equal
?A1 ?A2)))
(
holdsDuring
?C
(
orientation
?A1 ?A2
Near
)))
Media.kif 224-231
If
a process
is an
instance
of
in person communication
and
an agent
is an
agent
of
the process
and
another agent
is an
agent
of
the process
and
equal
the agent
and
the other agent
,
then
the agent
is
near
to
the other agent
holds
during
the process
(=>
(
and
(
instance
?CA
COVIDAntibody
)
(
holdsDuring
?T
(
and
(
not
(
attribute
?H
Covid19
))
(
part
?CA ?H))))
(
holdsDuring
(
ImmediateFutureFn
?T)
(
modalAttribute
(
attribute
?H
Covid19
)
Unlikely
)))
Medicine.kif 2785-2797
If
an entity
is an
instance
of
COVID antibody
and
Covid
is not an
attribute
of
another entity
and
the entity
is a
part
of
the other entity
holds
during
a time position
,
then the statement
Covid
is an
attribute
of
the other entity
has the
modal
force
of
unlikely
holds
during
immediately
after
the time position
(=>
(
and
(
instance
?CC
ComputerCable
)
(
not
(
instance
?C
Cable
))
(
part
?C ?CC))
(
or
(
instance
?C
MaleConnector
)
(
instance
?C
FemaleConnector
)))
ComputingBrands.kif 2746-2754
If
an object
is an
instance
of
cable
and
another object
is not an
instance
of
cable
and
the other object
is a
part
of
the object
,
then
the other object
is an
instance
of
公
or
the other object
is an
instance
of
female
(=>
(
and
(
instance
?CITY
AmericanCity
)
(
part
?CITY
California
)
(
not
(
equal
?CITY
LosAngelesCalifornia
)))
(
greaterThan
(
CardinalityFn
(
ResidentFn
LosAngelesCalifornia
))
(
CardinalityFn
(
ResidentFn
?CITY))))
CountriesAndRegions.kif 812-817
If
a geopolitical area
is an
instance
of
american city
and
the geopolitical area
is a
part
of
california
and
equal
the geopolitical area
and
los angeles california
,
then the number of
instances
in the
resident
of
los angeles california
is
greater
than the number of
instances
in the
resident
of
the geopolitical area
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
