Demonstration automatique dans le calcul des constructions

摘要: Le calcul des constructions est une extension de la logique d'ordre superieur dans laquelle le langage termes un lambda-calcul type comprenant types dependants, polymorphes et constructeurs type. La richesse ce systeme permet, en se basant sur semantique heyting l'isomorphisme curry-howard, representer les preuves par termes. puissance calculatoire fait egalement outil bien adapte au raisonnement programmes a preuve leur correction. demonstration automatique l'etude methodes qui partant d'une proposition construisent automatiquement preuve. Dans premiere partie cette these nous developpons telle methode pour constructions. Cette s'inscrit lignee celles developpees robinson du premier ordre huet sous nom resolution. En concerne automatique, nouveaute qu'apportent systemes types, tels que constructions, rapport aux logiques precedents role respectif resolution l'unification. Au l'ordre unification sont separees. ou meme nature, melent algorithme unique. seconde etudions problemes d'equations certaines ses restrictions. Tout d'abord montrons l'algorithme synthese peut etre utilise comme d'unification, plus exactement d'unification fermee. Ensuite cas particuliers decidables indecidables Nous simplement type, filtrage second decidable. indecidable tous calculs comportent polymorphes, inductifs