forall - Sigma Knowledge base Browser

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.

domainEnglishFormat.kif 65868-65868

antecedent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 17414-17422	An entity is an instance of human and for all another entity the other entity doesn't employ the entity holds during a time position if and only if unemployed person is an attribute of the entity holds during the time position
No TPTP formula. May not be expressible in strict first order.	Geography.kif 1516-1524	If cold climate zone is a climate type in area of a geographic area and for all a time interval the time interval is an instance of month and the geographic area average temperature for period the time interval for a real number celsius degree(s), then 10.0 is greater than the real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 6003-6016	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)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5989-6001	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)
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3202-3215	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of auctioning , then there exist a symbolic string and an entity_PURCHASE_AMOUNT such that the total of values in the class described by the symbolic string is the entity_PURCHASE_AMOUNT and the total purchase price of the collection is equal to the entity_PURCHASE_AMOUNT
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 2887-2903	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of financial transaction , then there exist a symbolic string and an entity such that the number of instances in the class described by the symbolic string is equal to number of items purchased in the collection
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 2845-2870	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of web listing , then the number of instances in there exist an entity, another entity and a third entity such that the class described by the entity and the number of instances in the collection is equal to number of bids in the collection
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 2922-2940	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of web listing , then there exist a symbolic string, an entity,, , another entity and the symbolic string such that the number of instances in the class described by the symbolic string is equal to number of bids in the collection
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 1033-1060	If a collection is an instance of collection and a web site is an instance of web site and an agent is an instance of agent and a web listing is an instance of web listing and a time point is an instance of time point and the agent sells the web listing and the web listing is not a member of the collection and for all a physical and another physical if the physical is an instance of web listing and the physical is a member of items for sale by the agent at the web site and the time point is a part of the time of existence of the physical and the physical is not equal to the web listing, then the physical is a member of the collection and if the other physical is a member of the collection, then the time point is a part of the time of existence of the physical and the other physical is an instance of web listing , then things for sale by the agent not listed in the web listing at the web site during the time point is equal to the collection
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 2956-2983	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of buying and there exists an object such that the object is an instance of geopolitical area and for all an agent and a process if the agent is an instance of agent and the process is an instance of buying and the process is a member of the collection and the agent is an agent of the process, then the agent is located at the object , then there exist a symbolic string, an entity and another entity_PURCHASE_AMOUNT such that the total of values in the class described by the symbolic string is the other entity_PURCHASE_AMOUNT and the value of the collection is equal to the other entity_PURCHASE_AMOUNT
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 2999-3026	If a collection is an instance of collection and for all a physical if the physical is a member of the collection, then the physical is an instance of selling and there exists an object such that the object is an instance of geopolitical area and for all an agent and a process if the agent is an instance of agent and the process is an instance of buying and the process is a member of the collection and the agent is an agent of the process, then the agent is located at the object , then there exist a symbolic string, an entity and another entity_SALE_AMOUNT such that the total of values in the class described by the symbolic string is the other entity_SALE_AMOUNT and the value of the collection is equal to the other entity_SALE_AMOUNT
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 8531-8545	If an object is an instance of auditorium seat and the object is a part of another object and a third object is a part of the other object and the other object is an instance of auditorium and the third object is an instance of performance stage and a fourth object is located at the object and the fourth object is an instance of human and a kind of process is a subclass of seeing and for all another process if the other process is an instance of a kind of process, then the third object is a patient of the other process , then the fourth object is capable of doing the kind of process as a agent
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 4241-4267	If a human is an instance of human and a collection is an instance of collection and for all an experimenting and a physical if there exists a kind of process such that the experimenting is an instance of experimenting and the physical is an instance of process and the physical is a member of events in the experimenting and the physical is an instance of a kind of process and the human is capable of doing the kind of process as a experiencer, then the physical is a member of the collection and if another physical is a member of the collection, then the other physical is an instance of process and there exist another experimenting and the other physicalESS such that the other experimenting is an instance of experimenting and the other physical is a member of events in the other experimenting and the other physical is an instance of the other physicalESS and the human is capable of doing the other physicalESS as a experiencer , then all the processes the human is qualified for is equal to the collection
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 4175-4190	If a human is an instance of human and a collection is an instance of collection and for all a web page, a process and an experimenting if the web page is an instance of web page and the process is an instance of accessing web page and the experimenting is an instance of experimenting and the human is an agent of the process and the web page is a patient of the process and the web page is the object of study of the experimenting, then the process is a member of the collection , then the collection is equal to all the treated web page views from the human
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3333-3356	If a collection is an instance of collection and a corpuscular object is an instance of hyperlink and for all a physical the physical is a member of another collection and the physical is an instance of accessing web page and the other collection is a component of the corpuscular object, then there exists a third collection such that the third collection is an instance of collection and for all a process if the process is an instance of requesting hyperlink and the corpuscular object is a patient of the process, then the process is a member of the third collection and the rate of clicking through the corpuscular object in the collection is equal to the number of instances in the third collection and the number of instances in the collection
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3668-3704	If a collection is an instance of collection and another collection is an instance of collection and the other collection is a proper sub-collection of the collection and for all a physical if the physical is a member of the collection, then the physical is an instance of accessing web page and for all a process, an agent,, , another process,, , the process and an object if the agent is an instance of human and the process is an instance of buying and the other process is an instance of accessing web page and the object is an instance of web page and the other process is a member of the collection and the other process ends up at the object and the agent is an agent of the process and the agent is an agent of the other process and the time of existence of the process takes place during the time of existence of the other process and the object is an instrument for the process, then the process is a member of the other collection , then there exist a time interval, an entity_IN_INTERVAL and another entity_IN_INTERVAL such that purchases made in the collection during the time interval is equal to the number of instances in the class described by the entity_IN_INTERVAL and the number of instances in the class described by the other entity_IN_INTERVAL

consequent

No TPTP formula. May not be expressible in strict first order.	People.kif 357-390	A year is an instance of the year the yearEAR and the male life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order.	People.kif 403-436	A year is an instance of the year an integer and the female life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order.	People.kif 310-342	A year is an instance of the year an integer and the life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM if the listITEM is a member of the list, then the listITEM is an instance of the symbolic string and there doesn't exist a fifth entity such that the fifth entity is an instance of the symbolic string and the fifth entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order.	People.kif 272-293	A real number is an average of a list if and only if there exist another list and a positive integer such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all another positive integer if the other positive integer is a member of the other list, then there exist another real number, the other real numberMINUSONE,, , a third positive integer and a fourth positive integer such that the other real number is greater than 1 and the other real number is less than or equal to length of the other list and the other positive integerth element of the other list is equal to the other real number and the third positive integer is a member of the list and the other real number is equal to the third positive integerth element of the list and the fourth positive integer is a member of the other list and the other real numberMINUSONE is equal to (the other real number and 1) and the other real numberMINUSONE is equal to the fourth positive integerth element of the other list and the other positive integer is equal to (the third positive integer and the fourth positive integer) and the positive integer is equal to length of the other list and the real number is equal to the positive integerth element of the other list and the positive integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7828-7836	An object is larger than another object if and only if for all a real number, another real number and an unit of measure if the measure of the object is the real number the unit of measure(s) and the measure of the other object is the other real number the unit of measure(s) and the unit of measure is an instance of unit of length, then the real number is greater than the other real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1292-1297	A collection is a proper sub-collection of another collection if and only if for all a physical if the physical is a member of the collection, then the physical is a member of the other collection
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 171-176	If all rooms in a room inventory have a kind of physical, then for all a kind of hotel unit if a kind of hotel unit is a member type of the room inventory, then a kind of physical is an amenity in the kind of hotel unit
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 233-238	If all rooms in a room inventory have policy a policy, then for all a kind of hotel unit if a kind of hotel unit is a member type of the room inventory, then the policy is a policy that applies to the kind of hotel unit
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 218-223	If all rooms in a room inventory have service a kind of physical, then for all a kind of hotel unit if a kind of hotel unit is a member type of the room inventory, then a kind of physical is an amenity in the kind of hotel unit
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 5946-5954	If an attribute is an attribute of an object and the attribute is an instance of sphere, then there exist a geometric point and a length measure such that for all another geometric point if the other geometric point is a vertex of the object, then the other geometric point is geometric distance the geometric point for the length measure
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17856-17865	If monochromatic is an attribute of an object and another object is a superficial part of the object and an attribute is an attribute of the other object and the attribute is an instance of primary color, then for all a third object if the third object is a superficial part of the object, then the attribute is an attribute of the third object
No TPTP formula. May not be expressible in strict first order.	Government.kif 1094-1114	If a human is a citizen of a nation and universal suffrage law is a sub-proposition of the regional law of the nation, then the regional law of the nation allows the human to perform task of the type for all an entity, another entity and a third entity if the human is a citizen of the nation and the entity year duration(s) is a suffrage age minimum of the nation and the age of the human is the other entity year duration(s) and the other entity is greater than or equal to the entity and the third entity is an instance of the election of the nation, then there exists a fourth entity such that the fourth entity is an instance of the voting of the third entity and the human is an agent of the fourth entity
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 147-154	If a collection is an element of belongings of an agent and the collection is an instance of room inventory, then for all a physical if the physical is a member of the collection, then the physical is an element of belongings of the agent
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4874-4885	If the greatest common divisor of @ROW is equal to an integer and the integer is not equal to 0, then for all another integer if the other integer is a member of (@ROW), then the other integer mod the integer is equal to 0
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4887-4901	If the greatest common divisor of @ROW is equal to an integer and the integer is not equal to 0, then there doesn't exist another integer such that the other integer is greater than the integer and for all a third integer if the third integer is a member of (@ROW), then the third integer mod the other integer is equal to 0
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4959-4969	If the least common multiple of @ROW is equal to an integer and the integer is not equal to 0, then for all another integer if the other integer is a member of (@ROW), then the integer mod the other integer is equal to 0
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4971-4985	If the least common multiple of @ROW is equal to an integer and the integer is not equal to 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 the other integer mod the third integer is equal to 0
No TPTP formula. May not be expressible in strict first order.	Music.kif 938-948	If a kind of data storage device is equal to the set of copies on a kind of data storage deviceS 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
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10017-10024	If a hole is a hole in a self connected object and another hole is a hole in the self connected object, then for all a third hole if the third hole is a part of the union of the parts of the hole and the other hole, then the third hole is a hole in the self connected object
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 992-1008	If an agent is an instance of agent and a web site is an instance of web site, then there exists a collection such that the collection is an instance of collection and for all a web listing if the web listing is an instance of web listing and the web listing is hosted on the web site and the agent sells the web listing, then the web listing is a member of the collection and items for sale by the agent at the web site is equal to the collection
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14279-14290	If an object is an instance of chin and another object is an instance of face and the object is a part of the other object, then for all a third object if the third object is a part of the other object and the third object is not a part of the object, then the third object is below to the object
No TPTP formula. May not be expressible in strict first order.	Food.kif 1013-1027	If a process is an instance of grinding and an entity is a patient of the process and the entity is an instance of corpuscular object, then there exists another entity such that the other entity is a result of the process and the other entity is an instance of collection and for all a third entity if the third entity is a member of the other entity, then the third entity is a part of the entity holds during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3376-3408	If a time interval is an instance of time interval and a web site is an instance of web site, then there exists a collection such that the collection is an instance of collection and for all an agent if the agent is a member of the collection, then there exists another time interval such that the agent is an instance of agent and the other time interval is an instance of buying and the agent is an agent of the other time interval and the web site is an instrument for the other time interval and the other time interval takes place during the time interval and there doesn't exist the time interval_BEFORE such that the time interval_BEFORE is an instance of time interval and the time interval_BEFORE happens earlier than the time interval and there exists the other time interval_BEFORE such that the other time interval_BEFORE is an instance of buying and the agent is an agent of the other time interval_BEFORE and the web site is an instrument for the other time interval_BEFORE and the other time interval_BEFORE takes place during the time interval holds during the time interval_BEFORE and new buyers at the web site during the time interval is equal to the collection
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3428-3455	If a time interval is an instance of time interval and a web site is an instance of web site, then there exists a collection such that the collection is an instance of collection and for all a physical if the physical is an instance of human and there doesn't exist the time interval_BEFORE such that the time interval_BEFORE is an instance of time interval and the time interval_BEFORE happens earlier than the time interval and the physical is a registered user of the web site holds during the time interval_BEFORE and there exists the time interval_DURING such that the time interval_DURING is an instance of time interval and the time interval_DURING takes place during the time interval and the physical is a registered user of the web site holds during the time interval, then the physical is a member of the collection and the collection is equal to new registrations at the web site during the time interval
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3475-3507	If a time interval is an instance of time interval and a web site is an instance of web site, then there exists a collection such that the collection is an instance of collection and for all an agent if the agent is a member of the collection, then there exists another time interval such that the agent is an instance of agent and the other time interval is an instance of selling and the agent is an agent of the other time interval and the web site is an instrument for the other time interval and the other time interval takes place during the time interval and there doesn't exist the time interval_BEFORE such that the time interval_BEFORE is an instance of time interval and the time interval_BEFORE happens earlier than the time interval and there exists the other time interval_BEFORE such that the other time interval_BEFORE is an instance of selling and the agent is an agent of the other time interval_BEFORE and the web site is an instrument for the other time interval_BEFORE and the other time interval_BEFORE takes place during the time interval holds during the time interval_BEFORE and new sellers at the web site during the time interval is equal to the collection

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement

