TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 2214-2215
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4716-4718
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 878-879
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4712-4712	加法函数的 1 数量是实数的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4713-4713	加法函数的 2 数量是实数的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5295-5295	0 是加法函数的单位元
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4708-4708	加法函数是结合函数的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4707-4707	加法函数是二元函数的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4709-4709	加法函数是交换函数的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4711-4711	加法函数是总值关系的 instance
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4714-4714	加法函数的 range 是实数的实例

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 682-682
No TPTP formula. May not be expressible in strict first order.	english_format.kif 684-684
No TPTP formula. May not be expressible in strict first order.	french_format.kif 414-414
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 20-20
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 2131-2131
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 366-366
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 423-423
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 889-889
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 65-65
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 436-436
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 458-458
No TPTP formula. May not be expressible in strict first order.	relations-cb.txt 54-54
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 5418-5418
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 683-683
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 5417-5417
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 5416-5416
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 57-57

antecedent

No TPTP formula. May not be expressible in strict first order.	Media.kif 3068-3089	如果符号串 equal ReverseFn 另一个符号串和非负整数 equal 那个另外符号串的 length 和那个非负整数是 greaterThan 1 和另一个非负整数是 greaterThan 0 和那个另外非负整数是 lessThan 那个非负整数和整数 equal 取(那个非负整数和 1) 和 2 的顶整数和那个另外非负整数EW equal ((那个整数和那个另外非负整数) 和那个整数) 和第三符号串 equal 那个另外符号串的 sub-string 从那个另外非负整数对于 (1 和那个另外非负整数) ，然后那个第三符号串 equal 那个符号串的 sub-string 从那个另外非负整数EW 对于 (1 和那个另外非负整数EW)
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 23916-23932	如果 Menopausal 是人类的 attribute 在时距 holdsDuring 和日是那个人类的 birthdate 和那个日是正整数 day 的 instance 和实数 equal (49 和整数) 和另一个实数 equal (52 和那个整数) 和时点 equal 那个时距的开始，然后那个时点是 greaterThan 那个实数和那个另外实数是 greaterThan 那个时点的声明 has 容易的语气
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 1224-1233	如果金融账户是信用账户的 instance 和有认知的主事持有 account 那个金融账户和实数是那个金融账户的 principal 总额和时距是那个金融账户的 agreement 週期和那个金融账户是对于 %3 的赚取 interest 和另一个实数 equal (那个实数和利益)，然后那个有认知的主事有义务执行符号串所描述的类别的任务
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 1273-1282	如果贷款是贷款的 instance 和那个贷款是有认知的主事的 borrower 和实数是那个贷款的 principal 总额和时距是那个贷款的 agreement 週期和那个贷款是对于 %3 的赚取 interest 和另一个实数 equal (那个实数和利益)，然后那个有认知的主事有义务执行符号串所描述的类别的任务
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2333-2355	如果金融资产是零息债券的 instance 和日是那个金融资产的帐号的 maturity 日期和那个金融资产Holder possesses 那个金融资产和实数测量单位是那个金融资产的帐号的 principal 总额和时距是那个金融资产的帐号的 agreement 週期和那个金融资产的帐号是对于 %3 的赚取 interest 和另一个实数 equal (那个实数和第三实数)，然后有存在金融交易这样那个金融交易是付款的 instance 和那个金融交易在那个金融资产Holder 结束和那个金融资产的帐号是那个金融交易的源头和那个另外实数那个测量单位是那个金融交易的 transaction 总额
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 436-453	如果金融交易是存款的 instance 和金融账户是金融账户的 instance 和那个金融交易在那个金融账户的 currency 结束和实数测量单位是那个金融交易的 transaction 总额和那个金融账户对于 %3 的 current 帐户存款和另一个实数 equal (第三实数和那个实数)，然后那个金融账户对于 %3 的 current 帐户存款
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1935-1944	如果串列是连续时间间隔表列的 instance 和时距 equal 那个串列的第正整数几个元素和另一个时距 equal 那个串列的第 (那个正整数和 1) 几个元素，然后那个另外时距的开始 equal 那个时距的结束
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5117-5128	如果整数不 equal 0 和 (取另一个整数和那个整数的底整数和那个整数和第三整数) equal 那个另外整数，然后那个另外整数模除那个整数 equal 那个第三整数

consequent

