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 and RealNumber
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4713-4713	域加成, 2 and RealNumber
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5295-5295	身份元素加成 and 0
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4708-4708	例加成 and AssociativeFunction
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4707-4707	例加成 and BinaryFunction
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4709-4709	例加成 and CommutativeFunction
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4711-4711	例加成 and TotalValuedRelation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4714-4714	範圍加成 and RealNumber

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	等於 SymbolicString and ReverseFn SymbolicString 等於 NonnegativeInteger and SymbolicString 的 length 比較多 NonnegativeInteger and 1 比較多 NonnegativeInteger and 0 少於 NonnegativeInteger and NonnegativeInteger 等於 Integer and 天花板部減法 NonnegativeInteger and 1 and 2 等於 NonnegativeIntegerEW and 加成減法 Integer and NonnegativeInteger and Integer 等於 SymbolicString and SymbolicString 的 sub-string 從 NonnegativeInteger 對於加成 1 and NonnegativeInteger 等於 SymbolicString and SymbolicString 的 sub-string 從 NonnegativeIntegerEW 對於加成 1 and NonnegativeIntegerEW
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 23916-23932	持有期間 TimeInterval and attribute Human and Menopausal Day 是 Human 的 birthdate 例 Day and 天 PositiveInteger and 月 Month and 年 Integer 等於 RealNumber and 加成 49 and Integer 等於 RealNumber and 加成 52 and Integer 等於 TimePoint and 開始 TimeInterval 模態屬性比較多 TimePoint and RealNumber 比較多 RealNumber and TimePoint and 容易
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 1224-1233	例金融賬戶 and 信用賬戶 CognitiveAgent 持有 account 金融賬戶 RealNumber 是金融賬戶的 principal 總額 TimeInterval 是金融賬戶的 agreement 週期金融賬戶是對於 %3 的賺取 interest 等於 RealNumber and 加成 RealNumber and 利益持有義務卡帕 SymbolicString and RealNumber 是 SymbolicString 的 transaction 總額 and CognitiveAgent
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 1273-1282	例貸款 and 貸款貸款是 CognitiveAgent 的 borrower RealNumber 是貸款的 principal 總額 TimeInterval 是貸款的 agreement 週期貸款是對於 %3 的賺取 interest 等於 RealNumber and 加成 RealNumber and 利益持有義務卡帕 SymbolicString and RealNumber 是 SymbolicString 的 transaction 總額 and CognitiveAgent
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 2333-2355	例金融資產 and 零息債券 Day 是金融資產的帳號的 maturity 日期擁有金融資產Holder and 金融資產測量 RealNumber and UnitOfMeasure 是金融資產的帳號的 principal 總額 TimeInterval 是金融資產的帳號的 agreement 週期金融資產的帳號是對於 %3 的賺取 interest 等於 RealNumber and 加成 RealNumber and RealNumber FinancialTransaction 例 FinancialTransaction and 付款目的地 FinancialTransaction and 金融資產Holder 起源 FinancialTransaction and 金融資產的帳號測量 RealNumber and UnitOfMeasure 是 FinancialTransaction 的 transaction 總額
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 436-453	例 FinancialTransaction and 存款例金融賬戶 and 金融賬戶目的地 FinancialTransaction and 金融賬戶的 currency 測量 RealNumber and UnitOfMeasure 是 FinancialTransaction 的 transaction 總額金融賬戶對於 %3 的 current 帳戶存款等於 RealNumber and 加成 RealNumber and RealNumber 金融賬戶對於 %3 的 current 帳戶存款
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1935-1944	例 List and ConsecutiveTimeIntervalList 等於 TimeInterval and 清單順序 List and PositiveInteger 等於 TimeInterval and 清單順序 List and 加成 PositiveInteger and 1 等於開始 TimeInterval and 結束 TimeInterval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5117-5128	等於 Integer and 0 等於加成乘法地板部 Integer and Integer and Integer and Integer and Integer 等於剩餘 Integer and Integer and Integer

consequent

No TPTP formula. May not be expressible in strict first order.	People.kif 272-293	RealNumber 是 List 的 average List PositiveInteger 等於列表長度 List and 列表長度 List 等於清單順序 List and 1 and 清單順序 List and 1 PositiveInteger 在列表中 PositiveInteger and List RealNumber RealNumberMINUSONE, PositiveInteger and PositiveInteger 比較多 RealNumber and 1 小於或等於 RealNumber and 列表長度 List 等於清單順序 List and PositiveInteger and RealNumber 在列表中 PositiveInteger and List 等於 RealNumber and 清單順序 List and PositiveInteger 在列表中 PositiveInteger and List 等於 RealNumberMINUSONE and 減法 RealNumber and 1 等於 RealNumberMINUSONE and 清單順序 List and PositiveInteger 等於 PositiveInteger and 加成 PositiveInteger and PositiveInteger 等於 PositiveInteger and 列表長度 List 等於 RealNumber and 部清單順序 List and PositiveInteger and PositiveInteger
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5993-6006	等於路徑重量 GraphPath and RealNumber 圖形部分 GraphArc and GraphPath 圖形部分 GraphArc and GraphPath 弧重 GraphArc and RealNumber 弧重 GraphArc and RealNumber GraphElement 圖形部分 GraphElement and GraphPath 等於 GraphElement and GraphArc 等於 GraphElement and GraphArc 等於路徑重量 GraphPath and 加成 RealNumber and RealNumber
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5979-5991	等於路徑重量 GraphPath and RealNumber 子圖 GraphPath and GraphPath 圖形部分 GraphArc and GraphPath 弧重 GraphArc and RealNumber GraphElement 圖形部分 GraphElement and GraphPath 圖形部分 GraphElement and GraphPath 等於 GraphElement and GraphArc 等於 RealNumber and 加成路徑重量 GraphPath and RealNumber
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5104-5115	等於剩餘 Integer and Integer and Integer 等於 Integer and 0 等於加成乘法地板部 Integer and Integer and Integer and Integer and Integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3258-3268	等於 RealNumber and ListSumFn List 比較多列表長度 List and 1 等於 RealNumber and 加成 List 的 first and ListSumFn SubListFn 2, 列表長度 List and List
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3083-3102	等於 List and 列表連接 List and List 等於 List and 空列表等於 List and 空列表小於或等於 PositiveInteger and 列表長度 List 小於或等於 PositiveInteger and 列表長度 List 例 PositiveInteger and PositiveInteger 例 PositiveInteger and PositiveInteger 等於清單順序 List and PositiveInteger and 清單順序 List and PositiveInteger 等於清單順序 List and 加成列表長度 List and PositiveInteger and 清單順序 List and PositiveInteger
No TPTP formula. May not be expressible in strict first order.	Media.kif 3068-3089	等於 SymbolicString and ReverseFn SymbolicString 等於 NonnegativeInteger and SymbolicString 的 length 比較多 NonnegativeInteger and 1 比較多 NonnegativeInteger and 0 少於 NonnegativeInteger and NonnegativeInteger 等於 Integer and 天花板部減法 NonnegativeInteger and 1 and 2 等於 NonnegativeIntegerEW and 加成減法 Integer and NonnegativeInteger and Integer 等於 SymbolicString and SymbolicString 的 sub-string 從 NonnegativeInteger 對於加成 1 and NonnegativeInteger 等於 SymbolicString and SymbolicString 的 sub-string 從 NonnegativeIntegerEW 對於加成 1 and NonnegativeIntegerEW
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3190-3202	等於 List and SubListFn PositiveInteger, Integer and List 比較多減法 Integer and PositiveInteger and 1 等於 List and 列表連接名單清單順序 List and PositiveInteger and SubListFn 加成 1 and PositiveInteger, Integer and List
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1453-1465	等於 RealNumber and VarianceAverageFn Number and List 比較多列表長度 List and 1 等於 RealNumber and 加成 VarianceAverageFn Number and 清單順序 List and 1 and VarianceAverageFn Number and SubListFn 2, 列表長度 List and List
No TPTP formula. May not be expressible in strict first order.	Food.kif 1248-1262	例 Object and Mixture 例 UnitOfMeasure and UnitOfMeasure mixtureRatio Substance, Substance, RealNumber, RealNumber and UnitOfMeasure 測量 Object and 測量 RealNumber and UnitOfMeasure 部分 Substance and Object 部分 Substance and Object 測量 Substance and 測量 RealNumber and UnitOfMeasure 測量 Substance and 測量 RealNumber and UnitOfMeasure 等於 RealNumber and 加成 RealNumber and RealNumber
No TPTP formula. May not be expressible in strict first order.	Biography.kif 69-85	例 Process and BarMitzvah 患者 Process and Human 例 Human and 男孩會員 Human and Collection 例 Collection and 猶太教 Day 是 Human 的 birthdate 例 Day and 天 PositiveInteger and 月 Month and 年 Integer Integer3 TimePosition 例 Integer3 and Integer 等於 Integer3 and 加成 Integer and 13 例 TimePosition and 天 PositiveInteger and 月 Month and 年 Integer3 等於何時 Process and 眼前的未來 TimePosition
No TPTP formula. May not be expressible in strict first order.	Biography.kif 99-115	例 Process and BatMitzvah 患者 Process and Human 例 Human and 女孩會員 Human and Collection 例 Collection and 猶太教 Day 是 Human 的 birthdate 例 Day and 天 PositiveInteger and 月 Month and 年 Integer Integer3 TimePosition 例 Integer3 and Integer 等於 Integer3 and 加成 Integer and 13 例 TimePosition and 天 PositiveInteger and 月 Month and 年 Integer3 等於何時 Process and 眼前的未來 TimePosition
No TPTP formula. May not be expressible in strict first order.	Geography.kif 555-560	例 UnitOfMeasure and UnitOfArea 測量 RealNumber and UnitOfMeasure 是只對 GeographicArea 的 land 地區測量 RealNumber and UnitOfMeasure 是只對 GeographicArea 的 water 區域測量加成 RealNumber and RealNumber and UnitOfMeasure 是 GeographicArea 的 total 區域
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17206-17212	例 TimePosition and 小時 NonnegativeInteger and 天 PositiveInteger and 月 Month and 年 Integer 例 TimePosition and 小時 NonnegativeInteger and 天 PositiveInteger and 月 Month and 年 Integer 等於相對時間 TimePosition and 中央時區 and TimePosition 等於 NonnegativeInteger and 加成 NonnegativeInteger and 6
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17218-17224	例 TimePosition and 小時 NonnegativeInteger and 天 PositiveInteger and 月 Month and 年 Integer 例 TimePosition and 小時 NonnegativeInteger and 天 PositiveInteger and 月 Month and 年 Integer 等於相對時間 TimePosition and 東部時區 and TimePosition 等於 NonnegativeInteger and 加成 NonnegativeInteger and 5
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17194-17200	例 TimePosition and 小時 NonnegativeInteger and 天 PositiveInteger and 月 Month and 年 Integer 例 MonthST and 小時 NonnegativeInteger and 天 PositiveInteger and 月 Month and 年 Integer 等於相對時間 TimePosition and 山區時區 and MonthST 等於 NonnegativeInteger and 加成 NonnegativeInteger and 7
No TPTP formula. May not be expressible in strict first order.	Merge.kif 17182-17188	例 TimePosition and 小時 NonnegativeInteger and 天 PositiveInteger and 月 Month and 年 Integer 例 TimePosition and 小時 NonnegativeInteger and 天 PositiveInteger and 月 Month and 年 Integer 等於相對時間 TimePosition and 太平洋時區 and TimePosition 等於 NonnegativeInteger and 加成 NonnegativeInteger and 8
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 510-517	測量 RealNumber and UnitOfMeasure 是 GeographicArea 的 total 高速公路系統長度測量 RealNumber and UnitOfMeasure 是 GeographicArea 的鋪設鐵路 length 測量 RealNumber and UnitOfMeasure 是 GeographicArea 的未鋪設高速公路 length 例 UnitOfMeasure and UnitOfLength 測量加成 RealNumber and RealNumber and UnitOfMeasure 是 GeographicArea 的 total 高速公路系統長度
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 503-508	測量 RealNumber and UnitOfMeasure 是 GeographicArea 的 total 高速公路系統長度測量 RealNumber and UnitOfMeasure 是 GeographicArea 的鋪設鐵路 length 測量 RealNumber and UnitOfMeasure 是 GeographicArea 的未鋪設高速公路 length 等於 RealNumber and 加成 RealNumber and RealNumber
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 6501-6509	CompoundSubstance 是 CompoundSubstance 的 conjugate PositiveInteger PositiveInteger PositiveInteger 是 CompoundSubstance 的 proton 號碼 PositiveInteger 是 CompoundSubstance 的 proton 號碼等於 PositiveInteger and 加成 PositiveInteger and 1 等於 PositiveInteger and 加成 PositiveInteger and 1

statement

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

Merge.kif 4720-4721

Integer 等於接班人 Integer and 加成 Integer and 1

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

KB Term:			Term intersection

English Word: