Analyse de la déduction et mise en évidence de points de contrôle qui apparaissent dans une preuve effectuée sur une machine. Les raisonnements qui peuvent être menés pour les comparer, les exploiter, les réutiliser sont de nature analogique et ne sont pas eux-mêmes intégrés dans le mécanisme de principe de supervision. – Introduction; Motivations de la déduction automatique; Preuves de la déduction automatique et preuves mathématiques; L’analogie dans les preuves mathématiques et automatiques; Utiliser l’analogie en déduction automatique; Manipulation de preuves; Différence entre deux problèmes; Définir une différence; Analogie utilisant une différence élémentaire; Utilisation plus générale de la différence.