Anne-Laure Schneider

Nous allons commencer par étudier la structure mathématique des jeux qui nous seront utiles en logique, structure qui se transposera automatiquement aux preuves. Nous montrerons que la catégorie des jeux simples est close monoïdale symétrique, avant de nous intéresser à des jeux un peu plus complexes, dit jeux avec répétitions, ou jeux d'arènes de Hyland-Ong. Ces jeux, peu exploités encore, fournissent une modélisation particulièrement adaptée aux connecteurs de la logique linéaire. Enfin nous nous intéresserons plus précisément à la logique focalisée d'Andreoli, pour laquelle nous présenterons un modèle qui permet d'implémenter la recherche de preuves sous forme de recherche de stratégie gagnante dans un jeu adapté.

Nous allons définir et étudier une sémantique pour la théorie de la démonstration, en utilisant des jeux à deux joueurs. Les stratégies adoptées par un joueur seront les preuves. Nous allons démontrer que ces jeux constituent une catégorie close monoïdale symétrique, en définissant une composition pour les stratégies. Ce langage nous permettra d'écrire et de prouver de façon différente des théorèmes classiques de la logique. Dans le cadre de ce mémoire, nous allons utiliser plusieurs sortes de jeux différents, chacun d'eux nous donnant un nouveau cadre. Les notions d'innocence et de jeux d'arène dits subtils nous donneront également de nouvelles idées pour développer la théorie de la démonstration.

Un polynôme de R[X] s'écrit comme une somme de carrés si et seulement s'il ne prend que des valeurs positives. Qu'en est-il de polynômes en plusieurs indéterminées ? Le 17^ème problème de Hilbert concernait l'expression de tels polynômes comme somme de carrés. En fait, de nombreux polynômes positifs ne sont pas somme de carrés. Cependant, on a des résultats d'écriture comme somme de carrés de polynômes à indéterminées non commutatives, lorsqu'ils sont positifs dans un sens à définir.
Les polynômes non commutatifs sont évalués en substituant aux indéterminées des opérateurs bornés ou des matrices.
Un polynôme à coefficients dans C, prenant des valeurs positives quels que soient les opérateurs unitaires en lesquels on l'évalue s'écrit comme une somme de carrés. On peut également faire le test avec les opérateurs hermitiens.
Si pour toute matrice réelle de toute taille, l'évaluation du polynôme donne une matrice positive, on dit que le polynôme est "positif au sens matriciel". On a : un polynôme est "positif au sens matriciel" si et seulement si ce polynôme est somme de carrés.

En général, lorsque l'on cherche à déterminer si une formule F est vraie ou non, la seule façon de procéder est de supposer qu'elle est vraie, et de chercher une preuve. S'il n'y en a pas, peut-être que l'on a obtenu un contre-exemple, mais si l'on veut trouver une preuve de la négation de F, il nous faut recommencer le processus de recherche de preuve à zéro.
Ici nous proposons une sémantique des jeux qui nous permet de rechercher simultanément une preuve de F et une preuve de sa négation. Ces travaux sont encore en cours, le but étant d'obtenir une telle sémantique pour la logique linéaire. Pour cela, nous avons commencé avec LKF+ (logique classique avec focus et uniquement les connecteurs positifs), et ensuite étendu les jeux à LKF, et ensuite à MALL avec focus. La principale différence avec les jeux habituels est qu'ici le Joueur cherche à prouver F, et que l'Opposant, au lieu de seulement chercher à atteindre un contre-exemple à F, cherche à prouver la négation de F.
Ces jeux peuvent être plus particulièrement utiles pour les problèmes ouverts, pour lesquels on ne peut pas faire de conjecture valable, et ils nous aident à comprendre comment un échec dans la recherche de preuve peut malgré tout nous donner des informations utiles pour prouver le contraire.

Nous allons commencer par étudier la structure mathématique des jeux qui nous seront utiles en logique, structure qui se transposera automatiquement aux preuves. Nous montrerons que la catégorie des jeux simples est close monoïdale symétrique, avant de nous intéresser à des jeux un peu plus complexes, dit jeux avec répétitions, ou jeux d'arènes de Hyland-Ong. Ces jeux, peu exploités encore, fournissent une modélisation particulièrement adaptée aux connecteurs de la logique linéaire. Enfin nous nous intéresserons plus précisément à la logique focalisée d'Andreoli, pour laquelle nous présenterons un modèle qui permet d'implémenter la recherche de preuves sous forme de recherche de stratégie gagnante dans un jeu adapté.