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

Auteur principal : Dowek, Gilles, 1966-, AuteurAuteur secondaire : Huet, Gérard, 1947-, Directeur de thèseAuteur secondaire collectivité : Université Paris Diderot - Paris 7, Etablissement de soutenanceType de document : ThèseLangue : français.Pays: France.Éditeur : [S.l.] : [s.n.], 1991Description : 1 vol. (128 p.) ; 30 cmISBN: 2726107168.Bibliographie : Bibliogr. p. 123-126. Index.Sujet MSC : 68V15, Computer science support for mathematical research and practice, Theorem proving
03B35, General logic, Mechanization of proofs and logical operations
03B40, General logic, Combinatory logic and lambda calculus
03B70, General logic, Logic in computer science
97-02, Research exposition (monographs, survey articles) pertaining to mathematics education
Note de thèse: Thèse de doctorat, informatique fondamentale, 1991, Paris 7En-ligne : Zentralblatt | MathSciNet Item type: Thèse
Tags from this library: No tags from this library for this title. Log in to add tags.
Holdings
Current library Call number Status Date due Barcode
CMI
Salle S
Thèses DOW (Browse shelf(Opens below)) Available 10610-01

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

There are no comments on this title.

to post a comment.