No TPTP formula. May not be expressible in strict first order.	People.kif 272-293	实数是串列的 average 若且唯若有存在另一个串列和正整数这样那个另外串列的长度 equal 那个串列的长度和那个另外串列的第 1 几个元素 equal 那个串列的第 1 几个元素和对所有另一个正整数如果那个另外正整数是那个另外串列的 member，然后有存在另一个实数，那个另外实数MINUSONE,，，第三正整数， and 和第四正整数这样那个另外实数是 greaterThan 1 和那个另外实数是 lessThanOrEqualTo 那个另外串列的长度和那个另外串列的第那个另外正整数几个元素 equal 那个另外实数和那个第三正整数是那个串列的 member 和那个另外实数 equal 那个串列的第那个第三正整数几个元素和那个第四正整数是那个另外串列的 member 和那个另外实数MINUSONE equal (那个另外实数和 1) 和那个另外实数MINUSONE equal 那个另外串列的第那个第四正整数几个元素和那个另外正整数 equal (那个第三正整数和那个第四正整数) 和那个正整数 equal 那个另外串列的长度和那个实数 equal 那个另外串列的第那个正整数几个元素和那个正整数
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5993-6006	如果图路径的值 equal 实数和图弧是那个图路径的 part 和另一个图弧是那个图路径的 part 和那个图弧的值是另一个实数和那个另外图弧的值是第三实数和对所有图元素如果那个图元素是那个图路径的 part，然后那个图元素 equal 那个图弧或那个图元素 equal 那个另外图弧，然后那个图路径的值 equal (那个另外实数和那个第三实数)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5979-5991	如果图路径的值 equal 实数和另一个图路径是那个图路径的 subGraph 和图弧是那个图路径的 part 和那个图弧的值是另一个实数和对所有图元素如果那个图元素是那个图路径的 part，然后那个图元素是那个另外图路径的 part 或那个图元素 equal 那个图弧，然后那个实数 equal (那个另外图路径的值和那个另外实数)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5104-5115	如果整数模除另一个整数 equal 第三整数和那个另外整数不 equal 0，然后 (取那个整数和那个另外整数的底整数和那个另外整数和那个第三整数) equal 那个整数
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3258-3268	如果实数 equal ListSumFn 串列和那个串列的长度是 greaterThan 1，然后那个实数 equal (那个串列的 first 和 ListSumFn SubListFn 2, 那个串列的长度 and 那个串列)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3083-3102	如果串列 equal List包含另一个串列和第三串列和那个另外串列不 equal 空列表和那个第三串列不 equal 空列表和正整数是 lessThanOrEqualTo 那个另外串列的长度和另一个正整数是 lessThanOrEqualTo 那个第三串列的长度和那个正整数是正整数的 instance 和那个另外正整数是正整数的 instance，然后那个串列的第那个正整数几个元素 equal 那个另外串列的第那个正整数几个元素和那个串列的第 (那个另外串列的长度和那个另外正整数) 几个元素 equal 那个第三串列的第那个另外正整数几个元素
No TPTP formula. May not be expressible in strict first order.	Media.kif 3068-3089	如果符号串 equal ReverseFn 另一个符号串和非负整数 equal 那个另外符号串的 length 和那个非负整数是 greaterThan 1 和另一个非负整数是 greaterThan 0 和那个另外非负整数是 lessThan 那个非负整数和整数 equal 取(那个非负整数和 1) 和 2 的顶整数和那个另外非负整数EW equal ((那个整数和那个另外非负整数) 和那个整数) 和第三符号串 equal 那个另外符号串的 sub-string 从那个另外非负整数对于 (1 和那个另外非负整数) ，然后那个第三符号串 equal 那个符号串的 sub-string 从那个另外非负整数EW 对于 (1 和那个另外非负整数EW)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3190-3202	如果串列 equal SubListFn 正整数, 整数 and 另一个串列和 (那个整数和那个正整数) 是 greaterThan 1，然后那个串列 equal List包含 (那个另外串列的第那个正整数几个元素) 和 SubListFn (1 和那个正整数), 那个整数 and 那个另外串列
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1453-1465	如果实数 equal 方差均差函数数字 and 串列和那个串列的长度是 greaterThan 1，然后那个实数 equal (方差均差函数那个数字 and 那个串列的第 1 几个元素和方差均差函数那个数字 and SubListFn 2, 那个串列的长度 and 那个串列)
No TPTP formula. May not be expressible in strict first order.	Food.kif 1248-1262	如果客体是混合物的 instance 和测量单位是测量单位的 instance 和 mixtureRatio 物质, 另一个物质, 实数, 另一个实数 and 那个测量单位和那个客体的 measure 是第三实数那个测量单位和那个物质是那个客体的 part 和那个另外物质是那个客体的 part 和那个物质的 measure 是那个实数那个测量单位和那个另外物质的 measure 是那个另外实数那个测量单位，然后那个第三实数 equal (那个实数和那个另外实数)
No TPTP formula. May not be expressible in strict first order.	Biography.kif 69-85	如果过程是 BarMitzvah 的 instance 和人类是那个过程的 patient 和那个人类是男孩的 instance 和那个人类是群体的 member 和那个群体是犹太教的 instance 和日是那个人类的 birthdate 和那个日是正整数 day 的 instance，然后有存在整数和时间位置这样那个整数是整数的 instance 和那个整数 equal (另一个整数和 13) 和那个时间位置是那个正整数 day 的 instance 和那个过程出现的 time equal 紧接那个时间位置 after
No TPTP formula. May not be expressible in strict first order.	Biography.kif 99-115	如果过程是 BatMitzvah 的 instance 和人类是那个过程的 patient 和那个人类是女孩的 instance 和那个人类是群体的 member 和那个群体是犹太教的 instance 和日是那个人类的 birthdate 和那个日是正整数 day 的 instance，然后有存在整数和时间位置这样那个整数是整数的 instance 和那个整数 equal (另一个整数和 13) 和那个时间位置是那个正整数 day 的 instance 和那个过程出现的 time equal 紧接那个时间位置 after
No TPTP formula. May not be expressible in strict first order.	Geography.kif 555-560	如果测量单位是 UnitOfArea 的 instance 和实数那个测量单位是只对地理区域的 land 地区和另一个实数那个测量单位是只对那个地理区域的 water 区域，然后 (那个实数和那个另外实数) 那个测量单位是那个地理区域的 total 區域
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17206-17212	如果时间位置是非负整数 hour 的 instance 和另一个时间位置是另一个非负整数 hour 的 instance 和时间那个时间位置在时区中央时区 equal 那个另外时间位置，然后那个另外非负整数 equal (那个非负整数和 6)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17218-17224	如果时间位置是非负整数 hour 的 instance 和另一个时间位置是另一个非负整数 hour 的 instance 和时间那个时间位置在时区东部时区 equal 那个另外时间位置，然后那个另外非负整数 equal (那个非负整数和 5)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17194-17200	如果时间位置是非负整数 hour 的 instance 和另一个时间位置是另一个非负整数 hour 的 instance 和时间那个时间位置在时区山区时区 equal 那个另外时间位置，然后那个另外非负整数 equal (那个非负整数和 7)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17182-17188	如果时间位置是非负整数 hour 的 instance 和另一个时间位置是另一个非负整数 hour 的 instance 和时间那个时间位置在时区太平洋时区 equal 那个另外时间位置，然后那个另外非负整数 equal (那个非负整数和 8)
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 510-517	如果实数测量单位是地理区域的 total 高速公路系统长度和那个实数1 那个测量单位是那个地理区域的铺设铁路 length 和那个实数2 那个测量单位是那个地理区域的未铺设高速公路 length 和那个测量单位是 UnitOfLength 的 instance，然后 (那个实数1 和那个实数2) 那个测量单位是那个地理区域的 total 高速公路系统长度
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 503-508	如果实数测量单位是地理区域的 total 高速公路系统长度和那个实数1 那个测量单位是那个地理区域的铺设铁路 length 和那个实数2 那个测量单位是那个地理区域的未铺设高速公路 length ，然后那个实数 equal (那个实数1 和那个实数2)
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 6501-6509	如果复合物质是另一个复合物质的 conjugate ，然后有存在正整数和另一个正整数这样那个正整数是那个另外复合物质的 proton 号码和那个另外正整数是那个复合物质的 proton 号码和那个正整数 equal (那个另外正整数和 1) 或那个另外正整数 equal (那个正整数和 1)

statement

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

Merge.kif 4720-4721

对所有整数 (那个整数+1) equal (那个整数和 1)

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

KB Term:			Term intersection

English Word: