TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 2318-2322
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5586-5594
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 991-995
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5582-5582	O argumento numero 1 de KappaFn e' uma instancia de Sequencia Simbolica
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5583-5583	O argumento numero 2 de KappaFn e' uma instancia de Formula
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5580-5580	KappaFn e' uma instancia de Funcao Binaria
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5581-5581	KappaFn e' uma instancia de Relacao Parcial
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5584-5584	O contra-dominio de KappaFn e' uma instancia de Classe

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 508-508
No TPTP formula. May not be expressible in strict first order.	english_format.kif 513-513
No TPTP formula. May not be expressible in strict first order.	french_format.kif 297-297
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 157-157
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 2074-2074
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 249-249
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 662-662
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 196-196
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 318-318
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 325-325
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 315-315
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 32125-32125
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 509-509
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 32124-32124
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 32123-32123

antecedent

No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 1007-1011	Entidade e' uma instancia de PersonalAccount o numero de instancias dentro de a classe descrita por Sequencia Simbolica e' maior que 1 Entidade e' uma instancia de JointAccount
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3239-3259	Colecao e' uma instancia de Colecao Numero Real e' uma instancia de Medida de Divisa Numero Inteiro e' uma instancia de Numero Real Numero Real e' igual a GMBFn Colecao Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica ABPFn Colecao e' igual a Numero Real + Numero Inteiro
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3282-3302	Colecao e' uma instancia de Colecao Numero Real e' uma instancia de Medida de Divisa Numero Inteiro e' uma instancia de Numero Real Numero Real e' igual a GMVFn Colecao Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica ASPFn Colecao e' igual a Numero Real + Numero Inteiro

consequent

