Algebres des logiques modales et intuitionnistes : procedures de decision et formes canoniques
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
Pas de résumé disponible.
Abstract FR:
L'objet de cette these est l'etude des logiques modales et intuitionnistes, dont les structures algebriques, contrairement a la logique classique, sont encore mal connues. Ces deux familles de logique sont particulierement utilisees aujourd'hui en informatique, en theorie de la programmation et en intelligence artificielle. Les logiques modales et les logiques intuitionnistes ont des liens etroits que nous rappelons et utilisons dans cette etude. Cette these comprend trois parties. La premiere partie donne une presentation uniforme de ces structures logiques, sous les aspects syntaxiques puis semantiques avec la notion centrale des modeles de kripke. La deuxieme partie developpe les procedures de decision connues, avec une etude particuliere du cas intuitionniste. La derniere partie presente les resultats nouveaux obtenus en partie a l'aide des outils de reecriture: ceci fournit essentiellement de nouvelles procedures de decision et des caracterisations de formes canoniques dans un formalisme uniforme