Structures multi-contextuelles et logiques modales intuititionnistes et hybrides, Multi-contextual structures and intuitionistic modal and hybrid logics

AVERTISSEMENT

Ce document est le fruit d'un long travail approuvé par le
jury de soutenance et mis à disposition de l'ensemble de la
communauté universitaire élargie.

Il est soumis à la propriété intellectuelle de l'auteur. Ceci
implique une obligation de citation et de référencement lors
de l’utilisation de ce document.

D’autre part, toute contrefaçon, plagiat, reproduction
illicite encourt une poursuite pénale.


➢ Contact SCD Nancy 1 : theses.sciences@scd.uhp-nancy.fr




LIENS


Code de la Propriété Intellectuelle. articles L 122. 4
Code de la Propriété Intellectuelle. articles L 335.2- L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm Département de formation doctorale en informatique École doctorale IAEM Lorraine
UFR STMIA D.F.D. Informatique
Structures Multi-Contextuelles et
Logiques Modales Intuitionnistes et
Hybrides
Thèse
présentée et soutenue publiquement le 3 décembre 2010
pour l’obtention du
Doctorat de l’université Henri Poincaré – Nancy 1
(spécialité informatique)
par
Yakoub SALHI
Composition du jury
Président :
Stéphane Demri Directeur de recherche, CNRS, Cachan, France
Rapporteurs :
Valeria De Paiva Directeur de recherche, Cuill Inc., Menlo Park, Cali-
fornie, États-Unis d’Amérique
Andreas Herzig Directeur de recherche CNRS, Toulouse, France
Examinateurs :
Patrick Blackburn Directeur de recherche, INRIA, Nancy, France
Stéphane Demri de recherche, CNRS, Cachan, France
Didier Galmiche Professeur, Université Henri Poincaré, Nancy, France
Dominique Larchey-Wendling Chargé de recherche, CNRS, Nancy, France
Laboratoire Lorrain de Recherche en Informatique et ses Applications – UMR 7503i
À mes parents et à ma famille.iiiii
Remerciements
Jetienstoutd’abordàremercierlesmembresdujuryquim’ontfaitl’honneurdeparticiper
à la critique ainsi qu’à la soutenance de ma thèse :
– Mme. Valeria De Paiva, Directrice de recherche à Cuil incorporation en Californie, qui a
accepté d’être rapporteur de cette thèse, et dont les nombreuses remarques ont été très
constructives;
– M. Andreas Herzig, Directeur de recherche au CNRS à Toulouse, qui m’a fait lui aussi
l’honneur et le plaisir d’accepter d’être rapporteur de ma thèse, et dont les différentes
remarques et suggestions m’ont aidé dans la mise en valeur des idées présentées dans ce
mémoire;
– M.PatrickBlackburn,Directeurderechercheàl’INRIALorraine,quejeremercied’avoir
accepté de faire partie du jury de thèse;
– Stéphane Demri, Directeur de recherche au CNRS à Cachan, qui m’a fait l’honneur de
présider le jury, et que je remercie également pour l’intérêt qu’il a porté à ma thèse;
– Dominique Larchey-Wendling, Chargé de recherche au CNRS à Nancy, qui a accepté
d’être membre de mon jury, et avec qui j’ai eu des discussions très enrichissantes;
– DidierGalmiche,Professeuràl’universitéHenriPoincaréàNancy,quin’apasseulement
étémembredujurymaissurtoutmondirecteurdethèse.Jeleremerciechaleureusement
pour la patience dont il a fait preuve et pour l’énergie et le temps qu’il a consacré à me
soutenir et me prodiguer des conseils sur tous les plans de ma vie thésard. Un grand
merci Didier!
Je souhaite également remercier les membres de ma famille et mes proches de leur soutien
sansfaille.Mespenséesvonttoutparticulièrementàmesparents, monpetitfrèreAyoubetma
petite soeur Djihane. Je tiens aussi à remercier tout mon groupe : Houda, Taha, Asma, Farhet
et Khanssa pour leur aide, sans oublier mes grands amis Reda et Salim. Merci aux collègues
qui m’ont aidé dans la préparation de ma soutenance : Mounira, Henri et Jean-René.
JetiensensuiteàremerciervivementNoëlleCarbonell,professeur,pourlesencouragements
qu’elle a su me faire. C’était avec beaucoup de tristesse que j’ai appris son décès. Merci aussi
à Dominique Mery, professeur, dont j’ai également apprécié les encouragements.
Enfin, je remercie tous ceux qui sont venus assister à la soutenance de ma thèse et au pot
qui a suivi.ivv
« C’est avec la logique que nous prouvons et avec
l’intuition que nous trouvons. »
Henri Poincaré (1854 – 1912)vivii
Résumé
En informatique, les logiques formelles ont une place centrale dans la représentation et
le traitement des connaissances. Elles sont utilisées pour la modélisation et la vérification
de systèmes informatiques et de leurs propriétés ainsi que pour la formalisation de différents
types de raisonnement. Dans ce contexte il existe un large spectre de logiques non-classiques
parmi lesquelles les logiques modales jouent un rôle important. Alors que les logiques modales
classiques ont été largement étudiées, nous nous focalisons dans cette thèse sur les logiques
modales intuitionnistes et aussi hybrides floues en abordant un certain nombre de questions
principalement du point de vue de la théorie de la démonstration. Nous proposons pour ces
logiquesdenouveauxsystèmesdepreuve,notammentsuivantlesformalismesdedéductionna-
turelleetdecalculdesséquents,quisontfondéssurdenouvellesstructuresmulti-contextuelles
généralisant la structure standard de séquent.
Ainsi dans le cadre des logiques modales intuitionnistes formées à partir des combinaisons
des axiomes T, B, 4 et 5, nous définissons des systèmes de preuve sans labels ayant de bonnes
propriétés comme par exemple celle de la sous-formule. En outre, nous proposons des procé-
dures de décision simples à partir de nos nouveaux calculs des séquents. Nous étudions égale-
mentlapremièreversionintuitionnistedelalogiquehybrideIHLetnousproposonssonpremier
calcul des séquents à partir duquel nous donnons la première démonstration de sa décidabi-
lité. Enfin, nous introduisons une nouvelle famille de logiques hybrides floues fondées sur les
logiques modales de Gödel. Nous proposons pour ces des procédures de décision avec
génération de contre-modèles en utilisant un ensemble de règles de preuve fondées sur une
structure multi-contextuelle adaptée.
Mots-clés:logiquesmodalesintuitionnistes,logiqueshybrides,structuresmulti-contextuelles,
déduction naturelle, calcul des séquents, décidabilité, procédures de décision.
Abstract
In computer science, formal logics are central for studying the representation and the
treatment of knowledge. Indeed, they are widely used for modeling and verifying computer
systems and their properties and also for formalizing different kinds of reasoning. In this
context there exist many non-classical logics and among them modal logics play a key role.
As classical modal logics have been deeply studied, we focus in this thesis on the intuitionistic
modal logics and also on fuzzy hybrid logics by studying some important questions mainly
from the viewpoint of proof theory . We define for these logics new proof systems, following
natural deduction and sequent calculus formalisms, that are based on new multi-contextual
structures generalizing the standard sequent structure.
Then in the framework of the intutionistic modal logics obtained from the combinations
of the axioms T, B, 4 and 5, we define label-free proof systems having nice properties, like for
instance the subformula property. Moreover we propose simple decision procedures from our
new sequent calculi. We also study the first intuitionistic version of hybrid logic called IHL
and define its first sequent calculus from which we provide the first proof of its decidability.
Finally, we introduce a new family of fuzzy hybrid logics that are based on Gödel modal logics
and we define for these logics some decision procedures with contermodel generation by using
a set of proof rules based on an appropriate multi-contextual structure.
Keywords : intuitionistic modal logics, hybrid logics, multi-contextual structures, natural
deduction, sequent calculus, decidability, decision procedures.