TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 1964-1966
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2981-2984
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 596-598
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2977-2977	O argumento numero 1 de ListOrderFn e' uma instancia de Lista
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2978-2978	O argumento numero 2 de ListOrderFn e' uma instancia de Inteiro positivo
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2975-2975	ListOrderFn e' uma instancia de Funcao Binaria
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2976-2976	ListOrderFn e' uma instancia de Relacao Parcial
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2979-2979	O contra-dominio de ListOrderFn e' uma instancia de Entidade

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 263-263
No TPTP formula. May not be expressible in strict first order.	english_format.kif 268-268
No TPTP formula. May not be expressible in strict first order.	french_format.kif 150-150
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 169-169
No TPTP formula. May not be expressible in strict first order.	japanese_format.kif 1978-1978
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 102-102
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 159-159
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 338-338
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 207-207
No TPTP formula. May not be expressible in strict first order.	relations-ro.kif 169-169
No TPTP formula. May not be expressible in strict first order.	relations-sv.txt 156-156
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 337-337
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 264-264
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 34697-34697
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 34696-34696
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 34695-34695
No TPTP formula. May not be expressible in strict first order.	terms-de.txt 108-108
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 338-338

antecedent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 476-484	@ROW e' &o oposto de Atributo e' igual a Entidade elemento de (@ROW) Atributo e' igual a Entidade elemento de (@ROW) Inteiro positivo e' igual a Inteiro positivo Entidade tem um atributo de Atributo Entidade tem um atributo de Atributo
No TPTP formula. May not be expressible in strict first order.	Merge.kif 18446-18451	defaultMaxValue Predicado, Inteiro positivo and Quantidade Predicado @ARGS Entidade e' igual a Inteiro positivoth elemento de (@ARGS) o argumento Quantidade e' maior que Entidade tem a forca modal de Likely
No TPTP formula. May not be expressible in strict first order.	Merge.kif 18429-18434	defaultMinValue Predicado, Inteiro positivo and Quantidade Predicado @ARGS Entidade e' igual a Inteiro positivoth elemento de (@ARGS) o argumento Entidade e' maior que Quantidade tem a forca modal de Likely
No TPTP formula. May not be expressible in strict first order.	Merge.kif 18463-18468	defaultValue Predicado, Inteiro positivo and Quantidade Predicado @ARGS Entidade e' igual a Inteiro positivoth elemento de (@ARGS) o argumento Quantidade e' igual a Entidade tem a forca modal de Likely
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3219-3223	Comprimento de Lista e' igual a Inteiro positivo Inteiro positivoth elemento de Lista e' igual a Entidade LastFn Lista e' igual a Entidade
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1838-1845	NumberList e' igual a PhysicalQuantityToNumberFn MeasuringResultList Quantidade Fisica e' igual a Entidade elemento de MeasuringResultList Numero Real e' igual a Entidade elemento de NumberList Numero Real Unidade de Medida(s) e' igual a Quantidade Fisica
No TPTP formula. May not be expressible in strict first order.	Media.kif 2106-2113	exactCardinality Relacao, Inteiro positivo and 1 Relacao e' uma instancia de Predicado Relacao @ARGS Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade e' igual a Entidade
No TPTP formula. May not be expressible in strict first order.	Media.kif 2093-2103	exactCardinality Relacao, Inteiro positivo and 1 Relacao e' uma instancia de Predicado Relacao @ARGS Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade e' igual a Entidade
No TPTP formula. May not be expressible in strict first order.	Geography.kif 427-431	LatitudeFn Atributo Directional and @ROW e' uma instancia de Regiao 1th elemento de (@ROW) e' igual a Numero Real AngularDegree(s) Numero Real e' menor ou igual a 90.0
No TPTP formula. May not be expressible in strict first order.	Geography.kif 467-474	LongitudeFn Atributo Directional and @ROW e' uma instancia de Regiao 1th elemento de (@ROW) e' igual a Numero Real AngularDegree(s) Numero Real e' menor ou igual a 180.0
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1935-1944	Lista e' uma instancia de ConsecutiveTimeIntervalList Intervalo Temporal e' igual a Entidade elemento de Lista Intervalo Temporal e' igual a ( Inteiro positivo + 1)th elemento de Lista o comeco de Intervalo Temporal e' igual a o fim de Intervalo Temporal
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1806-1811	measuringResult MeasuringList and MeasuringResultList Processo e' igual a Entidade elemento de MeasuringList Entidade e' igual a Entidade elemento de MeasuringResultList Entidade e' o resultado de Processo
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 694-710	processList @ROW Fisico e' um membro de (@ROW) Fisico e' um membro de (@ROW) Entidade elemento de (@ROW) e' igual a Fisico Entidade elemento de (@ROW) e' igual a Fisico Inteiro positivo e' menos que Inteiro positivo tempo de existencia de Fisico acontence antes de tempo de existencia de Fisico
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 799-817	viewedItemList AutonomousAgent and Lista Processo e' uma instancia de AccessingWebPage Processo e' uma instancia de AccessingWebPage Processo e' um agente de AutonomousAgent Processo e' um agente de AutonomousAgent Inteiro positivo e' uma instancia de Inteiro positivo Inteiro positivo e' uma instancia de Inteiro positivo Inteiro positivoth elemento de Lista e' igual a Processo Inteiro positivoth elemento de Lista e' igual a Processo Inteiro positivo e' maior que Inteiro positivo tempo de existencia de Processo acontence antes de tempo de existencia de Processo

