Cet exposé aborde un aspect de la démonstration automatique. La démonstration automatique est une branche de l’informatique consacrée à la construction de programmes qui cherchent à démontrer des propositions. J’ai choisi ce sujet parce qu’il me semble qu’il peut apporter une petite contribution à la question générale du séminaire “Qu’est-ce qu’une logique ?”. Je dois dire, avant de commencer, que cette question me met particulièrement mal à l’aise. Elle suppose qu’il y a un certain nombre de choses qu’on appelle des logiques, par exemple, la logique du premier ordre, la logique modale, ou plus précisément telle logique modale : S4 ou S5, la logique d’ordre supérieur, etc. et qu’il faut définir cette classe de choses. Dans ce sens, la notion de “logique” me semble, sinon synonyme, au moins très proche de celle de “système formel”. On peut donc donner une première définition “une logique est un système formel”, ce qui nous amène au problème de définir la notion de “système formel”. Mais il me semble, et c’est là que la question me met mal à l’aise, que cette notion de système formel est déjà relativement bien définie. On ne peut donc pas faire comme si personne avant nous n’avait défini cette notion mais il me semble au contraire qu’il faut partir de cette définition.