TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 2220-2223
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4746-4750
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 884-887
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4742-4742	O argumento numero 1 de DivisionFn e' uma instancia de Numero Real
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4743-4743	O argumento numero 2 de DivisionFn e' uma instancia de Numero Real
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5297-5297	1 e' um elemento identificador de DivisionFn
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4739-4739	DivisionFn e' uma instancia de Funcao Binaria
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4741-4741	DivisionFn e' uma instancia de Relacao Parcial
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4744-4744	O contra-dominio de DivisionFn e' uma instancia de Numero Real

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 686-686
No TPTP formula. May not be expressible in strict first order.	english_format.kif 688-688
No TPTP formula. May not be expressible in strict first order.	french_format.kif 416-416
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 80-80
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 2133-2133
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 368-368
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 425-425
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 893-893
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 120-120
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 438-438
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 460-460
No TPTP formula. May not be expressible in strict first order.	relations-cb.txt 114-114
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 19992-19992
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 687-687
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 19991-19991
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 19990-19990
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 176-176

antecedent

No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 17948-17959	approximateDiameter Objeto auto-conectado and Numero Real Numero RealM(s) sphereRadius Objeto and Numero Real + 2.0 Numero RealM(s) a medida de Objeto e' Numero Real Unidade de Medida(s) a medida de Objeto auto-conectado e' Numero Real Unidade de Medida(s) Numero RealM e' uma instancia de UnitOfLength Unidade de Medida e' uma instancia de UnitOfVolume Numero Real e' igual a Numero Real
No TPTP formula. May not be expressible in strict first order.	Media.kif 3068-3089	Sequencia Simbolica e' igual a ReverseFn Sequencia Simbolica Numero Inteiro nao-negativo e' igual a StringLengthFn Sequencia Simbolica Numero Inteiro nao-negativo e' maior que 1 Numero Inteiro nao-negativo e' maior que 0 Numero Inteiro nao-negativo e' menos que Numero Inteiro nao-negativo Numero Inteiro e' igual a o teto de ( Numero Inteiro nao-negativo + 1) + 2 Numero Inteiro nao-negativoEW e' igual a (( Numero Inteiro + Numero Inteiro nao-negativo) + Numero Inteiro) Sequencia Simbolica e' igual a SubstringFn Sequencia Simbolica, Numero Inteiro nao-negativo and (1 + Numero Inteiro nao-negativo) Sequencia Simbolica e' igual a SubstringFn Sequencia Simbolica, Numero Inteiro nao-negativoEW and (1 + Numero Inteiro nao-negativoEW)
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4645-4658	Objeto e' uma instancia de CoffeeArabica a medida de Objeto e' Numero Real Gram(s) ObjetoC e' uma instancia de Caffeine ObjetoC e' uma &parte de Objeto a medida de ObjetoC e' Numero Real Gram(s) Numero Real e' igual a Numero Real + Numero Real Numero Real e' maior ou igual a 0.008 Numero Real e' menor ou igual a 0.014
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4669-4682	Objeto e' uma instancia de CoffeeRobusta a medida de Objeto e' Numero Real Gram(s) ObjetoC e' uma instancia de Caffeine ObjetoC e' uma &parte de Objeto a medida de ObjetoC e' Numero Real Gram(s) Numero Real e' igual a Numero Real + Numero Real Numero Real e' maior ou igual a 0.017 Numero Real e' menor ou igual a 0.04
No TPTP formula. May not be expressible in strict first order.	Geography.kif 2215-2225	irrigatedLandArea Area Geografica and Numero Real Unidade de Medida(s) Unidade de Medida e' uma instancia de UnitOfArea totalArea Area Geografica and Numero Real Unidade de Medida(s) Numero Real e' igual a Numero Real + Numero Real irrigatedLandArea Area Geografica and Numero Real Unidade de Medida(s)
No TPTP formula. May not be expressible in strict first order.	Geography.kif 2227-2237	irrigatedLandArea Area Geografica and Numero Real Unidade de Medida(s) totalArea Area Geografica and Numero Real Unidade de Medida(s) Unidade de Medida e' uma instancia de UnitOfArea Numero Real e' igual a Numero Real + Numero Real irrigatedLandArea Area Geografica and Numero Real Unidade de Medida(s)
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3735-3756	A medida de Objeto e' Numero Real Lumen(s) a medida de Objeto e' Numero Real Lumen(s) Objeto e' uma &parte de Objeto Objeto e' uma &parte de Objeto Objeto e' igual a Objeto Numero Real e' maior que Numero Real Numero Real + Numero Real e' igual a Numero Real contrastRatio Objeto and Numero Real Objeto Objeto, Numero Real and Numero Real a medida de Objeto e' Numero Real Lumen(s) a medida de Objeto e' Numero Real Lumen(s) Objeto e' uma &parte de Objeto Objeto e' uma &parte de Objeto Objeto e' igual a Objeto Numero Real e' maior que Numero Real Numero Real + Numero Real e' maior que Numero Real
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5117-5128	Numero Inteiro e' igual a 0 (o maior numero inteiro menor or igual a Numero Inteiro + Numero Inteiro + Numero Inteiro + Numero Inteiro) e' igual a Numero Inteiro Numero Inteiro mod Numero Inteiro e' igual a Numero Inteiro
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 538-548	principalAmount FinancialAccount and Numero Real Unidade de Medida(s) fixedInterestRate FinancialAccount and Numero Real simpleInterest FinancialAccount, Numero Real Unidade de Medida(s) and Intervalo Temporal Numero Real-Decimal e' igual a Numero Real + 100 Numero Real e' igual a Numero Real + Numero Real-Decimal
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 587-597	simpleInterest FinancialAccount, Numero Real Unidade de Medida(s) and Intervalo Temporal principalAmount FinancialAccount and Numero Real Unidade de Medida(s) Numero Real-Decimal e' igual a Numero Real + Numero Real Numero Real e' igual a Numero Real-Decimal + 100.0 interestRatePerPeriod FinancialAccount, Numero Real and Intervalo Temporal