consequent

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.	Merge.kif 2998-3003	O argumento numero Inteiro positivo de Relacao e' uma instancia de Classe Relacao e' uma instancia de Predicado Relacao @ROW Inteiro positivoth elemento de (@ROW) e' uma instancia de Classe
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3005-3010	O argumento numero Inteiro positivo de Relacao e' uma sub-classe de Classe Relacao e' uma instancia de Predicado Relacao @ROW Inteiro positivoth elemento de (@ROW) e' uma sub-classe de Classe
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3252-3256	Numero Real e' igual a ListSumFn Lista 1 e' igual a comprimento de Lista Numero Real e' igual a 1th elemento de Lista
No TPTP formula. May not be expressible in strict first order.	Merge.kif 295-302	Lista e' igual a Lista Lista e' igual a (@ROW1) Lista e' igual a (@ROW2) Entidade elemento de (@ROW1) e' igual a Entidade elemento de (@ROW2)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3083-3102	Lista e' igual a a lista composta de Lista e Lista Lista e' igual a NullList Lista e' igual a NullList Inteiro positivo e' menor ou igual a comprimento de Lista Inteiro positivo e' menor ou igual a comprimento de Lista Inteiro positivo e' uma instancia de Inteiro positivo Inteiro positivo e' uma instancia de Inteiro positivo Inteiro positivoth elemento de Lista e' igual a Inteiro positivoth elemento de Lista (comprimento de Lista + Inteiro positivo)th elemento de Lista e' igual a Inteiro positivoth elemento de Lista
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3179-3188	Lista e' igual a SubListFn Inteiro positivo, Numero Inteiro and Lista ( Numero Inteiro + Inteiro positivo) e' igual a 1 Lista e' igual a ( Inteiro positivoth elemento de Lista)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3190-3202	Lista e' igual a SubListFn Inteiro positivo, Numero Inteiro and Lista ( Numero Inteiro + Inteiro positivo) e' maior que 1 Lista e' igual a a lista composta de ( Inteiro positivoth elemento de Lista) e SubListFn (1 + Inteiro positivo), Numero Inteiro and Lista
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1486-1497	Numero Real e' igual a VarianceAverageFn Numero Real and Lista 1 e' igual a comprimento de Lista Numero Real e' igual a ( Numero Real + 1th elemento de Lista) + ( Numero Real + 1th elemento de Lista)
No TPTP formula. May not be expressible in strict first order.	Weather.kif 1453-1465	Numero Real e' igual a VarianceAverageFn Numero and Lista comprimento de Lista e' maior que 1 Numero Real e' igual a (VarianceAverageFn Numero and 1th elemento de Lista + VarianceAverageFn Numero and SubListFn 2, comprimento de Lista and Lista)
No TPTP formula. May not be expressible in strict first order.	Media.kif 2093-2103	exactCardinality Relacao, Inteiro positivo and 1 Relacao e' uma instancia de Predicado Relacao @ARGS Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade e' igual a Entidade
No TPTP formula. May not be expressible in strict first order.	Media.kif 2075-2090	exactCardinality Relacao, Inteiro positivo and 1 Relacao e' uma instancia de Predicado Entidade @ARGS Relacao @ARGS Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade e' igual a Entidade
No TPTP formula. May not be expressible in strict first order.	Media.kif 2137-2150	exactCardinality Relacao, Inteiro positivo and Numero Inteiro Relacao e' uma instancia de Predicado Classe Entidade and @ARGS Classe e' uma instancia de Conjunto ou Classe Relacao @ARGS Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade e' uma instancia de Classe o numero de instancias dentro de Classe e' igual a Numero Inteiro
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3232-3237	Lista e' uma instancia de Lista Lista e' igual a NullList FirstFn Lista e' igual a 1th elemento de Lista
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 2388-2404	Processo e' uma instancia de SEO Entidade e' um patient de Processo Processo tem por fim Entidade_BEFORE Entidade_AFTER, Entidade, Entidade, Entidade and Entidade Entidade_BEFORE e' uma instancia de SRPResults Entidade_AFTER e' uma instancia de SRPResults Entidade e' igual a Entidadeth elemento de Entidade_BEFORE Entidade e' igual a Entidadeth elemento de Entidade_AFTER Entidade e' uma instancia de BestMatchAlgorithm Entidade e' uma instancia de BestMatchAlgorithm tempo de existencia de Entidade acontence antes de tempo de existencia de Entidade tempo de existencia de Processo acontence antes de tempo de existencia de Entidade tempo de existencia de Entidade acontence antes de tempo de existencia de Processo Entidade e' maior que Entidade
No TPTP formula. May not be expressible in strict first order.	Media.kif 2210-2223	maxCardinality Relacao, Inteiro positivo and Numero Inteiro Relacao e' uma instancia de Predicado Classe Entidade and @ARGS Classe e' uma instancia de Conjunto ou Classe Relacao @ARGS Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade e' uma instancia de Classe o numero de instancias dentro de Classe e' menor ou igual a Numero Inteiro
No TPTP formula. May not be expressible in strict first order.	Media.kif 2174-2187	minCardinality Relacao, Inteiro positivo and Numero Inteiro Relacao e' uma instancia de Predicado Classe Entidade and @ARGS Classe e' uma instancia de Conjunto ou Classe Relacao @ARGS Entidade e' igual a Inteiro positivoth elemento de (@ARGS) Entidade e' uma instancia de Classe o numero de instancias dentro de Classe e' maior ou igual a Numero Inteiro
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3212-3217	LastFn Lista e' igual a Entidade Inteiro positivo comprimento de Lista e' igual a Inteiro positivo Inteiro positivoth elemento de Lista e' igual a Entidade
No TPTP formula. May not be expressible in strict first order.	Media.kif 2125-2134	exactCardinality Relacao, Numero Inteiro and Numero Inteiro Sequencia Simbolica @ARGS o numero de instancias dentro de a classe descrita por Sequencia Simbolica e' igual a Numero Inteiro
No TPTP formula. May not be expressible in strict first order.	Merge.kif 519-531	exhaustiveAttribute Atributo and @ROW Entidade Entidade e' uma instancia de Atributo Entidade Inteiro positivo Entidade e' igual a Entidade Entidade e' igual a Inteiro positivoth elemento de (@ROW)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3113-3116	Entidade e' um membro de Lista Inteiro positivo Inteiro positivoth elemento de Lista e' igual a Entidade
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2910-2915	Lista e' uma instancia de Lista Unica Inteiro positivo Inteiro positivo Inteiro positivoth elemento de Lista e' igual a Inteiro positivoth elemento de Lista Inteiro positivo e' igual a Inteiro positivo
No TPTP formula. May not be expressible in strict first order.	Media.kif 2198-2207	maxCardinality Relacao, Numero Inteiro and Numero Inteiro Sequencia Simbolica @ARGS o numero de instancias dentro de a classe descrita por Sequencia Simbolica e' menor ou igual a Numero Inteiro
No TPTP formula. May not be expressible in strict first order.	Media.kif 2161-2170	minCardinality Relacao, Numero Inteiro and Numero Inteiro Sequencia Simbolica @ARGS o numero de instancias dentro de a classe descrita por Sequencia Simbolica e' maior ou igual a Numero Inteiro

statement

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

Merge.kif 3042-3046

@ROW Entidade comprimento de (@ROW + Entidade)th elemento de (@ROW + Entidade) e' igual a Entidade

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

KB Term:			Term intersection

English Word: