Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic. Although Herbrand originally proved his theorem for arbitrary formulas of first-order logic, the simpler version shown here, restricted to formulas in prenex form containing only existential quantifiers, became more popular.
| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:label
| - Satz von Herbrand (de)
- Herbrand's theorem (en)
- Théorème de Herbrand (fr)
- エルブランの定理 (ja)
- Twierdzenie Herbranda (pl)
- Teorema de Herbrand (pt)
- Теорема Ербрана (uk)
- 埃尔布朗定理 (zh)
|
| rdfs:comment
| - Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic. Although Herbrand originally proved his theorem for arbitrary formulas of first-order logic, the simpler version shown here, restricted to formulas in prenex form containing only existential quantifiers, became more popular. (en)
- エルブランの定理（英: Herbrand's theorem）は1930年にジャック・エルブランが発表した数理論理学上の基本定理である。エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。 を節の有限集合とするとき、以下の2つは同値である。
* が充足不能
* から得られる基礎例（エルブラン基底）の有限集合で充足不能なものが存在 エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自動定理証明の理論的な基盤になっている。チューリングマシンの停止性問題と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では一階述語論理を命題論理と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。 なお、エルブランの本来の証明は任意の一階述語論理式を対象としたものだが、多くの場合、冠頭形の論理式に制限し単純化した定理で表される。 (ja)
- Twierdzenie Herbranda to jedno z najważniejszych twierdzeń konstruktywnych logiki pierwszego rzędu: Formuła jest tautologią wtedy i tylko wtedy, gdy tautologią jest pewne rozwinięcie Herbranda tej formuły. Ponieważ każde rozwinięcie jest właściwie skończoną formułą rachunku zdań,a więc da się rozstrzygnąć w czasie skończonym (wykładniczym), liczba rozwinięć Herbrandadla formuły natomiast jest zbiorem przeliczalnym, umożliwia to udowodnienie każdej tautologiilogiki pierwszego rzędu, chociaż może tozająć nieograniczoną ilość czasu. (pl)
- 在逻辑学中，埃尔布朗定理(Herbrand's theorem)建立了命题逻辑计算和谓词逻辑计算之间的关系，因此埃尔布朗定理可能是一种已知的确定手段来判断一个命题的命题逻辑计算是否是有限的，对于一个含有复杂谓词的公式，它的谓词逻辑计算也起到同样的判断。通过对埃尔布朗定理的应用，部分解决回答了上述问题。但是虽然有Gödel(哥德尔)，Tarski(塔尔斯基)，Church(邱奇)，Turing(图灵)和其他科学家在逻辑学领域中卓越的研究成果，但是至今不存在一个算法，能够决定一个普遍公式的谓词逻辑计算是否是可计算的这样一个问题，我们不知道这个算法是否是可以被证明的。 (zh)
- Der Satz von Herbrand ist ein Satz der mathematischen Logik, der 1930 vom französischen Logiker Jacques Herbrand publiziert wurde. Er macht eine Aussage darüber, wann eine prädikatenlogische Formel ohne Gleichheit allgemeingültig oder erfüllbar ist und erlaubt eine Reduktion auf Allgemeingültigkeit oder Erfüllbarkeit in der Aussagenlogik. Der Satz besagt: (de)
- En logique, le théorème de Herbrand, publié en 1930 par Jacques Herbrand, établit un lien entre la logique du premier ordre et la logique propositionnelle (qui peut-être vu comme la logique d'ordre zéro). La validité (ou prouvabilité) d’une formule du premier ordre se ramène à la validité (ou prouvabilité) d'un ensemble fini de formules propositionnelles. (fr)
- Em lógica matemática, o teorema de Herbrand é um resultado básico de Jacques Herbrand (1930). Ele essencialmente permite um tipo de redução da lógica de primeira ordem para a lógica proposicional. Embora originalmente Herbrand tenha provado seu teorema para fórmulas arbitrárias da lógica de primeira ordem, a versão mais simples, mostrada aqui, que é restrita a fórmulas em forma normal prenex contendo apenas quantificadores existenciais, tornou-se mais popular. Sendo a fórmula de primeira ordem com quantificadores livres. Então é válido se, e somente se, existe uma sequência finita de termos :, com (pt)
- Теорема Ербрана — фундаментальний результат математичної логіки, отриманий Жаком Ербраном в 1930 р. Суть теореми у тому, що вона гарантує формальну виводимість (довідність) формули елементарної (першопорядкової) логіки з аксіом, якщо методом Ербрана можна показати загальзначимість цієї формули в т. зв. ербрановському універсумі, що представляє із себе суто синтаксичну (ефективно породжувану) конструкцію. При цьому в основі методу Ербрана лежать ідея непрямого доказу й ідея зведення формули логіки предикатів у скулемовській нормальній формі (можливо, з функціональними символами) до деякого окремого випадку (до пропозиційної формули в канонічній формі), який дозволив би зробити висновок про загальнозначимість вихідної формули. В результаті такої процедури переходу «від часткового до загально (uk)
|
| differentFrom
| |
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| has abstract
| - Der Satz von Herbrand ist ein Satz der mathematischen Logik, der 1930 vom französischen Logiker Jacques Herbrand publiziert wurde. Er macht eine Aussage darüber, wann eine prädikatenlogische Formel ohne Gleichheit allgemeingültig oder erfüllbar ist und erlaubt eine Reduktion auf Allgemeingültigkeit oder Erfüllbarkeit in der Aussagenlogik. Der Satz besagt: Sei eine geschlossene prädikatenlogische Formel ohne Gleichheit.Dann gibt es eine (aus berechenbare) quantorenfreie Formel , sodass gilt: ist eine Tautologie genau dann, wenn es variablenfreie Substitutionsinstanzen von gibt, sodasseine aussagenlogische Tautologie ist. (de)
- Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic. Although Herbrand originally proved his theorem for arbitrary formulas of first-order logic, the simpler version shown here, restricted to formulas in prenex form containing only existential quantifiers, became more popular. (en)
- En logique, le théorème de Herbrand, publié en 1930 par Jacques Herbrand, établit un lien entre la logique du premier ordre et la logique propositionnelle (qui peut-être vu comme la logique d'ordre zéro). La validité (ou prouvabilité) d’une formule du premier ordre se ramène à la validité (ou prouvabilité) d'un ensemble fini de formules propositionnelles. Alors qu'il est possible de déterminer algorithmiquement si une formule propositionnelle est démontrable ou pas, on sait — depuis les travaux de Gödel, Tarski, Church, Turing et autres — que la même question pour les formules du premier ordre est indécidable. Le théorème de Herbrand montre qu’elle est cependant semi-décidable : bien qu’il n’existe pas d’algorithme qui détermine si une formule donnée est prouvable ou pas, il existe une procédure qui résout partiellement la question en répondant « oui » si et seulement si la formule donnée est prouvable (pour certaines formules non prouvables, le calcul ne s'arrête pas). (fr)
- エルブランの定理（英: Herbrand's theorem）は1930年にジャック・エルブランが発表した数理論理学上の基本定理である。エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。 を節の有限集合とするとき、以下の2つは同値である。
* が充足不能
* から得られる基礎例（エルブラン基底）の有限集合で充足不能なものが存在 エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自動定理証明の理論的な基盤になっている。チューリングマシンの停止性問題と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では一階述語論理を命題論理と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。 なお、エルブランの本来の証明は任意の一階述語論理式を対象としたものだが、多くの場合、冠頭形の論理式に制限し単純化した定理で表される。 (ja)
- Twierdzenie Herbranda to jedno z najważniejszych twierdzeń konstruktywnych logiki pierwszego rzędu: Formuła jest tautologią wtedy i tylko wtedy, gdy tautologią jest pewne rozwinięcie Herbranda tej formuły. Ponieważ każde rozwinięcie jest właściwie skończoną formułą rachunku zdań,a więc da się rozstrzygnąć w czasie skończonym (wykładniczym), liczba rozwinięć Herbrandadla formuły natomiast jest zbiorem przeliczalnym, umożliwia to udowodnienie każdej tautologiilogiki pierwszego rzędu, chociaż może tozająć nieograniczoną ilość czasu. (pl)
- Em lógica matemática, o teorema de Herbrand é um resultado básico de Jacques Herbrand (1930). Ele essencialmente permite um tipo de redução da lógica de primeira ordem para a lógica proposicional. Embora originalmente Herbrand tenha provado seu teorema para fórmulas arbitrárias da lógica de primeira ordem, a versão mais simples, mostrada aqui, que é restrita a fórmulas em forma normal prenex contendo apenas quantificadores existenciais, tornou-se mais popular. Sendo a fórmula de primeira ordem com quantificadores livres. Então é válido se, e somente se, existe uma sequência finita de termos :, com e , de tal forma que é válido. Se isto é válido, é chamado de disjunção de Herbrand para . Informalmente: uma fórmula , em forma prenex contendo quantificadores existenciais só é demonstrável (válida) em lógica de primeira ordem se e somente se uma disjunção composta de instâncias de substituição da sub-fórmula de quantificadores livres de A é uma Tautologia (lógica) (proposicionalmente derivável). A restrição às fórmulas em forma prenex contendo somente quantificadores existenciais não limita a generalidade do teorema, porque as fórmulas podem ser convertidas para a forma prenex e seus quantificadores universais podem ser removidos. (pt)
- 在逻辑学中，埃尔布朗定理(Herbrand's theorem)建立了命题逻辑计算和谓词逻辑计算之间的关系，因此埃尔布朗定理可能是一种已知的确定手段来判断一个命题的命题逻辑计算是否是有限的，对于一个含有复杂谓词的公式，它的谓词逻辑计算也起到同样的判断。通过对埃尔布朗定理的应用，部分解决回答了上述问题。但是虽然有Gödel(哥德尔)，Tarski(塔尔斯基)，Church(邱奇)，Turing(图灵)和其他科学家在逻辑学领域中卓越的研究成果，但是至今不存在一个算法，能够决定一个普遍公式的谓词逻辑计算是否是可计算的这样一个问题，我们不知道这个算法是否是可以被证明的。 (zh)
- Теорема Ербрана — фундаментальний результат математичної логіки, отриманий Жаком Ербраном в 1930 р. Суть теореми у тому, що вона гарантує формальну виводимість (довідність) формули елементарної (першопорядкової) логіки з аксіом, якщо методом Ербрана можна показати загальзначимість цієї формули в т. зв. ербрановському універсумі, що представляє із себе суто синтаксичну (ефективно породжувану) конструкцію. При цьому в основі методу Ербрана лежать ідея непрямого доказу й ідея зведення формули логіки предикатів у скулемовській нормальній формі (можливо, з функціональними символами) до деякого окремого випадку (до пропозиційної формули в канонічній формі), який дозволив би зробити висновок про загальнозначимість вихідної формули. В результаті такої процедури переходу «від часткового до загального» проблема доказовості (виводимості) в деякій першопорядковій системі аксіом зводиться до проблеми загальнозначимості в логіці висловлювань. Видатне значення роботи Ербрана стало очевидним, по-перше, у світлі пізніших теорем Черча і Шеннона про алгоритмічну нерозв'язність проблеми розвязності (загальнозначимості в будь-якому універсумі) для формул елементарної логіки, а по-друге, у світлі алгоритмічних задач в області штучного інтелекту, які спираються на логіку. Досі метод Ербрана служить основою для більшості сучасних автоматичних алгоритмів пошуку доведень. (uk)
|
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is Wikipage redirect
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)