Il est souvent arrivé que, par le passé, les scientifiques affirment l'existence d'objets inobservables dont ils rejettent aujourd'hui l'existence. Quelle leçon tirer de ce fait ? On est tenté d'en conclure que les méthodes qu'emploient les scientifiques pour connaître l'inobservable ne sont pas fiables, de sorte que cette connaissance serait située hors de leur portée. Cette thèse identifie et rejette deux présupposés qui conduisent à cette conclusion, à savoir que la méthode de l'hypothèse serait la seule manière de produire des connaissances des inobservables, et que cette méthode se déploierait de manière instantanée. Si, au contraire, les modalités concrètes de l'activité expérimentale et la dimension diachronique de la recherche théorique sont prises en compte, chacun de ces deux présupposés doit être rejeté comme abstrait. La connaissance des effondrements théoriques passés légitime alors la croyance en la vérité des théories actuelles. / History of science presents us with numerous cases in which scientists conclude that an unobservable entity previously posited as real actually does not exist. What the lesson is to be drawn from this fact ? One is tempted to draw the conclusion that the methods employed by scientists to produce knowledge of unobservable objects are not reliable: gaining this knowledge would be beyond their reach. This thesis identifies and rejects two presuppositions that lead to this conclusion: that the method of hypothesis is the only way to produce knowledge of unobservables and that it can be employed in an instantaneous manner. On the contrary, if the concrete modalities of the experimental activity and the diachronical dimension of theoretical research are taken into account, each of these two presuppositions appear to be too abstract and should be rejected. Knowledge of past theoretical collapses then legitimates the belief in the truth of current scientific theories.

La théorie des jeux a développé, à ses débuts, une vocation pour les sciences sociales et économiques, avec des applications disparates, comme par exemple le traitement de données médicales. Elle apparaît aujourd'hui comme un paradigme de concepts et de techniques très général, dont le potentiel reste encore à exploiter en informatique. Dans cette thèse nous étudions une branche particulière, la théorie des jeux combinatoires (à deux joueurs), pour en tirer bénéfice dans le domaine, très actif, des sémantiques formelles des langages de programmation. D'un jeu, nous pouvons séparer l'aspect syntaxique, inhérent aux dénouements possibles des matchs, de l'aspect sémantique, inhérent aux prévisions sur le gagnant et la quantification de son gain (en termes d'un enjeu quelconque, tel que l'argent ou le préstige). Pour modeliser la notion de gain, la structure d'évaluation choisie ne doit pas forcément être celle des booléens (gagné ou perdu), ou celle des entiers naturels ou relatifs. Il suffit qu'elle vérifie des propriétés, assez faibles, garantissant l'existence d'une sémantique même lorsque le jeu donne lieu à des matchs infinis, comme dans le cas du jeu de la bisimulation entre processus concurrents, et du jeu de la programmation logique. Dans ce travail, nous étudions la caractérisation sémantique d'un langage logique (avec ou sans contrainte) en termes de jeu à deux joueurs. Au-delà du modèle intuitif des jeux, dont la valeur pédagogique mériterait d'être approfondie, une telle interprétation permet de réutiliser un des algorithmes les plus utilisés dans la théorie des jeux combinatoire, Alpha-Bêta, comme moteur de résolution pour les langages logiques. Les résultats récents et spectaculaires obtenus par les programmes d'échecs (souvenons-nous de la défaite du champion du monde Kasparov contre le programme Deep Blue d'IBM) témoignent d'une forme d'intelligence artificielle développée dans ces programmes qui peut être transposée et exploitée dans la résolution des langages logiques. La résolution d'interrogations existentielles conjonctives dans une théorie de clauses de Horn du premier ordre est en particulier concernée. En effet, la capacité d'Alpha-Bêta à simplifier le calcul ou, en d'autres termes, sa capacité à éliminer les coups inintéressants, n'est pas intimement liée à un type de jeu ou à un type de gain particuliers, mais demande juste des propriétés algébriques qui sont satisfaites dans le jeu de la programmation logique. La correction d'Alpha-Bêta est prouvée de façon formelle pour un éventail de structures très large. Les valeurs calculées pourront être aussi bien des entiers naturels, comme dans le cas du jeu d'échecs, que des substitutions ou des contraintes, comme dans le cas des langages logiques.

No description available.