Cette thèse développe une approche originale de l'interprétation interactive de la théorie de la démonstration en logique linéaire. À l'inverse du cadre joueur/opposant communément associé aux sémantiques des jeux pour la logique, nous proposons un modèle dans lequel les deux joueurs ont des rôles symétriques. Plus précisément, nous passons d'une situation dans laquelle un joueur tente de démontrer un énoncé tandis que l'autre tente de le réfuter à une situation dans laquelle les deux joueurs tentent de démontrer des énoncés contraires. Dans la tradition du calcul vu comme comme recherche de démonstrations, chaque étape de l'interaction est vue comme une étape de deux recherches de démonstrations orthogonales en calcul des séquents. Ce travail contribue dans une certaine mesure à formaliser les liens entre la recherche de démonstrations et la normalisation de démonstrations. Nous présentons d'abord un jeu symétrique simple pour le fragment additif de la logique linéaire, en guise d'introduction à la recherche duale de démonstrations. Nous passons ensuite à un jeu symétrique bien plus complexe pour le fragment additif et multiplicatif de la logique linéaire. Afin d'obtenir un résultat de pleine complétude, nous développons ensuite un troisième jeu à la fois symétrique et concurrent. Enfin, nous étudions quelques extensions de notre modèle.
| Identifer | oai:union.ndltd.org:CCSD/oai:pastel.archives-ouvertes.fr:pastel-00006196 |
| Date | 15 October 2009 |
| Creators | Delande, Olivier |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0018 seconds