En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire, inventée par le logicien Jean-Yves Girard en 1986, est un système formel qui, du point de vue logique, décompose et analyse les logiques classique et intuitionniste et, du point de vue calculatoire, est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources.

Property Value
dbo:abstract
  • En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire, inventée par le logicien Jean-Yves Girard en 1986, est un système formel qui, du point de vue logique, décompose et analyse les logiques classique et intuitionniste et, du point de vue calculatoire, est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources. La logique classique n'étudie pas les aspects les plus élémentaires du raisonnement. Sa structure peut être décomposée dans des systèmes formels plus élémentaires qui décrivent des étapes plus fines de la déduction ; en particulier, il est possible de s'intéresser à des logiques où certaines règles de la logique classique n'existent pas. De telles logiques sont appelées des logiques sous-structurelles. L'une de ces logiques sous-structurelles est la logique linéaire ; il lui manque en particulier la règle de contraction de la logique classique qui dit en gros que si on peut faire un raisonnement avec une même hypothèse invoquée deux fois, on peut faire le même raisonnement sans dupliquer cette hypothèse et la règle d'affaiblissement qui permet d'éliminer de l'ensemble des hypothèses une hypothèse inutilisée dans le raisonnement. (fr)
  • En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire, inventée par le logicien Jean-Yves Girard en 1986, est un système formel qui, du point de vue logique, décompose et analyse les logiques classique et intuitionniste et, du point de vue calculatoire, est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources. La logique classique n'étudie pas les aspects les plus élémentaires du raisonnement. Sa structure peut être décomposée dans des systèmes formels plus élémentaires qui décrivent des étapes plus fines de la déduction ; en particulier, il est possible de s'intéresser à des logiques où certaines règles de la logique classique n'existent pas. De telles logiques sont appelées des logiques sous-structurelles. L'une de ces logiques sous-structurelles est la logique linéaire ; il lui manque en particulier la règle de contraction de la logique classique qui dit en gros que si on peut faire un raisonnement avec une même hypothèse invoquée deux fois, on peut faire le même raisonnement sans dupliquer cette hypothèse et la règle d'affaiblissement qui permet d'éliminer de l'ensemble des hypothèses une hypothèse inutilisée dans le raisonnement. (fr)
dbo:discoverer
dbo:wikiPageID
  • 526211 (xsd:integer)
dbo:wikiPageLength
  • 14475 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 176122587 (xsd:integer)
dbo:wikiPageWikiLink
prop-fr:wikiPageUsesTemplate
dct:subject
rdfs:comment
  • En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire, inventée par le logicien Jean-Yves Girard en 1986, est un système formel qui, du point de vue logique, décompose et analyse les logiques classique et intuitionniste et, du point de vue calculatoire, est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources. (fr)
  • En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire, inventée par le logicien Jean-Yves Girard en 1986, est un système formel qui, du point de vue logique, décompose et analyse les logiques classique et intuitionniste et, du point de vue calculatoire, est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources. (fr)
rdfs:label
  • Logica lineare (it)
  • Logique linéaire (fr)
  • 線形論理 (ja)
  • Logica lineare (it)
  • Logique linéaire (fr)
  • 線形論理 (ja)
rdfs:seeAlso
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:discipline of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is oa:hasTarget of
is foaf:primaryTopic of