Catta, Davide
[Author]
;
Montpellier
[Contributor];
Retoré, Christian
[Contributor];
Moot, Richard
[Contributor];
Quatrini, Myriam
[Contributor]
Les preuves vues comme des jeux et réciproquement : sémantique dialogique de langages naturel ou logiques ; Proofs as games and games as proofs : dialogical semantics of logical and natural languages
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
Electronic Thesis;
E-Book
Title:
Les preuves vues comme des jeux et réciproquement : sémantique dialogique de langages naturel ou logiques ; Proofs as games and games as proofs : dialogical semantics of logical and natural languages
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Notre travail de thèse se situe au carrefour de plusieurs disciplines :d'une part, la logique mathématique et l'informatique théorique, d'autre part le traitement automatique du langage naturel et plus particulièrement la sémantique formelle du langage naturel. Le fil conducteur est la présence constante des méthodes logiques issues de la théorie de la preuve et par le problème philosophique qui a motivé notre thèse : quels sont les liens entre la notion de preuve et celle de signification linguistique ou logique ?Plus concrètement, nous étudions des systèmes formels dont les preuves sont vues comme des stratégies gagnantes pour des jeux à deux joueurs. Dans ces jeux, un jouer, appelé Proposant, essaye de construire une justification pour un certain énoncé tandis que l'autre, l'Opposant, essaye de construire une réfutation de cet énoncé.La thèse est composée de trois parties, chaque partie contenant deux ou trois chapitres.La première partie est propédeutique. Dans les deux chapitres qui la composent nous présentons les outils mathématiques utilisés dans notre thèse ainsi que les principes logiques et philosophiques qui ont guidés nos travaux, notamment la sémantique inférentialiste.La deuxième partie de notre thèse contient deux longs chapitres, lesquels présentent les résultats de théorie de la démonstration qui constituent le cœur de notre thèse.En particulier, dans le premier chapitre de cette partie, nous définissons précisément un système de logique dialogique pour la logique classique du premier ordre avec termes. Nous montrons que, pour une formule A, l'existence d'une stratégie gagnante pour A équivaut au fait que A est une théorème logique. Bien que des systèmes de logique dialogique pour la logique classique du premier ordre existent depuis les années 1960 il n'existait pas à ce jour de preuve convaincante publiée de ce résultat, notamment en présence de termes. Dans le deuxième chapitre de cette deuxième partie, nous présentons une sémantique dénotationnelle pour la variante constructive de la ...