vignette|Arbre de résolution linéaire
En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire est un système formel inventé par le logicien Jean-Yves Girard en 1987. Du point de vue logique, la logique linéaire décompose et analyse les logiques classique et intuitionniste. Du point de vue calculatoire, elle 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 daffaiblissement qui permet d'éliminer de l'ensemble des hypothèses une hypothèse inutilisée dans le raisonnement.
La logique linéaire peut se comprendre au travers de la correspondance de Curry-Howard comme un système de typage des programmes d'ordre supérieur (lambda-calcul typé) permettant d'exprimer la manière dont ceux-ci gèrent leurs ressources, et notamment le fait qu'une ressource soit consommée linéairement, c'est-à-dire une et une seule fois pendant l'exécution du programme.
La logique linéaire promeut une vision « géométrique » des syntaxes formelles en cultivant l'analogie avec l'algèbre linéaire (espaces cohérents) et en introduisant de nouvelles représentations des preuves/programmes utilisant des graphes (réseaux de preuves), voire des opérateurs (géométrie de l'interaction). Elle a également permis à Girard de proposer une approche logique de la complexité algorithmique (logique linéaire légère et élémentaire).
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Les logiques sous-structurelles sont des logiques mathématiques où certaines règles d'inférence ne sont pas utilisées ou ont une utilisation restreinte. En particulier, par rapport à la logique classique ou à la logique intuitionniste, il leur manque la règle de contraction qui dit peu ou prou 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.
Jean-Yves Girard, né en 1947 à Lyon, est un logicien et mathématicien contemporain, directeur de recherche au CNRS (émérite) au département de logique de la programmation de l'institut de mathématiques de Luminy (devenu l'Institut de Mathématiques de Marseille depuis le ). Il a reçu la médaille d'argent du CNRS en 1983. Depuis 1994, il est correspondant de l'Académie des sciences, et membre de l'Académie européenne depuis 1995. Jean-Yves Girard est un ancien élève de l'École normale d'instituteurs de Lyon (1962) et de l'École normale supérieure de Saint-Cloud (sciences) (1966).
vignette|Arbre de résolution linéaire En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire est un système formel inventé par le logicien Jean-Yves Girard en 1987. Du point de vue logique, la logique linéaire décompose et analyse les logiques classique et intuitionniste. Du point de vue calculatoire, elle 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.
Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.
A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code!
Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics a
Introduit le Mathgraph Theorem Prover, montrant son approche unique pour représenter des propositions et organiser des graphiques pour la logique de premier ordre.
Explore l'application pratique de la théorie du langage, y compris le tri rapide, le typage progressif et la gestion efficace de la mémoire, ainsi que les défis de la synthèse des programmes de réduction.