Abstract FR:

En démonstration automatique pour les logiques modales on distingue les méthodes directes des méthodes par traduction. La première partie du mémoire est relative aux méthodes directes. Des calculs par résolution complets sont définis pour les logiques propositionnelles C, CD et CT. Pour ce qui est des calculs par tableaux, différentes classes de stratégies complètes sont définies pour une famille de logiques modales propositionnelles usuelles. Nous avons implémenté (et testé) ces stratégies dans le démonstrateur pour logiques modales d'ATINF. En complément de ce travail, pour une classe de logiques normales multi-modales, il a été montré que SAT peut être réduit à 3-SAT de façon polynomiale. La seconde partie du mémoire est consacrée à la notion de traduction inverse que nous avons introduite. En effet, avec les méthodes par traduction, si une preuve est obtenue dans la logique cible, l'utilisateur qui a formalisé son problème dans la logique source peut difficilement faire le lien avec son problème initial. Afin d'étudier la construction de preuves dans la logique source à partir de preuves dans la logique cible, une hiérarchie de traductions inverses a été introduite. Ainsi pour les logiques D, T, S5, S4, D4 (propositionnelles ou du premier ordre) différentes traductions inverses sont étudiées lorsque des calculs par résolution, tableaux et connexion sont utilisés