Property |
Value |
dbo:abstract
|
- 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)
- 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)
|
dbo:namedAfter
| |
dbo:wikiPageID
| |
dbo:wikiPageLength
|
- 11929 (xsd:nonNegativeInteger)
|
dbo:wikiPageRevisionID
| |
dbo:wikiPageWikiLink
| |
prop-fr:wikiPageUsesTemplate
| |
dct:subject
| |
rdfs:comment
|
- 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)
- 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)
|
rdfs:label
|
- Herbrand's theorem (en)
- Satz von Herbrand (de)
- Théorème de Herbrand (fr)
- Теорема Ербрана (uk)
- エルブランの定理 (ja)
|
rdfs:seeAlso
| |
owl:sameAs
| |
prov:wasDerivedFrom
| |
foaf:isPrimaryTopicOf
| |
is dbo:wikiPageDisambiguates
of | |
is dbo:wikiPageWikiLink
of | |
is oa:hasTarget
of | |
is foaf:primaryTopic
of | |