consequent

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 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 52-64	Ano e' uma instancia de o ano Numero Inteiro PopulationGrowthFn Area Geopolitica and Ano e' igual a Numero Real ( Numero Inteiro + Numero InteiroP) e' igual a 1 Posicao Temporal e' uma instancia de o ano Numero InteiroP PopulationFn Area Geopolitica e' igual a Numero Real vale durante Ano PopulationFn Area Geopolitica e' igual a Numero Real vale durante Posicao Temporal Numero Real + Numero Real e' igual a Numero Real ( Numero Real + 1) e' igual a Numero Real
No TPTP formula. May not be expressible in strict first order.	People.kif 272-293	average Lista and Numero Real Lista Inteiro positivo comprimento de Lista e' igual a comprimento de Lista 1th elemento de Lista e' igual a 1th elemento de Lista Inteiro positivo Inteiro positivo e' um membro de Lista Numero Real Numero RealMINUSONE, Inteiro positivo and Inteiro positivo Numero Real e' maior que 1 Numero Real e' menor ou igual a comprimento de Lista Inteiro positivoth elemento de Lista e' igual a Numero Real Inteiro positivo e' um membro de Lista Numero Real e' igual a Inteiro positivoth elemento de Lista Inteiro positivo e' um membro de Lista Numero RealMINUSONE e' igual a ( Numero Real + 1) Numero RealMINUSONE e' igual a Inteiro positivoth elemento de Lista Inteiro positivo e' igual a ( Inteiro positivo + Inteiro positivo) Inteiro positivo e' igual a comprimento de Lista Numero Real e' igual a Inteiro positivoth elemento de Lista + Inteiro positivo
No TPTP formula. May not be expressible in strict first order.	People.kif 1528-1539	beliefGroupPercentInRegion BeliefGroup, Numero Real and Area Geografica Colecao Colecao, Fisico, Fisico2, Numero Real1 and Numero Real2 Fisico e' situado em Area Geografica Fisico e' membro de BeliefGroup Fisico e' membro de Colecao memberCount Colecao and Numero Real1 Fisico2 e' situado em Area Geografica Fisico2 e' membro de Colecao memberCount Colecao and Numero Real2 Numero Real + 100 e' igual a Numero Real1 + Numero Real2
No TPTP formula. May not be expressible in strict first order.	Cars.kif 1928-1933	compressionRatio Engine and Numero Real minCylinderVolume Engine and Numero Real Unidade de Medida(s) maxCylinderVolume Engine and Unidade de MedidaAX Unidade de Medida(s) Numero Real e' igual a Numero Real + Unidade de MedidaAX
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.	People.kif 1547-1558	ethnicityPercentInRegion Grupo Etnico, Numero Real and Area Geografica Colecao Colecao, Fisico, Fisico2, Numero Real1 and Numero Real2 Fisico e' situado em Area Geografica Fisico e' membro de Grupo Etnico Fisico e' membro de Colecao memberCount Colecao and Numero Real1 Fisico2 e' situado em Area Geografica Fisico2 e' membro de Colecao memberCount Colecao and Numero Real2 Numero Real + 100 e' igual a Numero Real1 + Numero Real2
No TPTP formula. May not be expressible in strict first order.	People.kif 1566-1577	languagePercentInRegion Linguagem, Numero Real and Area Geografica Colecao Colecao, Agente Sentiente, Agente Sentiente2, Numero Real1 and Numero Real2 Agente Sentiente e' situado em Area Geografica Agente Sentiente e' membro de Colecao speaksLanguage Agente Sentiente and Linguagem memberCount Colecao and Numero Real1 Agente Sentiente2 e' situado em Area Geografica Agente Sentiente2 e' membro de Colecao memberCount Colecao and Numero Real2 Numero Real + 100 e' igual a Numero Real1 + Numero Real2
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13326-13331	A medida de Fisico e' Numero Real OunceMass(s) a medida de Fisico e' Numero Real + 16.0 PoundMass(s)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5104-5115	Numero Inteiro mod Numero Inteiro e' igual a Numero Inteiro Numero Inteiro e' igual a 0 (o maior numero inteiro menor or igual a Numero Inteiro + Numero Inteiro + Numero Inteiro + Numero Inteiro) e' igual a Numero Inteiro
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3277-3284	Numero Real e' igual a AverageFn Lista comprimento de Lista e' maior que 0 Numero Real e' igual a ListSumFn Lista + comprimento de Lista
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1475-1484	Numero Real e' igual a VarianceFn Lista Numero Real e' igual a AverageFn Lista Numero Real e' igual a VarianceAverageFn Numero Real and Lista + comprimento de Lista
No TPTP formula. May not be expressible in strict first order.	Cars.kif 4081-4113	Objeto e' uma instancia de BimetalTemperatureSensor Objeto e' uma instancia de Metal Objeto e' uma instancia de Metal Objeto e' igual a Objeto Objeto e' uma &parte de Objeto Objeto e' uma &parte de Objeto Entidade e' uma instancia de Medida de Temperatura Entidade e' uma instancia de Medida de Temperatura Numero Real e' uma instancia de Medida de Comprimento Numero Real e' uma instancia de Medida de Comprimento Numero Real e' uma instancia de Medida de Comprimento Numero Real e' uma instancia de Medida de Comprimento Entidade e' igual a Entidade Posicao Temporal e' igual a Posicao Temporal a medida de Objeto e' Entidade a medida de Objeto e' Numero Real a medida de Objeto e' Numero Real vale durante Posicao Temporal a medida de Objeto e' Entidade a medida de Objeto e' Numero Real a medida de Objeto e' Numero Real vale durante Posicao Temporal Numero Real + Numero Real e' igual a Numero Real + Numero Real
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 2845-2870	Colecao e' uma instancia de Colecao Fisico Fisico e' membro de Colecao Fisico e' uma instancia de WebListing o numero de instancias dentro de Entidade Entidade and Entidade a classe descrita por Entidade + o numero de instancias dentro de Colecao e' igual a BidCountFn Colecao
No TPTP formula. May not be expressible in strict first order.	Cars.kif 1314-1348	Entidade e' uma instancia de EngineChoke DeviceOn e' um atributo de Entidade vale durante Processo DeviceOff e' um atributo de Entidade vale durante Processo Objeto auto-conectado e' uma instancia de EngineCylinder capacity Objeto auto-conectado and Quantidade Constante Processo e' uma instancia de FourStrokeCompression Processo e' uma instancia de FourStrokeCompression eventLocated Processo and Objeto auto-conectado eventLocated Processo and Objeto auto-conectado Objeto e' uma instancia de Air Objeto e' uma instancia de Fuel Objeto e' uma &parte de Quantidade ConstanteIX1 Objeto e' uma &parte de Quantidade ConstanteIX1 a medida de Quantidade ConstanteIX1 e' Quantidade Constante Objeto e' uma instancia de Air Objeto e' uma instancia de Fuel Objeto e' uma &parte de Quantidade ConstanteIX2 Objeto e' uma &parte de Quantidade ConstanteIX2 a medida de Quantidade ConstanteIX2 e' Quantidade Constante Unidade de Medida e' uma instancia de Unidade de Medida a medida de Objeto e' ObjetoM Unidade de Medida(s) a medida de Objeto e' ObjetoM Unidade de Medida(s) a medida de Objeto e' ObjetoM Unidade de Medida(s) a medida de Objeto e' ObjetoM Unidade de Medida(s) ObjetoM + ObjetoM e' maior que ObjetoM + ObjetoM
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3095-3114	Experimenting e' uma instancia de Experimenting Intervalo Temporal e' uma instancia de Intervalo Temporal o numero de instancias dentro de a classe descrita por Sequencia Simbolica + o numero de instancias dentro de a classe descrita por Sequencia Simbolica e' igual a PPIFn Experimenting and Intervalo Temporal
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3056-3073	Experimenting e' uma instancia de Experimenting Entidade e' uma instancia de Intervalo Temporal o numero de instancias dentro de a classe descrita por Sequencia Simbolica + o numero de instancias dentro de a classe descrita por Sequencia Simbolica e' igual a PPSFn Experimenting
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 5915-5924	Humano e' uma instancia de HumanAdult a medida de Humano e' Numero Real Pounds(s) bloodVolume Humano and Numero Real2 Liter(s) Numero Real2 e' igual a Numero Real + 0.07 + 2.33
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 3721-3739	SearchResultsPage e' uma instancia de SearchResultsPage Lista e' uma instancia de SRPResults Lista e' um componente de SearchResultsPage o numero de instancias dentro de a classe descrita por Sequencia Simbolica + comprimento de Lista e' igual a SRPEngagementFn SearchResultsPage
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 4563-4571	Numero Real e' uma instancia de Quantidade Numero Real e' uma instancia de Quantidade LiftFn Numero Real and Numero Real e' igual a ( Numero Real + Numero Real) + Numero Real
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 1570-1577	Irradiar e' uma instancia de RadiatingElectromagnetic carrierFrequency Irradiar and Numero Real Hertz(s) wavelength Irradiar and Numero Real Meter(s) Numero Real Meter(s) e' igual a 299792458 + Numero Real Meter(s)

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.	Merge.kif 7367-7369	Numero Real AngularDegree(s) e' igual a Numero Real + Pi + 180.0 Radian(s)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7012-7014	Numero Real CelsiusDegree(s) e' igual a ( Numero Real + 32.0) + 1.8 FahrenheitDegree(s)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7239-7241	Numero Real Cup(s) e' igual a Numero Real + 2 Pint(s)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7248-7250	Numero Real Ounce(s) e' igual a Numero Real + 8 Cup(s)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7230-7232	Numero Real Pint(s) e' igual a Numero Real + 2 Quart(s)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 7221-7223	Numero Real Quart(s) e' igual a Numero Real + 4 UnitedStatesGallon(s)
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13333-13336	Numero Real Numero Real OunceMass(s) e' igual a Numero Real + 16.0 PoundMass(s)

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

KB Term:			Term intersection

English Word: