TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1500-1501
No TPTP formula. May not be expressible in strict first order.	Merge.kif 397-399
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 63-64
No TPTP formula. May not be expressible in strict first order.	spanish_format.kif 72-74
No TPTP formula. May not be expressible in strict first order.	Merge.kif 395-395	The number 1 argument of disjoint is an instance of class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 396-396	The number 2 argument of disjoint is an instance of class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 393-393	disjoint is an instance of binary predicate
No TPTP formula. May not be expressible in strict first order.	Merge.kif 394-394	disjoint is an instance of symmetric relation

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 285-285
No TPTP formula. May not be expressible in strict first order.	english_format.kif 290-290
No TPTP formula. May not be expressible in strict first order.	french_format.kif 165-165
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 75-75
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 1985-1985
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 117-117
No TPTP formula. May not be expressible in strict first order.	relations-cb.txt 109-109
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 182-182
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 370-370
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 59-59
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 185-185
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 172-172
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 166-166
No TPTP formula. May not be expressible in strict first order.	Merge.kif 569-569	disjoint decomposition is internally related to disjoint
No TPTP formula. May not be expressible in strict first order.	Merge.kif 414-414	disjoint relation is internally related to disjoint
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 286-286
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 19848-19848
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 19847-19847
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 19846-19846
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 167-167

antecedent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 419-424	If the number a positive integer argument of a relation is an instance of a class and the number the positive integer argument of another relation is an instance of another class and the class is disjoint from the other class, then the relation and the other relation are disjoint
No TPTP formula. May not be expressible in strict first order.	Merge.kif 426-431	If the number a positive integer argument of a relation is a subclass of a class and the number the positive integer argument of another relation is a subclass of another class and the class is disjoint from the other class, then the relation and the other relation are disjoint
No TPTP formula. May not be expressible in strict first order.	Merge.kif 433-438	If the range of a function is an instance of a class and the range of another function is an instance of another class and the class is disjoint from the other class, then the function and the other function are disjoint
No TPTP formula. May not be expressible in strict first order.	Merge.kif 440-445	If the values returned by a function are subclasses of a kind of class and the values returned by another function are subclasses of another kind of class and a kind of class is disjoint from another kind of class, then the function and the other function are disjoint
No TPTP formula. May not be expressible in strict first order.	Merge.kif 401-407	If a class is disjoint from another class, then there doesn't exist an entity such that the entity is an instance of the class and the entity is an instance of the other class

consequent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 2955-2960	If a class is disjointly decomposed into another class, a third class, and a fourth class, then the other class is disjoint from the third class and the third class is disjoint from the fourth class and the fourth class is disjoint from the other class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2944-2953	If a class is disjointly decomposed into @ROW, then for all a third class and a fourth class if the third class is a member of (@ROW) and the fourth class is a member of (@ROW) and the third class is not equal to the fourth class, then the third class is disjoint from the fourth class

appearance as argument number 0

No TPTP formula. May not be expressible in strict first order.	MilitaryProcesses.kif 974-974	Above the line is disjoint from below the line
No TPTP formula. May not be expressible in strict first order.	Merge.kif 8778-8778	Afternoon is disjoint from evening
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 360-360	Alt key is disjoint from control key
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 362-362	Alt key is disjoint from function key
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 361-361	Alt key is disjoint from shift key
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 1313-1313	Alt key hold down is disjoint from control key hold down
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 1312-1312	Alt key hold down is disjoint from shift key hold down
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 8205-8205	Anaerobic exercise device is disjoint from aerobic exercise device
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 19012-19012	Ante meridiem is disjoint from post meridiem
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 6909-6909	Apartment building is disjoint from single family residence
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 295-295	Arrow key is disjoint from enter key
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14613-14613	Article is disjoint from book
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 172-172	Artillery cannon is disjoint from military tank
No TPTP formula. May not be expressible in strict first order.	Economy.kif 5837-5837	Asphalt is disjoint from fossil fuel
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13916-13916	Astronomical body is disjoint from geographic area
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12241-12241	Attaching is disjoint from detaching
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 1656-1656	Audio input is disjoint from joystick motion
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 1657-1657	Audio input is disjoint from keyboard action
No TPTP formula. May not be expressible in strict first order.	ComputerInput.kif 1655-1655	Audio input is disjoint from touch surface action
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10150-10150	Autonomic process is disjoint from intentional process
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 15672-15672	Barn is disjoint from residential building
No TPTP formula. May not be expressible in strict first order.	Sports.kif 740-740	Baseball steal is disjoint from baseball hit
No TPTP formula. May not be expressible in strict first order.	Sports.kif 739-739	Baseball steal is disjoint from baseball walk
No TPTP formula. May not be expressible in strict first order.	Sports.kif 748-748	Baseball strike is disjoint from baseball hit
No TPTP formula. May not be expressible in strict first order.	Sports.kif 696-696	Baseball walk is disjoint from baseball hit

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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

KB Term:			Term intersection

English Word: