La réalisabilité est une branche de la logique mathématique, et plus précisément de la théorie de la démonstration, qui définit une relation logique entre les formules d'un système logique et les programmes d'un modèle de calcul. Elle a été introduite dans les années 40 par Kleene comme une interprétation des formules de l' (en) par des ensembles (d'indices) de fonctions récursives. Elle a depuis été étendue à toute sorte d'autres systèmes logiques, et aujourd'hui est vue comme une généralisation de la correspondance de Curry-Howard.

Property Value
dbo:abstract
  • La réalisabilité est une branche de la logique mathématique, et plus précisément de la théorie de la démonstration, qui définit une relation logique entre les formules d'un système logique et les programmes d'un modèle de calcul. Elle a été introduite dans les années 40 par Kleene comme une interprétation des formules de l' (en) par des ensembles (d'indices) de fonctions récursives. Elle a depuis été étendue à toute sorte d'autres systèmes logiques, et aujourd'hui est vue comme une généralisation de la correspondance de Curry-Howard. Étant donnés une formule et un programme on note la propriété « réalise » ; cette notation est réminiscente du forcing de Cohen avec lequel la réalisabilité présente des analogies formelles. La réalisabilité conduit à une interprétation des formules comme des spécifications de programme : par exemple la tautologie est réalisée par les programmes qui étant donnée une entrée de type rendent un résultat de type . (fr)
  • La réalisabilité est une branche de la logique mathématique, et plus précisément de la théorie de la démonstration, qui définit une relation logique entre les formules d'un système logique et les programmes d'un modèle de calcul. Elle a été introduite dans les années 40 par Kleene comme une interprétation des formules de l' (en) par des ensembles (d'indices) de fonctions récursives. Elle a depuis été étendue à toute sorte d'autres systèmes logiques, et aujourd'hui est vue comme une généralisation de la correspondance de Curry-Howard. Étant donnés une formule et un programme on note la propriété « réalise » ; cette notation est réminiscente du forcing de Cohen avec lequel la réalisabilité présente des analogies formelles. La réalisabilité conduit à une interprétation des formules comme des spécifications de programme : par exemple la tautologie est réalisée par les programmes qui étant donnée une entrée de type rendent un résultat de type . (fr)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 979264 (xsd:integer)
dbo:wikiPageLength
  • 2255 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 188442511 (xsd:integer)
dbo:wikiPageWikiLink
prop-fr:année
  • 1945 (xsd:integer)
  • 1998 (xsd:integer)
  • 2002 (xsd:integer)
prop-fr:auteursOuvrage
  • S. R. Buss (fr)
  • S. R. Buss (fr)
prop-fr:langue
  • en (fr)
  • en (fr)
prop-fr:lienAuteur
  • Stephen Cole Kleene (fr)
  • Stephen Cole Kleene (fr)
prop-fr:nom
  • Troelstra (fr)
  • Oosten (fr)
  • Kleene (fr)
  • Troelstra (fr)
  • Oosten (fr)
  • Kleene (fr)
prop-fr:prénom
  • Anne (fr)
  • S. C. (fr)
  • Jaap van (fr)
  • Anne (fr)
  • S. C. (fr)
  • Jaap van (fr)
prop-fr:périodique
  • Journal of Symbolic Logic (fr)
  • Mathematical Structures in Computer Science (fr)
  • Journal of Symbolic Logic (fr)
  • Mathematical Structures in Computer Science (fr)
prop-fr:titre
  • Realizability: an historical essay (fr)
  • On the interpretation of intuitionistic number theory (fr)
  • Realizability: an historical essay (fr)
  • On the interpretation of intuitionistic number theory (fr)
prop-fr:titreChapitre
  • Realizability (fr)
  • Realizability (fr)
prop-fr:titreOuvrage
  • Handbook of proof theory (fr)
  • Handbook of proof theory (fr)
prop-fr:url
prop-fr:wikiPageUsesTemplate
prop-fr:éditeur
  • North Holland (fr)
  • North Holland (fr)
dct:subject
rdfs:comment
  • La réalisabilité est une branche de la logique mathématique, et plus précisément de la théorie de la démonstration, qui définit une relation logique entre les formules d'un système logique et les programmes d'un modèle de calcul. Elle a été introduite dans les années 40 par Kleene comme une interprétation des formules de l' (en) par des ensembles (d'indices) de fonctions récursives. Elle a depuis été étendue à toute sorte d'autres systèmes logiques, et aujourd'hui est vue comme une généralisation de la correspondance de Curry-Howard. (fr)
  • La réalisabilité est une branche de la logique mathématique, et plus précisément de la théorie de la démonstration, qui définit une relation logique entre les formules d'un système logique et les programmes d'un modèle de calcul. Elle a été introduite dans les années 40 par Kleene comme une interprétation des formules de l' (en) par des ensembles (d'indices) de fonctions récursives. Elle a depuis été étendue à toute sorte d'autres systèmes logiques, et aujourd'hui est vue comme une généralisation de la correspondance de Curry-Howard. (fr)
rdfs:label
  • Réalisabilité (fr)
  • 可实现性 (zh)
  • Réalisabilité (fr)
  • 可实现性 (zh)
rdfs:seeAlso
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is oa:hasTarget of
is foaf:primaryTopic of