No TPTP formula. May not be expressible in strict first order.	Government.kif 1203-1210	For all ?AGENT, ?VOTER,, , ?ELECTION and ?VOTING if ?ELECTION is an instance of the election of ?AGENT and ?VOTING is an instance of the voting of ?ELECTION and ?VOTER is an agent of ?VOTING, then male is an attribute of ?VOTER contains information exclusive male suffrage
No TPTP formula. May not be expressible in strict first order.	Government.kif 885-893	For all ?COUNTRY, ?ELECTION,, , ?VOTING and ?VOTER if ?COUNTRY is an instance of nation and ?ELECTION is an instance of the election of ?COUNTRY and ?VOTING is an instance of the voting of ?ELECTION and ?VOTER is an agent of ?VOTING, then ?VOTER is a citizen of ?COUNTRY contains information voter citizenship requirement
No TPTP formula. May not be expressible in strict first order.	Government.kif 1054-1065	For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE if ?AGENT is a citizen of ?POLITY and ?VOTINGAGE year duration(s) is a suffrage age minimum of ?POLITY and the age of ?AGENT is ?AGE year duration(s) and ?AGE is greater than or equal to ?VOTINGAGE and ?ELECTION is an instance of the election of ?POLITY, then ?AGENT is capable of doing the voting of ?ELECTION as a agent contains information universal suffrage law
No TPTP formula. May not be expressible in strict first order.	Government.kif 1122-1136	For all ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE and ?AGE if ?VOTER is a citizen of ?POLITY and ?VOTINGAGE year duration(s) is a suffrage age minimum of ?POLITY and the age of ?VOTER is ?AGE year duration(s) and ?AGE is greater than or equal to ?VOTINGAGE and ?ELECTION is an instance of the election of ?POLITY, then there exists ?VOTING such that ?VOTING is an instance of the voting of ?ELECTION and ?VOTER is an agent of ?VOTING contains information compulsory suffrage law
No TPTP formula. May not be expressible in strict first order.	Media.kif 1972-1980	There exists a time interval such that the time interval is an instance of time interval and the time interval finishes the time of existence of Jesus of Nazareth and the time interval starts the time of existence of Twelve apostles and for all an entity if the entity is a member of Twelve apostles holds during the time interval, then Jesus of Nazareth is a friend of the entity holds during the time interval

appearance as argument number 0

No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14690-14693	For all a real number the real number Ounce(s) is equal to the real number and 16.0 pound mass(s)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4749-4750	For all an integer (the integer+2) is equal to (the integer and 1)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4733-4734	For all an integer (the integer+1) is equal to (the integer and 1)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3035-3038	For all @ROW and another entity length of (@ROW and the other entity) is equal to (length of (@ROW)+1)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3040-3044	For all @ROW and another entity length of (@ROW and the other entity)th element of (@ROW and the other entity) is equal to the other entity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3315-3316	For all @ROW and another entity (@ROW) starts (@ROW and the other entity)

Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)

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

KB Term:			Term intersection

English Word: