Algèbres des logiques modales et intuitionistes : procédures de décision et formes canoniques / par Annie Foret ; sous la direction de Gérard Huet

Bibliogr. en fin de volume

Thèse de doctorat informatique 1990 Paris 7

L'objet de cette thèse est l'étude des logiques modales et intuitionnistes, dont les structures algébriques, contrairement à la logique classique, sont encore mal connues. Ces deux familles de logique sont particulièrement utilisées aujourd'hui en informatique, en théorie de la programmation et en intelligence artificielle. Les logiques modales et les logiques intuitionnistes ont des liens étroits que nous rappelons et utilisons dans cette étude. Cette thèse comprend trois parties. La première partie donne une présentation uniforme de ces structures logiques, sous les aspects syntaxiques puis sémantiques ― avec la notion centrale des modèles de Kripke. La deuxième partie développe les procédures de décision connues, avec une étude particulière du cas intuitionniste. La dernière partie présente les résultats nouveaux obtenus en partie à l'aide des outils de réécriture: ceci fournit essentiellement de nouvelles procédures de décision et des caractérisations de formes canoniques dans un formalisme uniforme