An Entity of Type: Rule105846054, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

In predicate logic, existential instantiation (also called existential elimination) is a rule of inference which says that, given a formula of the form , one may infer for a new constant symbol c. The rule has the restrictions that the constant c introduced by the rule must be a new term that has not occurred earlier in the proof, and it also must not occur in the conclusion of the proof. It is also necessary that every instance of which is bound to must be uniformly replaced by c. This is implied by the notation , but its explicit statement is often left out of explanations.

Property Value
dbo:abstract
  • En lógica de predicados, la ejemplificación existencial (también llamada eliminación existencial)​​​ es una regla de inferencia válida que dice que, dada una fórmula de la forma , es posible inferir para una nueva constante o variable simbólica c. La regla tiene la restricción de que los constantes o variables c introducidas por la regla deben ser nuevo término que no ha ocurrido antes en la prueba. En una notación formal, la regla puede ser denotada donde a es un término arbitrario que no ha sido parte de nuestra prueba hasta el momento. (es)
  • In predicate logic, existential instantiation (also called existential elimination) is a rule of inference which says that, given a formula of the form , one may infer for a new constant symbol c. The rule has the restrictions that the constant c introduced by the rule must be a new term that has not occurred earlier in the proof, and it also must not occur in the conclusion of the proof. It is also necessary that every instance of which is bound to must be uniformly replaced by c. This is implied by the notation , but its explicit statement is often left out of explanations. In one formal notation, the rule may be denoted by where a is a new constant symbol that has not appeared in the proof. (en)
  • 存在例化(そんざいれいか、英: Existential instantiation, Existential elimination)は、述語論理において、という形式を持った式が与えられると、新しい定数記号cについてを推論することができるという、妥当な推論規則のひとつである。この規則は、導入された定数cが、証明にはこれまで用いられてこなかった新しい項でなければならないという制約を有する。 例えば、形式的な記法においては、規則は次のように表記される。 ここでaは、その時点まで証明に現れていない新しい定数記号である。 (ja)
  • In de predicatenlogica is existentiële instantiatie (EI) een afleidingsregel die uit een propositie over een bepaald object uit het een propositie afleidt over een specifiek object in dat domein. Deze propositie maakt gebruik van de existentiekwantor. Formeel verloopt existentiële instantiatie als volgt: waarbij c0 een nieuwe, nog niet eerder gebruikte constante is. Deze redenatie is geldig aangezien we alleen een naam geven aan een bestaande x. Een voorbeeld (met , de natuurlijke getallen als domein): "Er is een getal dat deelbaar is door 2. c is deelbaar door 2.". De constante c is één specifiek getal uit het domein dat deelbaar is door 2. Bij het kiezen van een constante moet een nieuwe constante gekozen worden aangezien het predicaat niet hoeft te gelden voor eerder gebruikte (bekende) constanten. Een nieuw gekozen constante wordt ook wel een Skolem constante genoemd, vernoemd naar de Noorse wiskundige Albert Thoralf Skolem. Wanneer men een eerder gebruikte constante invult, is het mogelijk ongeldige proposities af te leiden: stel, men ontdekt een getal x waarvoor geldt: . dan is het mogelijk deze een nieuwe naam te geven, zoals e, maar het zou onjuist zijn om een al bestaande constante, zoals π, te gebruiken. Als er voor de existentiekwantor nog universele kwantoren staan, dan dient men een functie in te vullen met de variabelen van die kwantor(en) aangezien het ingevulde object uit het domein afhangt van de objecten die ingevuld zijn bij de variabelen van de universele kwantor(en). Zo'n functie wordt een Skolem functie genoemd. (nl)
  • Na lógica de predicados, instanciação existencial (também chamada como eliminação existencial) é uma regra de inferência válida, onde dada um fórmula da forma , pode-se inferir como um novo símbolo de constante ou variável denotada por c. A regra tem a restrição de que a constante ou variável c que forem introduzidas pela regra, devem ser um novo termo que não ocorreu no início da prova. A regra denotada em notação formal: onde 'a' é um termo arbitrário que não tem sido parte da prova até agora. (pt)
dbo:wikiPageID
  • 34632680 (xsd:integer)
dbo:wikiPageLength
  • 1549 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1092223076 (xsd:integer)
dbo:wikiPageWikiLink
dbp:field
dbp:name
  • Existential instantiation (en)
dbp:type
dbp:wikiPageUsesTemplate
dcterms:subject
rdf:type
rdfs:comment
  • En lógica de predicados, la ejemplificación existencial (también llamada eliminación existencial)​​​ es una regla de inferencia válida que dice que, dada una fórmula de la forma , es posible inferir para una nueva constante o variable simbólica c. La regla tiene la restricción de que los constantes o variables c introducidas por la regla deben ser nuevo término que no ha ocurrido antes en la prueba. En una notación formal, la regla puede ser denotada donde a es un término arbitrario que no ha sido parte de nuestra prueba hasta el momento. (es)
  • 存在例化(そんざいれいか、英: Existential instantiation, Existential elimination)は、述語論理において、という形式を持った式が与えられると、新しい定数記号cについてを推論することができるという、妥当な推論規則のひとつである。この規則は、導入された定数cが、証明にはこれまで用いられてこなかった新しい項でなければならないという制約を有する。 例えば、形式的な記法においては、規則は次のように表記される。 ここでaは、その時点まで証明に現れていない新しい定数記号である。 (ja)
  • Na lógica de predicados, instanciação existencial (também chamada como eliminação existencial) é uma regra de inferência válida, onde dada um fórmula da forma , pode-se inferir como um novo símbolo de constante ou variável denotada por c. A regra tem a restrição de que a constante ou variável c que forem introduzidas pela regra, devem ser um novo termo que não ocorreu no início da prova. A regra denotada em notação formal: onde 'a' é um termo arbitrário que não tem sido parte da prova até agora. (pt)
  • In predicate logic, existential instantiation (also called existential elimination) is a rule of inference which says that, given a formula of the form , one may infer for a new constant symbol c. The rule has the restrictions that the constant c introduced by the rule must be a new term that has not occurred earlier in the proof, and it also must not occur in the conclusion of the proof. It is also necessary that every instance of which is bound to must be uniformly replaced by c. This is implied by the notation , but its explicit statement is often left out of explanations. (en)
  • In de predicatenlogica is existentiële instantiatie (EI) een afleidingsregel die uit een propositie over een bepaald object uit het een propositie afleidt over een specifiek object in dat domein. Deze propositie maakt gebruik van de existentiekwantor. Formeel verloopt existentiële instantiatie als volgt: . dan is het mogelijk deze een nieuwe naam te geven, zoals e, maar het zou onjuist zijn om een al bestaande constante, zoals π, te gebruiken. (nl)
rdfs:label
  • Existential instantiation (en)
  • Instanciación existencial (es)
  • 存在例化 (ja)
  • Existentiële instantiatie (nl)
  • Instanciação existencial (pt)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License