No TPTP formula. May not be expressible in strict first order.	People.kif 357-390	Ano e' uma instancia de o ano AnoEAR MaleLifeExpectancyAtBirthFn Area Geopolitica and Ano e' igual a Numero Real Lista Numero Inteiro, Sequencia Simbolica, Entidade, Entidade and Entidade Lista e' uma instancia de Lista comprimento de Lista e' uma instancia de Numero Inteiro ListaITEM ListaITEM e' um membro de Lista ListaITEM e' uma instancia de Sequencia Simbolica Entidade Entidade e' uma instancia de Sequencia Simbolica Entidade e' um membro de Lista Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica average Lista and Numero Real
No TPTP formula. May not be expressible in strict first order.	People.kif 82-97	Ano e' uma instancia de o ano Numero Inteiro BirthsPerThousandFn Area Geopolitica and Ano e' igual a Numero Real PopulationFn Area Geopolitica + 1000 e' igual a Numero Real Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica Numero Inteiro + Numero Real e' igual a Numero Real
No TPTP formula. May not be expressible in strict first order.	People.kif 118-133	Ano e' uma instancia de o ano Numero Inteiro DeathsPerThousandFn Area Geopolitica and Ano e' igual a Numero Real PopulationFn Area Geopolitica + 1000 e' igual a Numero Real Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica Numero Inteiro + Numero Real e' igual a Numero Real
No TPTP formula. May not be expressible in strict first order.	People.kif 238-264	Ano e' uma instancia de o ano Numero Inteiro DeathsPerThousandLiveBirthsFn Area Geopolitica and Ano e' igual a Numero Real Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica Numero Inteiro + 1000 e' igual a Numero Real Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica Numero Inteiro + Numero Real e' igual a Numero Real
No TPTP formula. May not be expressible in strict first order.	People.kif 403-436	Ano e' uma instancia de o ano Numero Inteiro FemaleLifeExpectancyAtBirthFn Area Geopolitica and Ano e' igual a Numero Real Lista Numero Inteiro, Sequencia Simbolica, Entidade, Entidade and Entidade Lista e' uma instancia de Lista comprimento de Lista e' uma instancia de Numero Inteiro ListaITEM ListaITEM e' um membro de Lista ListaITEM e' uma instancia de Sequencia Simbolica Entidade Entidade e' uma instancia de Sequencia Simbolica Entidade e' um membro de Lista Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica average Lista and Numero Real
No TPTP formula. May not be expressible in strict first order.	People.kif 310-342	Ano e' uma instancia de o ano Numero Inteiro LifeExpectancyAtBirthFn Area Geopolitica and Ano e' igual a Numero Real Lista Numero Inteiro, Sequencia Simbolica, Entidade, Entidade and Entidade Lista e' uma instancia de Lista comprimento de Lista e' uma instancia de Numero Inteiro ListaITEM ListaITEM e' um membro de Lista ListaITEM e' uma instancia de Sequencia Simbolica Entidade Entidade e' uma instancia de Sequencia Simbolica Entidade e' um membro de Lista Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica average Lista and Numero Real
No TPTP formula. May not be expressible in strict first order.	People.kif 156-187	Ano e' uma instancia de o ano Numero Inteiro MigrantsPerThousandFn Area Geopolitica and Ano e' igual a Numero Real ( Numero Inteiro + Numero Inteiro) e' igual a 1 Entidade e' uma instancia de o ano Numero Inteiro PopulationFn Area Geopolitica e' igual a Numero Real vale durante Ano Numero Real + 1000 e' igual a Numero Real Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica ( Numero Inteiro + Numero Inteiro) e' igual a Numero Real Numero Real + Numero Real e' igual a Numero Real
No TPTP formula. May not be expressible in strict first order.	People.kif 206-223	MaleToFemaleRatioFn Area Geopolitica e' igual a Numero Real Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica Numero Inteiro e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica Numero Inteiro + Numero Inteiro e' igual a Numero Real
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 182-189	lengthOfBroadGaugeRailway Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 712-719	lengthOfCrudeOilPipeline Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 210-217	lengthOfDualGaugeRailway Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 126-133	lengthOfElectrifiedRailway Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 568-575	lengthOfExpresswaySystem Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 154-161	lengthOfMultipleTrackRailway Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 237-244	lengthOfNarrowGaugeRailway Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 735-742	lengthOfNaturalGasPipeline Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 542-549	lengthOfPavedHighway Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 758-765	lengthOfPetroleumProductPipeline Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 265-272	lengthOfStandardGaugeRailway Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 294-306	lengthOfUnclassifiedGaugeRailway Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 601-608	lengthOfUnpavedHighway Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 1277-1287	totalFacilityTypeInArea Area Geografica, a classe correspondente a AirportWithPavedRunway and Numero Inteiro nao-negativo Sequencia Simbolica Entidade cardinality a classe descrita por Sequencia Simbolica and Numero Inteiro nao-negativo
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 1221-1228	totalFacilityTypeInArea Area Geografica, Classe and Numero Inteiro nao-negativo cardinality a classe descrita por Sequencia Simbolica and Numero Inteiro nao-negativo
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 484-491	totalLengthOfHighwaySystem Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 98-105	totalLengthOfRailwaySystem Area Geografica and Medida de Comprimento o comprimento de a classe descrita por Sequencia Simbolica e' Medida de Comprimento

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.	People.kif 456-469	Ano e' uma instancia de o ano Numero Inteiro ChildrenBornPerWomanFn Area Geopolitica and Ano e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica
No TPTP formula. May not be expressible in strict first order.	Military.kif 872-881	AvailableForMilitaryServiceMaleFn Area Geopolitica e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica
No TPTP formula. May not be expressible in strict first order.	Military.kif 895-906	FitForMilitaryServiceMaleFn Area Geopolitica e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 31734-31739	OrganismPopulationFn Organismo and Area Geografica e' igual a o numero de instancias dentro de a classe descrita por OrganismoI
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 31712-31717	PopulationFn Area Geopolitica e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica
No TPTP formula. May not be expressible in strict first order.	Military.kif 933-946	ReachingMilitaryAgeAnnuallyMaleFn Area Geopolitica and Ano e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica

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

KB Term:			Term intersection

English Word: