Démonstration automatique dans le calcul des constructions / par Gilles Dowek ; sous la direction de Gérard Huet

Bibliogr. p. 123-126. Index

Thèse de doctorat informatique fondamentale 1991 Paris 7

Le Calcul des Constructions est une extension de la logique d'ordre supérieur dans laquelle le langage des termes est un lambda-calcul typé comprenant des types dépendants, des types polymorphes et des constructeurs de type. La richesse de ce système de type permet, en se basant sur la sémantique de Heyting et l'isomorphisme de Curry-Howard, de représenter les preuves par des termes. La puissance calculatoire de ce système en fait également un outil bien adapté au raisonnement sur des programmes et à la preuve de leur correction. La démonstration automatique dans un système logique est l'étude des méthodes qui partant d'une proposition en construisent automatiquement une preuve. Dans la première partie de cette thèse nous développons une telle méthode pour le Calcul des Constructions. Cette méthode s'inscrit dans la lignée de celles développées par Robinson pour la logique du premier ordre et Huet pour la logique d'ordre supérieur sous le nom de résolution. En ce qui concerne la démonstration automatique, la nouveauté qu'apportent les systèmes de types, tels que le Calcul des Constructions, par rapport aux systèmes logiques précédents concerne le rôle respectif de la résolution et de l'unification. Au premier ordre et à l'ordre supérieur résolution et unification sont séparées. Dans les systèmes de types, où termes et preuves sont de même nature, résolution et unification se mêlent en un algorithme unique. Dans la seconde partie de cette thèse nous étudions les problèmes de résolution d'équations dans le Calcul des Constructions et certaines de ses restrictions. Tout d'abord nous montrons que l'algorithme de synthèse de preuves de la première partie peut être utilisé comme algorithme d'unification, ou plus exactement comme algorithme d'unification fermée. Ensuite nous étudions les cas particuliers décidables et indécidables de l'unification. Nous montrons que dans le Calcul des Constructions, comme dans le lambda-calcul simplement typé, le filtrage du second ordre est décidable. Nous montrons également que le filtrage d'ordre supérieur est indécidable dans tous les calculs qui comportent des types dépendants, des types polymorphes, des constructeurs de types ou des types inductifs