Abstract FR:

Notre objectif est de proposer un outil de preuve automatique dans le cadre d'une logique temporelle. Notre travail s'articule en deux volets. D'une part, nous presentons une logique temporelle qui etend au premier ordre la logique modale propositionnelle de halpern et shoham ; il s'agit d'une logique d'intervalles interpretee dans une algebre de relations. D'autre part, nous proposons une methode de demonstration automatique par traduction dans un langage type du premier ordre avec en fond la theorie de l'ordre strict lineaire. Plutot que d'integrer les axiomes de cette theorie aux formules a refuter, nous preferons adapter le systeme d'inference en modifiant l'algorithme d'unification. Nous appliquons cette demarche a une methode classique de preuve automatique dite methode des connexions et definissons ainsi la methode des connexions cycliques, laquelle utilise une forme particuliere d'unification, dite e-unification rigide, pour laquelle nous proposons un algorithme effectif base sur des techniques de completion et de paramodulation. Nous discutons egalement du probleme d'e-unification rigide simultane, au sujet duquel de nombreuses erreurs ont ete commises dans la litterature, et montrons pourquoi l'indecidabilite de ce probleme, tres recemment etablie par voronkov et degtyarev, ne remet pas en cause notre methode