TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1729-1730
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1839-1840
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 337-338
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1836-1836	Le nombre 1 argument de lessThan est une instance de nombre r�el
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1837-1837	Le nombre 2 argument de lessThan est une instance de nombre r�el
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1831-1831	lessThan est une instance de pr�dicat binaire
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1833-1833	lessThan est une instance de relation irr�flexive
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1834-1834	lessThan est une instance de relation �tendue aux quantit�es
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1832-1832	lessThan est une instance de relation transitive
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1835-1835	lessThan est trichotomiz� en nombre r�el

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 141-141
No TPTP formula. May not be expressible in strict first order.	english_format.kif 142-142
No TPTP formula. May not be expressible in strict first order.	french_format.kif 92-92
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 163-163
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 1919-1919
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 44-44
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 76-76
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 172-172
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 202-202
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 111-111
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 91-91
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 325-325
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1850-1850	greaterThan est l' inverse de lessThan
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 142-142
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 34144-34144
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 34143-34143
No TPTP formula. May not be expressible in strict first order.	terms-de.txt 52-52
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 326-326

antecedent

No TPTP formula. May not be expressible in strict first order.	Geography.kif 7524-7530	Objet en une partie est une instance de LiquidDrop approximateDiameter objet en une partie and nombre r�el Micrometer(s) 500.0 est moins que nombre r�el objet en une partie est une instance de Droplet
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3051-3062	FinancialInstrument FinancialInstrumentPrice and nombre r�el Agreement est une instance de CallOption underlier Agreement and FinancialInstrument price FinancialInstrument, FinancialInstrumentPrice unit� de mesure(s) and AutonomousAgent unit� de mesure est une instance de UnitOfCurrency strikePrice Agreement and nombre r�el unit� de mesure(s) FinancialInstrumentPrice est moins que nombre r�el outOfTheMoney Agreement and AutonomousAgent
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3002-3013	FinancialInstrument FinancialInstrumentPrice and nombre r�el Agreement est une instance de CallOption underlier Agreement and FinancialInstrument price FinancialInstrument, FinancialInstrumentPrice unit� de mesure(s) and AutonomousAgent unit� de mesure est une instance de UnitOfCurrency strikePrice Agreement and nombre r�el unit� de mesure(s) nombre r�el est moins que FinancialInstrumentPrice inTheMoney Agreement and AutonomousAgent
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3015-3026	FinancialInstrument FinancialInstrumentPrice and nombre r�el Agreement est une instance de PutOption underlier Agreement and FinancialInstrument price FinancialInstrument, FinancialInstrumentPrice unit� de mesure(s) and AutonomousAgent unit� de mesure est une instance de UnitOfCurrency strikePrice Agreement and nombre r�el unit� de mesure(s) FinancialInstrumentPrice est moins que nombre r�el inTheMoney Agreement and AutonomousAgent
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3064-3075	FinancialInstrument FinancialInstrumentPrice and nombre r�el Agreement est une instance de PutOption underlier Agreement and FinancialInstrument price FinancialInstrument, FinancialInstrumentPrice unit� de mesure(s) and AutonomousAgent unit� de mesure est une instance de UnitOfCurrency strikePrice Agreement and nombre r�el unit� de mesure(s) nombre r�el est moins que FinancialInstrumentPrice outOfTheMoney Agreement and AutonomousAgent
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 367-385	breathingRate AutonomousAgent, interval temporel and nombre entier interval temporel est une instance de minute nombre entier nombre entier est une instance de r�cr�ation ou exercice nombre entier est un agent de AutonomousAgent interval temporel prend place pendant temps d'existence de nombre entier HumanAdult est un attribut de AutonomousAgent pendant interval temporel nombre entier est plus grand que 16 nombre entier est moins que 12 Healthy est un attribut de AutonomousAgent pendant interval temporel
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 783-788	currentAccountBalance FinancialAccount, jour and nombre r�el UnitedStatesDollar(s) nombre r�el est moins que 0 nombre r�el est nombre r�el) overdraft FinancialAccount, nombre r�el UnitedStatesDollar(s) and jour
No TPTP formula. May not be expressible in strict first order.	Media.kif 3068-3089	Cha�ne sympbolique est ReverseFn cha�ne sympbolique nombre entier non n�gatif est StringLengthFn cha�ne sympbolique nombre entier non n�gatif est plus grand que 1 nombre entier non n�gatif est plus grand que 0 nombre entier non n�gatif est moins que nombre entier non n�gatif nombre entier est plafond de ( nombre entier non n�gatif + 1) + 2 nombre entier non n�gatifEW est nombre entier + nombre entier non n�gatif) + nombre entier) cha�ne sympbolique est SubstringFn cha�ne sympbolique, nombre entier non n�gatif and (1 + nombre entier non n�gatif) cha�ne sympbolique est SubstringFn cha�ne sympbolique, nombre entier non n�gatifEW and (1 + nombre entier non n�gatifEW)
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 701-714	FinancialAccount est une instance de FinancialAccount minimumBalance FinancialAccount, UsingAnAccount and nombre r�el unit� de mesure(s) unit� de mesure est une instance de UnitOfCurrency currentAccountBalance FinancialAccount, jour and nombre r�el unit� de mesure(s) nombre r�el est moins que nombre r�el processus processus est une instance de Penalty la date de processus est jour processus aboutit � CurrencyFn FinancialAccount
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 759-775	LiabilityAccount est une instance de LiabilityAccount minimumPayment LiabilityAccount, nombre r�el unit� de mesure(s) and MonthDuration unit� de mesure est une instance de UnitOfCurrency processus interval temporel interval temporel est une instance de mois processus aboutit � CurrencyFn LiabilityAccount paymentsPerPeriod LiabilityAccount, nombre r�el unit� de mesure(s) and interval temporel nombre r�el est moins que nombre r�el processus processus est une instance de Penalty processus aboutit � CurrencyFn LiabilityAccount
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 342-348	Entit� est une instance de humain l' entit� est nombre r�el YearDuration(s) pendant position temporel nombre r�el est plus grand que 12 nombre r�el est moins que 20 entit� est une instance de Teenager pendant position temporel
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 269-274	Entit� est une instance de humain l' entit� est nombre r�el YearDuration(s) pendant position temporel nombre r�el est moins que 18 entit� est une instance de HumanYouth pendant position temporel
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13885-13900	Entit� est une instance de substance pure boilingPoint substance pure and nombre r�el unit� de mesure(s) meltingPoint substance pure and nombre r�el unit� de mesure(s) unit� de mesure est une instance de UnitOfTemperature la mesure de entit� est nombre r�el unit� de mesure(s) pendant interval temporel nombre r�el est plus grand que nombre r�el nombre r�el est moins que nombre r�el Liquid est un attribut de entit� pendant interval temporel processus interval temporel recouvre temps d'existence de processus processus est une instance de mettre en fusion entit� est un patient de processus
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13902-13915	Entit� est une instance de substance pure meltingPoint substance pure and nombre r�el unit� de mesure(s) la mesure de entit� est nombre r�el unit� de mesure(s) pendant interval temporel unit� de mesure est une instance de UnitOfTemperature nombre r�el est moins que nombre r�el Solid est un attribut de entit� pendant interval temporel processus interval temporel recouvre temps d'existence de processus processus est une instance de congeler entit� est un patient de processus
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 2667-2673	Plan d'eau est une instance de Waterway depth physique, plan d'eau and nombre r�el unit� de mesure(s) unit� de mesure est une instance de UnitOfLength nombre r�el est moins que nombre r�el navigableForDraft plan d'eau and nombre r�el unit� de mesure(s)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13831-13840	Objet est une instance de substance pure substance pure est une sous-classe de substance pure boilingPoint substance pure and nombre r�el KelvinDegree(s) meltingPoint substance pure and nombre r�el KelvinDegree(s) la mesure de objet est nombre r�el KelvinDegree(s) nombre r�el est plus grand que nombre r�el nombre r�el est moins que nombre r�el Liquid est un attribut de objet
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13842-13851	Objet est une instance de substance pure substance pure est une sous-classe de substance pure meltingPoint substance pure and nombre r�el KelvinDegree(s) barometricPressure objet and nombre r�el InchMercury(s) nombre r�el est plus grand que 29.92 la mesure de objet est nombre r�el KelvinDegree(s) nombre r�el est moins que nombre r�el Solid est un attribut de objet
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 694-710	processList @ROW physique est un membre de (@ROW) physique est un membre de (@ROW) entit� physique entit� physique nombre entier positif est moins que nombre entier positif temps d'existence de physique arrive plus t�t que temps d'existence de physique
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 430-445	productPrice entit�, nombre r�el unit� de mesure(s) and agent cognitif unit� de mesure est une instance de UnitOfCurrency publishedPrice entit�, nombre r�el unit� de mesure(s), agent cognitif and PricingScheme validFor PricingScheme and AutonomousAgent entit� est une instance de entit� processus est une instance de acheter AutonomousAgent est une instance imm�diate de AutonomousAgent processus est un agent de AutonomousAgent processus a pour origine agent cognitif nombre r�el est moins que nombre r�el l'argument transactionAmount processus and nombre r�el a la force modale de Likely
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 5968-5982	typicalBloodVolume mammif�re and nombre r�el unit� de mesure(s) bloodVolume entit� and nombre r�el2 unit� de mesure(s) pendant position temporel entit� est une instance de mammif�re nombre r�el2 + 2.0 est plus grand que nombre r�el nombre r�el2 est moins que 0.8 + nombre r�el SevereBloodLoss est un attribut de entit� pendant position temporel
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 5950-5962	typicalBloodVolume mammif�re and nombre r�el unit� de mesure(s) bloodVolume entit� and nombre r�el2 unit� de mesure(s) pendant position temporel entit� est une instance de mammif�re nombre r�el2 + 2.0 est moins que nombre r�el CatastrophicBloodLoss est un attribut de entit� pendant position temporel
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3682-3695	minDeviceOperatingTemp entit� and entit� entit�(s) entit� est une instance de UnitOfTemperature entit� est situ� � entit� DeviceOn est un attribut de entit� airTemperature entit� and entit� entit�(s) entit� est moins que entit� pendant position temporel l'argument DeviceDamaged est un attribut de entit� pendant immediatement apr�s position temporel a la force modale de Likely
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3708-3721	minDeviceStorageTemp entit� and entit� entit�(s) entit� est une instance de UnitOfTemperature entit� est situ� � entit� DeviceOff est un attribut de entit� airTemperature entit� and entit� entit�(s) entit� est moins que entit� pendant position temporel l'argument DeviceDamaged est un attribut de entit� pendant immediatement apr�s position temporel a la force modale de Likely
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 1240-1246	oxygenSaturation entit� and entit� entit� est moins que 92.0 pendant position temporel Hypoxia est un attribut de entit� pendant position temporel

