Logic Theorist, le programme qui démontre

CCapucine

En 1956, la création de Logic Theorist est attribuée à Allen Newell, Herbert Simon et Cliff Shaw, qui auraient conçu ce programme pour démontrer des théorèmes de logique. Le programme ne se contente pas de traiter ces théorèmes comme des objets abstraits : il en produit des démonstrations, et cette capacité devient le cœur de son travail. Son terrain est un ouvrage précis, les Principia Mathematica, écrit par Whitehead et Russell. Logic Theorist démontre une grande partie des théorèmes d’un chapitre de ce livre : le résultat porte donc sur de nombreux théorèmes d’un même chapitre, plutôt que sur l’ensemble de l’ouvrage. Pour l’un de ces théorèmes, le programme trouve une démonstration plus élégante que celle présentée dans le livre. La comparaison porte sur une preuve particulière, au sein d’un ensemble plus vaste de démonstrations, et donne à voir ce que le programme accomplit : établir des théorèmes, avec, dans ce cas, une preuve jugée plus élégante que celle de l’ouvrage. Logic Theorist est présenté à l’atelier de Dartmouth et souvent considéré comme le premier programme d’intelligence artificielle. Il réunit ainsi deux éléments du récit : des théorèmes de logique démontrés par un programme, et une présentation à Dartmouth qui accompagne la place particulière qui lui est souvent reconnue dans l’histoire de l’intelligence artificielle.