This HTML5 document contains 37 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
n6https://global.dbpedia.org/id/
dbthttp://dbpedia.org/resource/Template:
rdfshttp://www.w3.org/2000/01/rdf-schema#
freebasehttp://rdf.freebase.com/ns/
dbpedia-pthttp://pt.dbpedia.org/resource/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
wikipedia-enhttp://en.wikipedia.org/wiki/
provhttp://www.w3.org/ns/prov#
dbchttp://dbpedia.org/resource/Category:
dbphttp://dbpedia.org/property/
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/
dbpedia-jahttp://ja.dbpedia.org/resource/

Statements

Subject Item
dbr:Herbrandization
rdfs:label
Herbrandization Herbrandização エルブラン化
rdfs:comment
論理式のエルブラン化（英: Herbrandization）とは、論理式のスコーレム化の双対となる構成である。ジャック・エルブランに因む。トアルフ・スコーレムは、レーヴェンハイム–スコーレムの定理（Skolem 1920）の証明の一部として、冠頭標準形の論理式のスコーレム化を考えていた。エルブランは、エルブランの定理（Herbrand 1930）を証明するため、その双対概念であるエルブラン化（冠頭標準形以外の論理式にも適用できるよう一般化されたもの）を用いた。 結果の論理式は元々の論理式と論理的同値である必要はない。充足可能性を保つスコーレム化と同様、スコーレム化の双対であるエルブラン化は論理的妥当性を保つ：結果の論理式が妥当であるのは、元々の論理式が妥当であるとき、かつそのときに限る。 A Herbrandização de uma fórmula lógica (denominação em homenagem a Jacques Herbrand) é um construção que é dual à Skolemização de uma fórmula. Thoralf Skolem tinha considerado a Skolemização de fórmulas na Forma normal prenex como parte da prova do Teorema de Löwenheim–Skolem (Skolem 1920). Herbrand trabalhou com essa noção dual de Herbrandização, generalizada para se aplicar a fórmulas não-prenex também, com o objetivo de provar o Teorema de Herbrand (Herbrand 1930). A Herbrandização de é obtida da seguinte maneira: The Herbrandization of a logical formula (named after Jacques Herbrand) is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim–Skolem theorem (Skolem 1920). Herbrand worked with this dual notion of Herbrandization, generalized to apply to non-prenex formulas as well, in order to prove Herbrand's theorem (Herbrand 1930).
dcterms:subject
dbc:Normal_forms_(logic) dbc:Logic
dbo:wikiPageID
5821699
dbo:wikiPageRevisionID
1070544322
dbo:wikiPageWikiLink
dbr:First-order_logic dbr:Jacques_Herbrand dbr:Jean_van_Heijenoort dbr:Validity_(logic) dbr:Duality_(mathematics) dbr:Löwenheim–Skolem_theorem dbc:Logic dbr:Satisfiability dbr:Skolemization dbr:Predicate_functor_logic dbc:Normal_forms_(logic) dbr:Thoralf_Skolem dbr:Herbrand's_theorem_(proof_theory) dbr:Logical_equivalence dbr:Prenex_form
owl:sameAs
dbpedia-ja:エルブラン化 n6:4mhb8 wikidata:Q5736209 dbpedia-pt:Herbrandização freebase:m.0f7898
dbp:wikiPageUsesTemplate
dbt:Short_description
dbo:abstract
The Herbrandization of a logical formula (named after Jacques Herbrand) is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim–Skolem theorem (Skolem 1920). Herbrand worked with this dual notion of Herbrandization, generalized to apply to non-prenex formulas as well, in order to prove Herbrand's theorem (Herbrand 1930). The resulting formula is not necessarily equivalent to the original one. As with Skolemization, which only preserves satisfiability, Herbrandization being Skolemization's dual preserves validity: the resulting formula is valid if and only if the original one is. A Herbrandização de uma fórmula lógica (denominação em homenagem a Jacques Herbrand) é um construção que é dual à Skolemização de uma fórmula. Thoralf Skolem tinha considerado a Skolemização de fórmulas na Forma normal prenex como parte da prova do Teorema de Löwenheim–Skolem (Skolem 1920). Herbrand trabalhou com essa noção dual de Herbrandização, generalizada para se aplicar a fórmulas não-prenex também, com o objetivo de provar o Teorema de Herbrand (Herbrand 1930). A fórmula resultante não é necessariamente equivalente à original. Assim como acontece na Skolemização, que somente preserva a satisfatibilidade, a Herbrandização sendo uma dual da Skolemização, preserva a validade: a fórmula resultante é válida se e somente se a original for. Seja uma fórmula na linguagem da Lógica de primeira ordem. Podemos assumir que não contém nenhuma variável que está ligada a duas ocorrências de quantificadores diferentes, e que nenhuma variável ocorre livre e ligada. (Ou seja, pode ser reescrita para assegurar essas condições, de modo que o resultado é uma fórmula equivalente). A Herbrandização de é obtida da seguinte maneira: * Primeiro, substitua qualquer variável livre em por símbolos de constante; * Depois, remova todos os quantificadores nas variáveis que (1) sejam quantificadas universalmente e que estejam dentro do escopo de uma quantidade par de símbolos de negação, ou (2) que sejam quantificadas existencialmente, e com estejam dentro do escopo de uma quantidade impar de símbolos de negação; * Finalmente, substitua cada variável por um símbolo de função, , onde são as variáveis que continuam quantificadas, e cujos quantificadores dominam . 論理式のエルブラン化（英: Herbrandization）とは、論理式のスコーレム化の双対となる構成である。ジャック・エルブランに因む。トアルフ・スコーレムは、レーヴェンハイム–スコーレムの定理（Skolem 1920）の証明の一部として、冠頭標準形の論理式のスコーレム化を考えていた。エルブランは、エルブランの定理（Herbrand 1930）を証明するため、その双対概念であるエルブラン化（冠頭標準形以外の論理式にも適用できるよう一般化されたもの）を用いた。 結果の論理式は元々の論理式と論理的同値である必要はない。充足可能性を保つスコーレム化と同様、スコーレム化の双対であるエルブラン化は論理的妥当性を保つ：結果の論理式が妥当であるのは、元々の論理式が妥当であるとき、かつそのときに限る。
prov:wasDerivedFrom
wikipedia-en:Herbrandization?oldid=1070544322&ns=0
dbo:wikiPageLength
3720
foaf:isPrimaryTopicOf
wikipedia-en:Herbrandization