-
Cet exposé est la transcription d'un exposé au séminaire "Qu'est-ce qu'une logique ?" (le Mardi 9 Avril 1996). Il 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 ? »