consequent

No TPTP formula. May not be expressible in strict first order.	People.kif 238-264	Ann�e est une instance de l' ann�e nombre entier DeathsPerThousandLiveBirthsFn secteur g�opolitique and ann�e est nombre r�el nombre entier est instances dans la classe d�crite par cha�ne sympbolique nombre entier + 1000 est nombre r�el nombre entier est instances dans la classe d�crite par cha�ne sympbolique nombre entier + nombre r�el est nombre r�el
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1948-1952	Nombre r�el est une instance de nombre r�el n�gatif nombre r�el est moins que 0 nombre r�el est une instance de nombre r�el
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1867-1871	Nombre r�el est plus petit ou �gal � nombre r�el nombre r�el est nombre r�el nombre r�el est moins que nombre r�el
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 172-187	Anemia est un attribut de objet objet est une instance de sang objet est une partie de objet Female est un attribut de objet la mesure de objet est 0.1 Liter(s) objetE est une instance de Hemoglobin objetE est une partie de objet objetE2 est une instance de Hemoglobin objetE est objetE2 objet2 est une partie de objet la mesure de objetE est nombre r�el Gram(s) nombre r�el est moins que 12
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 155-170	Anemia est un attribut de objet objet est une instance de sang objet est une partie de objet Male est un attribut de objet la mesure de objet est 0.1 Liter(s) objetE est une instance de Hemoglobin objetE est une partie de objet objetE2 est une instance de Hemoglobin objetE est objetE2 objet2 est une partie de objet la mesure de objetE est nombre r�el Gram(s) nombre r�el est moins que 13
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18727-18736	CollegeFreshman est un attribut de position humain occupe la position de position organisation nombre r�el student humain and organisation pendant nombre r�el YearDuration(s) nombre r�el est moins que 1
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18742-18752	CollegeJunior est un attribut de position humain occupe la position de position organisation nombre r�el student humain and organisation pendant nombre r�el YearDuration(s) nombre r�el est plus grand ou �gal � 2 nombre r�el est moins que 3
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18758-18768	CollegeSenior est un attribut de position humain occupe la position de position organisation nombre r�el student humain and organisation pendant nombre r�el YearDuration(s) nombre r�el est plus grand ou �gal � 3 nombre r�el est moins que 4
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 18774-18784	CollegeSophomore est un attribut de position humain occupe la position de position organisation nombre r�el student humain and organisation pendant nombre r�el YearDuration(s) nombre r�el est plus grand ou �gal � 1 nombre r�el est moins que 2
No TPTP formula. May not be expressible in strict first order.	Dining.kif 1148-1156	La probabilit� de ComfortFood est un attribut de entit� pourvu que HeartHealthyFood est un attribut de entit� vaut nombre r�el la probabilit� de ComfortFood est un attribut de entit� pourvu que HeartHealthyFood est un attribut de entit� vaut nombre r�el nombre r�el est moins que nombre r�el
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2623-2628	Formule diminue la probabilit� de formule le probabilit� de formule est nombre r�el la probabilit� de formule pourvu que formule vaut nombre r�el nombre r�el est moins que nombre r�el
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13576-13585	defaultMeasure objet and nombre r�el unit� de mesure(s) unit� de mesure est une instance de CompositeUnitOfMeasure l'argument entit� nombre r�elUANTITY entit� est une instance de objet la mesure de entit� est nombre r�elUANTITY unit� de mesure(s) nombre r�elUANTITY est moins que nombre r�el + .5 a la force modale de Unlikely
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13504-13513	defaultMinimumMeasure objet and nombre r�el unit� de mesure(s) unit� de mesure est une instance de CompositeUnitOfMeasure l'argument entit� nombre r�elUANTITY entit� est une instance de objet la mesure de entit� est nombre r�elUANTITY unit� de mesure(s) nombre r�elUANTITY est moins que nombre r�el a la force modale de Unlikely
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13515-13526	defaultMinimumMeasure objet and nombre r�el unit� de mesure(s) classe est une sous-classe de NonCompositeUnitOfMeasure unit� de mesure est une instance de classe l'argument entit� nombre r�elUANTITY and entit� entit� est une instance de objet la mesure de entit� est nombre r�elUANTITY entit�(s) entit� est une instance de classe nombre r�elUANTITY est moins que nombre r�el a la force modale de Unlikely
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13466-13476	defaultMinimumSphereRadius objet and nombre r�el unit� de mesure(s) objet est une instance de objet Sphere est un attribut de objet l'argument nombre r�elADIUS sphereRadius objet and nombre r�elADIUS unit� de mesure(s) nombre r�elADIUS est moins que nombre r�el a la force modale de Unlikely
No TPTP formula. May not be expressible in strict first order.	Merge.kif 4958-4972	La racine carr�e de nombre entier de @ROW est nombre entier nombre entier est nombre entier nombre entier est moins que nombre entier nombre entier nombre entier est un membre de (@ROW) nombre entier reste nombre entier est &%�gal � 0
No TPTP formula. May not be expressible in strict first order.	Dining.kif 772-795	AutonomousAgent est une instance de AutonomousAgent potentialCustomer agent cognitif and AutonomousAgent l'argument entit� est une instance de Reserving entit� aboutit � AutonomousAgent a la force modale de Necessity la probabilit� de entit�ES1 entit�ES1 est une instance de Reservation reservingEntity agent cognitif and entit�ES1 fulfillingEntity AutonomousAgent and entit�ES1 pourvu que customer agent cognitif and AutonomousAgent vaut nombre r�el la probabilit� de entit�ES2 entit�ES2 est une instance de Reservation reservingEntity agent cognitif and entit�ES2 fulfillingEntity AutonomousAgent and entit�ES2 pourvu que customer agent cognitif and AutonomousAgent vaut nombre r�el nombre r�el est moins que nombre r�el
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 1391-1400	Objet est une instance de Airport VeryShortRunwayAirport est un attribut de objet objet nombre r�el objet est une instance de Runway objet est une partie de objet le longueur de objet est nombre r�el Meter(s) nombre r�el est moins que 914
No TPTP formula. May not be expressible in strict first order.	Geography.kif 1940-1954	Secteur g�ographique est une instance de secteur g�ographique geographicSubregion ElevationLowPointFn secteur g�ographique and secteur g�ographique unit� de mesure est une instance de UnitOfLength elevation ElevationLowPointFn secteur g�ographique and nombre r�el unit� de mesure(s) secteur g�ographique nombre r�el geographicSubregion secteur g�ographique and secteur g�ographique secteur g�ographique est ElevationLowPointFn secteur g�ographique elevation secteur g�ographique and nombre r�el unit� de mesure(s) nombre r�el est moins que nombre r�el
No TPTP formula. May not be expressible in strict first order.	Weather.kif 888-894	R�gion est une instance de secteur g�ographique processus est une instance de ClearWeather eventLocated processus and r�gion cloudCoverFraction r�gion and nombre r�el non n�gatif nombre r�el non n�gatif est moins que 0.3
No TPTP formula. May not be expressible in strict first order.	Weather.kif 878-886	R�gion est une instance de secteur g�ographique processus est une instance de ClearWeather eventLocated processus and r�gion nombre r�el non n�gatif cloudCoverFraction r�gion and nombre r�el non n�gatif nombre r�el non n�gatif est moins que 0.3
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 4698-4708	Objet en une partie est une instance de Bottle l' arri�re de objet en une partie est objet en une partie le dessus de objet en une partie est objet en une partie unit� de mesure est une instance de UnitOfLength la largeur de objet en une partie est nombre r�el unit� de mesure(s) la largeur de objet en une partie est nombre r�el unit� de mesure(s) nombre r�el est moins que nombre r�el
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10983-10996	Processus est une instance de refroidir entit� est un patient de processus entit� nombre r�el and nombre r�el entit� est une instance de mesure de temperature entit� entit�(s) est nombre r�el pendant le d�but de temps d'existence de processus entit� entit�(s) est nombre r�el pendant la fin de temps d'existence de processus nombre r�el est moins que nombre r�el
No TPTP formula. May not be expressible in strict first order.	Medicine.kif 620-630	Processus est une instance de CPR d�palcement est une instance de Compressing objet est le chemin le long duquel d�palcement se produit d�palcement est un sous-processus de processus le longueur de objet est nombre r�el Centimeter(s) nombre r�el est plus grand que 5.0 nombre r�el est moins que 6.0
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 1926-1940	ComputerProcess est une instance de DataCompression dataProcessed ComputerProcess and DigitalData memorySize DigitalData and nombre r�el entit�(s) pendant immediatement avant temps d'existence de ComputerProcess memorySize DigitalData and nombre r�el entit�(s) pendant immediatement apr�s temps d'existence de ComputerProcess nombre r�el est moins que nombre r�el

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 6099-6106

Chemin du graph chemin du graph chemin du graph est une instance de l' ensemble de chemins qui partitionnent graph en deux graph s�par� chemin du graph est une instance de l' ensemble minimal de chemins qui partitionnent graph en deux graph s�par� la longueur de chemin du graph est nombre entier positif la longueur de chemin du graph est nombre entier positif nombre entier positif est moins que nombre entier positif

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

KB Term:			Term intersection

English Word: