Cours de Logique modale
2ème partie du module MFIA
Olivier Gasquet
ØBibliographie :
Ø
A companion to modal logic (Hughes et Cresswell)
Ø
Modal logic (Chellas)
Plan du cours
Introduction : Histoire et motivation en IA
Partie 1: Systèmes monomodaux
Chap1. Généralités sur la sémantique
Chap. 2 : Système K :
o
Langage et Axiomatique
o
Sémantique (de Kripke)
§ Satisfaction,
validité, vérité
o
Caractérisation (énoncé)
Plan du cours (suite)
Chap. 3 : Les axiomes D, T, B, 4, 5 :
o
Lecture des axiomes
o
Axiomatique
o
Sémantique du 2ème ordre
o
Correspondance
o
Sémantique du 1er ordre
Chap. 4 : Systèmes basés sur les axiomes G(k,l,m,n)
o
Correspondance
o
Théorème de Lemmon-Scott / Sahlqvist
o
Modèles canoniques et complétude
Plan du cours (suite)
Chap. 5 : Décidabilité par la méthode des filtrations
o
Définitions
o
Théorèmes
o
Exemples, décidabilité et contre-exemple
Chap. 6 : Déduction automatique : la méthode des tableaux
o
Présentation informelle
o
Présentation formelle
§ Définitions
§ Règles
classiques
§ Règles
pour K
§ Règles
pour D, T, 4
§ Adéquation
et complétude (énoncé)
§ Terminaison
et test de boucle
§ Stratégies
complètes et terminantes, complexité
Plan du cours
Partie 2: Systèmes multimodaux
o
Chap. 7 : Système multi-K
o
Chap. 8 : Les axiomes d’interaction
o
Chap. 9 : PDL
Partie 3: Autres systèmes
o
Chap. 10 : Logiques Temporelles
o
Chap. 11 : Logiques Terminologiques
o
Chap. 12 : Systèmes non-normaux
o
Chap. 13 : Systèmes précicatifs
Introduction : histoire
Aristote et les futurs contingents :
o
« Il est possible qu’on ait PILE » est vraie
Ø Lié au fait que PILE fait
partie des résultats possibles
o
« Il est impossible qu’on ait PILE » est fausse
Ø Lié au fait que PILE fait
partie des résultats possibles
o
« Il est possible qu’on ait PILE ou non Pile» est
logiquement vraie
Ø Non lié au fait que PILE fasse
partie des résultats possibles
o « Il est
impossible qu’on n’ait ni PILE, ni non PILE» est logiquement fausse
ØNon lié au fait que PILE fasse
partie des résultats possibles
Introduction : histoire
Modalités du nécessaire et du possible :
o
Nécessaire, Possible, Impossible et Contingent
o
Se ramènent à la seule modalité du nécessaire :
ØNécessaire A
ØImpossible A = Nécessaire non-A
ØNon Nécessaire A = Contingent A
ØPossible A = Non nécessaire
non-A
ØPile ou non-Pile est
nécessairement vrai
ØPile et non-Pile est impossible
= Pile et non-Pile est néc. faux
ØPile est contingent = Pile n’est
pas nécessairement vrai
ØPile est possible = non-Pile
n’est pas nécessairement vrai
Introduction : histoire
Raisonnement :
o
(Nécessaire A Ù Possible
B) ® Possible (A Ù B) ?
o
(Nécessaire A Ù Possible ØA) ®
faux ?
o
Nécessaire A ® A ?
o
A ® Possible A ?
o
Nécessaire A ® Possible A ?
o
Nécessaire (A ® B) ® (Nécessaire A ® Nécessaire B) ?
o
Si |-- A alors |-- Nécessaire A ?
o
Si non |-- A alors |-- Possible ØA ?
Introduction : histoire moderne
Deux solutions pour intégrer la nécessité à la LC :
o
Renoncer à l’extensionnalité :
p
|
£p
|
£p
|
£p
|
£p
|
£p
|
0
|
1
|
0
|
1
|
0
|
?
|
1
|
1
|
0
|
0
|
1
|
?
|
o
Renoncer à la bivalence :
{vrai, faux, indéterminé},
{vrai,plutôt vrai, plutôt
faux, faux},
…
[0,1],
Autres structures (ordres
totaux, partiels, …)
Introduction : histoire moderne
Autres modalités (linguistique):
o
Le verbe d’une proposition est « modifié » (adverbe,
mode,…)
Ø« Le résultat est probablement
pile » Incertaine
Ø« Le résultat serait
pile (si …) » Conditionnelle
Ø« Je sais que le résultat
est pile » Epistémique
Ø« Je crois que le résultat
est pile » Doxastique
Ø« Il est obligatoire d’avoir
pile ou d’avoir face » Déontique
Ø« Après le lancer, on aura
soit pile, soit face » Dynamique
Ø« Je veux que le résultat
soit pile » Intentionnelle
Ø« Partout ailleurs le
résultat est pile » Spatiale
Introduction : histoire moderne
Autres modalités (linguistique):
o
Modifications multiples (multimodales)
Ø« Tu crois que je sais
quel est le résultat»
Ø« Il est obligatoire
qu’après le lancer, le résultat soit pile ou face »
Ø« Je veux qu’elle croit
que le résultat est pile »
Ø« Après que tu me l’as
dit, je crois que tu crois que le résultat est pile »
Ø« Partout ailleurs
quelqu’un croit qu’ici le résultat est pile »
Introduction : histoire moderne
Autres modalités
£
= دØ
|
Ø£Ø = ¯
|
£Ø = د
|
Ø£ = ¯Ø
|
Nécessaire
|
Possible
|
Impossible
|
Contingent
|
Certain
|
Plausible
|
Exclus
|
Contestable
|
Obligatoire
|
Permis
|
Interdit
|
Facultatif
|
Voulu
|
Acceptable
|
Refusé
|
?
|
Cru
|
Envisageable
|
Rejeté
|
?
|
Dorénavant
|
Un de ces jours
|
Jamais
|
Pas éternellement
|
Partout ailleurs
|
Quelque part ailleurs
|
Nulle part ailleurs
|
Pas partout ailleurs
|
Introduction : motivation en IA
Représentation :
o
des connaissances, de l’incertain, des croyances, des normes, des
actions, des désirs, du conditionnel, du temps, de l’espace…
Raisonnement :
o
Je sais que p ® Je sais
que je sais que p ?
o
Je crois que p ® Je sais
que je crois que p ?
o
Après que tu m’as dit que tu es à Toulouse,
je crois que tu y
es ?
o
Je sais que demain c’est jeudi
® Demain, je saurai qu’on est jeudi ?
o
Je ne suis pas sûr que p
® Je sais que je ne suis pas sûr que p ?
Chap. 1 - Généralités sur la sémantique
Kripke et les mondes possibles
o
Nécessaire A = A est vrai dans tous les mondes possibles
o
Possible A = A est vrai dans au - un monde possible
o
Impossible A = A n’est vrai dans aucun monde possible
o
Contingent A = A est faux dans au - un monde possible
Axiome K et règle de Nécessitation :
o
K : £ (A ® B) ®
(£ A ® £ B)
o
Nec : Si |-- A alors |-- £
A
Þ Automatiquement vrai !
Chap. 1 - Généralités sur la sémantique
Raisonnement
o
(£A Ù ¯B)
® ¯(A
Ù B) ?
o
(£A Ù ¯ØA) ®
^ ?
o
(£A Ù £B)
® £
(A Ù B) ?
o
(¯A Ù ¯B)
® ¯
(A Ù B) ?
o
£ (A Ù B) ® (£A Ù
£B) ?
o
¯ (A Ù B) ® (¯A Ù
¯B) ?
o
£A ® A ?
o
A ® ¯A ?
o
£A ® ¯A ?
Chap. 2, 3, 4, 5
Chap. 2 : Système K :
o
Langage et Axiomatique
o
Sémantique (de Kripke)
§ Satisfaction,
validité, vérité
o
Caractérisation (énoncé)
Chap. 3 : Systèmes basés sur les axiomes D, T, B, 4, 5 :
o
Lecture des axiomes
o
Axiomatique
o
Sémantique du 2nd et du 1er ordre
o
Caractérisation (énoncé)
Chap. 4 : Systèmes basés sur les axiomes G(k,l,m,n)
o
Théorème de Lemmon-Scott / Sahlqvist
o
Modèles canoniques et complétude
Chap. 5 : Décidabilité par la méthode des filtrations
Chap. 2 : Système K
Langage et Axiomatique
o
Langage : LP + £ (+
¯ : optionnel, car ¯= Ø£Ø)
Ø£
(p Ù ¯q)
® (£p
Ú£q)
o
Axiomatique :
ØToutes les tautologies de LP et
MP (|-- A®B et |-- A Þ |-- B)
Ø(Schéma d’)Axiome K : £ (A ®
B) ® (£A
® £B)
ØRègle de Nécessitation : |-- A Þ |-- £A
Chap. 1 : Système K
Langage et Axiomatique
o
Un théorème de K est une formule qu’on peut obtenir par
les axiomes et RI ci-dessus. Notation : |--K A si A est un
théorème.
o
L’ensemble des théorèmes du système K est noté Th(K).
o
Une règle d’inférence dérivée est une règle de la
forme :
|--K
A1, …, |--K An Þ |--K A t.q. si A1,…,AnÎTh(K) alors
AÎTh(K)
ØEx : Règle d’inférence
dérivée (RM) : |-- A®B Þ |-- £A®£B
1. |-- A®B Hypothèse
2. |-- £ (A®B)® (£A®£B) Ax. K
3. |-- A®B Þ |-- £ (A®B) Nec. 1
4. |-- £A®£B MP
sur 2 et 3
ØEx : Règle d’inférence
dérivée (RM’) : |-- A®B Þ |-- ¯A®¯B
Chap. 1 : Système K
Langage et Axiomatique
ØEx : Théorème : |-- £(AÙB)
® (£AÙ£B)
1. |-- (AÙB)®A LP
2. |-- £ (AÙB)® £A RM
sur 1
3. |-- (AÙB)®B LP
4. |-- £ (AÙB)® £B RM
sur 3
5. |-- £(AÙB) ® (£AÙ£B) LP sur 2 et 4
Chap. 1 : Système K
Langage et Axiomatique
ØEx : Théorème : |-- (£AÙ£B) ®
£(AÙB)
1. |-- (AÙB)® (AÙB) LP
2. |-- A®(B® (AÙB)) LP
sur 1
3. |-- £ (A®(B® (AÙB))) Nec
sur 2
4. |-- £ (A®(B® (AÙB))) ® (£A® £(B® (AÙB))) Ax.
K
5. |-- £A® £(B® (AÙB)) MP
sur 3 et 4
6. |-- £(B® (AÙB)) ® (£B ® £(AÙB)) Ax.
K
7. |-- £A® (£B ® £(AÙB)) LP
sur 5 et 6
8. |-- (£AÙ£B) ® £(AÙB) LP sur
7
Chap. 1 : Système K :
Sémantique (de Kripke)
o
A partir d’une situation donnée (un monde possible, un état de
fait), d’autres situations sont envisageables.
o
A partir de ces dernières, d’autres sont envisageables, …
o
D’où le fait qu’un modèle soit un graphe
o
Mais ce modèle n’est qu’un modèle possible…
Chap. 1 : Système K
Sémantique (de Kripke)
o
Cadre : C = (W, R) où
ØW est un ensemble non vide (de
mondes possibles)
ØR est une relation binaire
(dite d’accessibilité)
ØC est un graphe (éventuellement
infini)
o
Modèle : M = (C,m) où
ØC est un cadre
Øm est une fonction (m: PROP
--> 2W)
ØM = (W,R,m) repose sur C
ØM est un système de
transition (graphe + labels)
Chap. 1 : Système K
Sémantique (de Kripke)
o
Soit A une formule, A est satisfaite par le monde possible
x du modèle M=(W,R,m) (noté M,x |== A) ssi :
ØM,x |== p ssi x
appartient à m(p)
ØM,x |== B Ù C ssi M,x |== B et M,x |== C
ØM,x |== ØB ssi non (M,x |== B)
ØM,x |== £B ssi "yÎW: R(x,y) Þ
M,y |== B
ØNB : M,x |== ¯ B ssi $y : R(x,v) & M,y |== B
NB : Soient x et y
éléments de W
* L’ensemble des
R-successeurs de x, noté R(x), est {yÎW : R(x,y)}
* On notera
indifféremment : xRy / R(x,y) / yÎR(x)
*
R(x) = Æ ssi M,x |== £^ et R(x) ¹ Æ ssi M,x |==
¯T
Chap. 1 : Système K
Sémantique (de Kripke)
o
C = (W,R)
Chap. 1 : Système K
Sémantique (de Kripke)
o
M = (W,R,m)
m(p) = {w1,w2,w3}
m(q) = {w2,w3,w4}
|
|
Chap. 1 : Système K
Sémantique (de Kripke)
o
M = (W,R,m)
|
|
|
|
|
|
|
|
M,w1 |== ¯q
M,w1 |== ¯p
M,w1 |== ¯Øp
M,w1 |== ¯(pÙq)
M,w1 |== أp
M,w1 |== £q
M,w8 |== £p
M,w8 |== دp
M,w1 |== £(q
Ù¯Øp)
|
|
|
Chap. 1 : Système K
Sémantique (de Kripke)
o
Soit A une formule, C=(W,R) un cadre et M=(C,m) un modèle :
o
A est satisfaite par M (noté M sat A) ssi $xÎW :
M,x |== A
o
A est satisfaite par C (noté C sat A) ssi $m : $xÎW : M,x |== A
o
A est vraie dans M (noté M |== A) ssi A est
satisfaite dans tout monde du modèle M, i.e. "xÎW : M,x |== A
o
A est vraie dans C (noté C |== A) ssi A est vraie
dans tout modèle M basé sur C i.e. "m :
"xÎW :
M,x |== A
o
A est K-valide (noté |==K A) ssi A est
satisfaite en tout monde de tout K-modèle
o
L’ensemble des formules K-valides est noté Valid(K)
Chap. 1 : Système K
Caractérisation sémantique
o
Théorème d’adéquation : Th(K) Í Valid(K).
o
Théorème de complétude : Valid(K) Í Th(K)
o
On dit que K est caractérisé par la classe des K-modèles
Fin Cours 1
Chap. 3 : Les axiomes D, T, B, 4, 5
Lecture des axiomes
o
Schémas d’axiome :
§ D : £A®¯A
· S’il est
obligatoire que A, c’est que A est permis
· Si
dorénavant A, alors un de ces jours A
· Si
partout A, alors quelque part A
· Si
partout ailleurs A, alors quelque part ailleurs A
Chap. 3 : Les axiomes D, T, B, 4, 5
Lecture des axiomes
§ T : £A®A
· Si je
sais que A, c’est que A est vrai
· Si je
crois que A, c’est que A est vrai
· S’il est
obligatoire que A, c’est que A est vrai
· Si
dorénavant A, alors A maintenant
· Si
partout A, alors ici A
· Si partout
ailleurs A, alors ici A
· Si après a on a A, c’est qu’on a A maintenant
Chap. 3 : Les axiomes D, T, B, 4, 5
Lecture des axiomes
§ 4 : £A®££A
· Si je
sais que A, je sais que je le sais
· Si je
crois que A, je crois que je le crois
· L’obligation
de A est elle-même obligatoire
· Si
dorénavant A, alors dorénavant : dorénavant A
· Si A est
vraie partout, alors partout il est vrai que partout A
· Si
partout ailleurs A, alors partout ailleurs il est vrai que partout ailleurs A
· Si après a on a A, c’est qu’après a suivie de a
on a A
Chap. 3 : Les axiomes D, T, B, 4, 5
Lecture des axiomes
§ B : ¯£A®A
§ 5 : ¯£A®£A
(contraposée : Ø£A ®
£Ø£A ou ¯A®£¯A)
· Si je ne
suis pas sûr de A, je suis sûr de ne pas être sûr
· Si je ne
crois pas que A, je pense que je ne le crois pas
· La
permission A est elle-même obligatoire
· Si un de
ces jours A, alors dorénavant : un de ces jours A
· Si
quelque part A est vraie partout, alors A est vraie partout
· Si
quelque part ailleurs A, alors partout ailleurs il est vrai que quelque part
ailleurs A
Chap. 3 : Les axiomes D, T, B, 4, 5
Axiomatique
o
On note KD, KDT, KD4, KD45, … les systèmes basés sur K plus les
axiomes D, D et T, D et 4, D, 4 et 5,… Certains ont des noms plus connus (KT4 =
S4, KT5 = S5, KT = T)
o
NB :
§ Th(KDT) =
Th(KT), en effet DÎTh(KT) :
1.
|--KT £A®A Ax. T
2.
|--KT A®¯A Contrap. d'Ax. T (en fait
de £ØA®ØA)
3.
|--KT £A®¯A LP
sur 1 et 2
Chap. 3 : Les axiomes D, T, B, 4, 5
Axiomatique
§ Th(KT45)
= Th(KT5), en effet 4ÎTh(KT5) :
1.
|--KT5 ¯¯A®£¯¯A Ax. 5
2.
|--KT5 ¯A®£¯A Ax. 5
3.
|--KT5 ¯¯A®¯£¯A RM’ sur 2
4.
|--KT5 £¯¯A®£¯£¯A RM sur 3
5.
|--KT5 ¯£¯A ®£¯A Ax. 5
6.
|--KT5 £¯£¯A ®££¯A RM sur 5
7.
|--KT5 ££¯A ®£¯A Ax.
T
8.
|--KT5 £¯A ®¯A Ax.
T
9.
|--KT5 ¯¯A ®¯A LP sur 1,4,6,7,8
10. |--KT5 £A ®££A Contrap.
9
Chap. 3 : Les axiomes D, T, B, 4, 5
Sémantique du 2ème ordre
o
Cadre : C = (W, R) et Modèle : M = (C,m) comme pour K
o
La classe M2KT des modèles M tels que
§ (i) "A : "xÎW : M,x |== £A Þ M,x |== A
caractérise KT.
§ On parle
de sémantique du second ordre
o
Remarque : (i) est vraie dès lors que xRx ; qu’en
est-il de la classe M1KT des modèles M tels que
§ "xÎW :
xRx (Þ modèles basés sur un cadre
réflexif)
Chap. 3 : Les axiomes D, T, B, 4, 5
Correspondance
o
En effet, toute formule de la forme £A ®A est vraie
dans tout modèle réflexif. Il est facile de vérifier que tout théorème de KT
est valide dans un modèle réflexif. Mais la réciproque ?
o
La classe M1KT caractérise KT : sémantique du
premier ordre
et M1KT ÍM2KT
o
P. ex. tout modèle basé sur le cadre C ci-dessous et tel que
w1Îm(p) Û w2Îm(p) est un modèle de M2KT.
Néanmoins, T n’est pas vraie
dans C.
Chap. 3 : Les axiomes D, T, B, 4, 5
Correspondance
o
De fait, pour chacun des axiomes X parmi D, T, B, 4, 5, il existe
une propriété P(X) du premier ordre telle que X est vraie dans tout cadre
vérifiant P(X) :
§ D :
sérialité ("x$y : xRy)
§ T :
réflexivité ("x : xRx)
§ 4 :
transitivité ("x,y,z :(xRy
& yRz) Þ xRz))
§ B :
symétrie ("x,y : xRy Þ yRx)
§ 5 :
euclidéanité : ("x,y,z :
(xRy & xRz) Þ yRz))
Il est assez facile de vérifier que correspondance Þ adéquation
MAIS il n’existe aucun résultat général assurant que correspondance Þ complétude (aucun contre-exemple pourtant)
Chap. 4 : Systèmes basés sur les axiomes G(k,l,m,n)
Correspondance
o On
dénote une suite de n connecteurs ¯
(resp. £) par ¯n (resp. £n)
o Le
schéma G(k,l,m,n) est le schéma :
§ ¯k £l p ®
£m ¯n p dont D, T, B, 4 et 5
sont des cas particuliers.
o Ce
schéma correspond à la propriété :
§ (R-1)k
o Rm Í Rl o
(R-1)n notée R(k,l,m,n)
où o et -1 sont la
composition et l’inverse des relations :
· yÎ R-1(x) ssi xÎ R(y) ; R0 = D et D
o S = S o D = S
· yÎRoS(x) ssi $z :
zÎR(x) & yÎS(z)
o Exemple :
5 = G(1,0,1,1) correspond à la propriété R-1 o R Í R
o Exemple
T = G(0,1,0,0) correspond à D Í R
Chap. 4 : Systèmes basés sur les axiomes G(k,l,m,n)
Correspondance
o
(R
-1)
k o R
m Í
R
l o (R
-1)
n graphiquement :
o Exemple :
5 = G(1,0,1,1) correspond à la propriété R-1 o R Í R
o Exemple :
T = G(0,1,0,0) correspond à D Í Rl
Chap. 4 : Systèmes basés sur les axiomes G(k,l,m,n)
Théorème (Lemmon-Scott / Sahlqvist) :
Soit S un système modal basé sur K
plus des axiomes de la famille G(k,l,m,n), la classe C1S des cadres
vérifiant R(k,l,m,n) pour chaque axiome G(k,l,m,n) du système caractérise S.
Þ
Th(S) = Valid(C1S).
o NB :
le théorème de Sahlqvist est beaucoup plus général.
Þ
Th(KT45) = Th(KT5) ssi Valid(C1KT45) = Valid(C1KT5),
or C1KT45
= classe des cadres réflexifs, transitifs et euclidiens
et C1KT5 = classe
des cadres réflexifs et euclidiens ;
or un cadre réflexif et
euclidien est transitif. QED.
Chap. 4 : Systèmes basés sur les axiomes G(k,l,m,n)
Modèle canonique et complétude
Soit S un système basé sur K
plus des axiomes G(k,l,m,n).
Dans ce qui suit, E dénote
un ensemble de formules.
On assimilera un ensemble
fini avec la conjonction de ses formules.
On note E |-- S
A ssi il existe une partie finie EF de E telle que |--S EF ® E
E est S-consistant
ssi pour tout A, on n’a pas E |--S A et E |--S ØA
E est S-maximal ssi
pour tout A du langage de S, on a AÎE ou ØAÎE
E est S-MaxC (S-maximal-consistant)
ssi il est S-maximal et S-consistant
Propriétés des ensembles S-MaxC :
E|--
S A ssi AÎE
Si
A®B
et AÎE, alors BÎE
(AÚB)ÎE ssi AÎE ou BÎE
…
Chap. 4 : Systèmes basés sur les axiomes G(k,l,m,n)
Modèle canonique et complétude
Lemme de Lindenbaum : Tout ensemble S-consistant peut être étendu à
un ensemble S-MaxC , i.e. E est S-consistant Þ il existe F
ensemble S-MaxC t.q. EÍF. Preuve par énumération des formules
n’appartenant pas à E.
Le modèle canonique M=(W,R,m)
pour le système S est défini comme suit :
· W = {x / x est un ensemble S-MaxC}
· R = {(x,y) / £-1(x)Íy} ; où £-j(x) dénote l’ensemble {A / £j A Î
x }
· m : m(p) = {x / pÎx}
Chap. 4 : Systèmes basés sur les axiomes G(k,l,m,n)
Modèle canonique et complétude
Lemme
de composition : x R n
y ssi £-n(x)Íy
Lemme fondamental : pour toute formule A et tout x S-MaxC : AÎx Û M,x|==A. Preuve
par induction sur la structure de A.
Lemme structurel : le cadre du modèle canonique est dans C1S
Preuve : soient x,y,z tels que xRky et xRmz,
il faut vérifier que l’ensemble
u0
= £-l(y)È£-n(z)
est S-consistant, donc il existe un S-MaxC u Ê u0 tel que yRlu et
zRnu
Chap. 4 : Systèmes basés sur les axiomes G(k,l,m,n)
Modèle canonique et complétude
Théorème de complétude : si A est S-consistante alors A est C1S-satisfiable
(elle est satisfaite par M d’ailleurs).
Preuve : A S-consistante Þ il existe x
S-MaxC t.q. AÎx Þ M,x|==A
Corollaire : si A est C1S-insatisfiable, elle
est S-contradictoire, ou ce qui revient au même, A ÎValid(C1S)
Þ
AÎTh(S)
Théorème d’adéquation : Il suffit de vérifier que les axiomes de S sont C1S-valides
et que les règles d’inférence (MP et Nec) préservent la C1S-validité.
Chap. 5 : Décidabilité par la méthode de filtration
Définitions :
o
Filtration : Idée, le fait que M,x |== A n’est lié qu’à la
valeur de vérité des sous-formules de A (SF(A)) dans les mondes de M.
o
Etant donné M=(W,R,m) et une formule A, on définit pour x,yÎW :
§ x»Ay Û
pour toute sous-formule B de A : M,x|== B ssi M,y|== B
§ c’est une
relation d’équivalence sur W.
§ Soit W/A
le quotient (il est fini) et |x| la classe d’équivalence de x
o
Une filtration de M par A est un modèle M*=(W*,R*,m*) tel
que :
(i)
W* = W/A
(ii)
m*(p) = (m(p)) /A
(iii)
"x,yÎW : x R y Þ |x| R*
|y|
(iv)
|x| R* |y| et £BÎSF(A) : M,x|==£B Þ M,y|==B
Chap. 5 : Décidabilité par la méthode de filtration
Théorèmes :
o
Théorème fondamental des filtrations : Soit M un modèle et
A une formule, soit M* une filtration de M par A, alors :
Ø Si BÎSF(A) alors M,x |== B Û
M,|x| |== B
o
Preuve par induction sur B
o
Problème : Soit S un système, A une formule et M un modèle
basé sur un cadre de C1S : M* est-il membre de C1S ?
Si oui, on en conclura que S est caractérisé par la classe CfS des
cadres finis de C1S.
o
Pas de résultat général, il faut traiter les systèmes un par un.
Chap. 5 : Décidabilité par la méthode de filtration
Exemples, décidabilité et contre-exemple :
o
Exemple 1 : système K. C1K = cadres qqx, Valid(C1K)=Valid(CfK)
o
Exemple 2 : système KT. On a C1KT = classe des
cadres réflexifs, il suffit de vérifier que la filtration d’un modèle réflexif
est réflexive.
o
Exemple 3 : système KT4 (S4). C1S4 = transitifs,
il suffit de trouver une filtration d’un modèle transitif qui soit transitive
(Prendre |x|R*|y| ssi M,|x| |==£B Þ
M,|y| |==B et montrer iii et iv)
o
Décidabilité :
§ Modèle filtré
fini + axiomatisation finie : décidabilité
§ Modèle filtré
borné : décidabilité (|W|£2|SF(A)|
et |x|£|SF(A)|)
o
KD4.De (Densité = ¯A®¯¯A)
pourtant décidable et avec p.m.f.
§ Echec de
la méthode de filtration
Chap. 6 : Déduction automatique : la méthode des tableaux
Présentation informelle : S4-contre-modèle pour ¯£p®¯£¯£p
Chap. 6 : Déduction automatique : la méthode des tableaux
Présentation informelle : K-contre-modèle pour (¯pÚ¯p)®¯(pÚq)
Chap. 6 : Déduction automatique : la méthode des tableaux
Présentation formelle : Définitions
o
Soit X un système, un (RX-)modèle-graphe est une structure G =
(N,S,f) telle que :
§ N est un
ensemble de nœuds
§ S est une
relation binaire sur N
§ f est une fonction : N ® 2FORM
o
Un modèle-graphe est dit fermé si l’un de ses nœuds contient ^
Chap. 6 : Déduction automatique : la méthode des tableaux
Présentation formelle : Définitions
o
Soit E un ensemble de formules, un RX-tableau pour E est une
suite G1, …, Gn,… de modèles-graphes telle que :
§ $n³1 :
Gn est fermé ou Gn=Gn+1
§ G1
est constitué d’un seul nœud associé à l’ensemble E
§ Gn+1
s’obtient depuis Gn en appliquant l’une
des règles de RX
o
Un tableau est fermé si $n³1 : Gn est fermé, il est ouvert
sinon.
o
Une formule est fermée par tableau si tous ses tableaux
sont fermés (voir plus bas), elle est ouverte sinon.
o
Les règles en question permettent la réécriture monotone d’une
partie de modèle-graphe (uniquement ajout de formules dans un ou plusieurs
nœuds et/ou ajout de nœuds et arcs)
Chap. 6 : Déduction automatique : la méthode des tableaux
Présentation formelle : Règles Classiques
(^)
(ØØ)
(Ù)
(Ú)
NB : A cause de la règle Ú, il
y a plusieurs tableaux possibles
Chap. 6 : Déduction automatique : la méthode des tableaux
Présentation formelle : Règles pour K
(¯)
Une seule
application par formule
(K)
Chap. 6 : Déduction automatique : la méthode des tableaux
Présentation formelle : Règles pour D, T, 4
(D)
Sauf si le nœud
a déjà un successeur
(T)
(4)
Chap. 6 : Déduction automatique : la méthode des tableaux
Présentation formelle : Adéquation et complétude
Théorème d’adéquation : Si une formule est K(D,T,4)-fermée par tableau
alors elle est K(D,T,4)-insatisfiable.
Théorème de complétude : Si une formule est K(D,T,4)-ouverte par
tableau (=un de ses K(D,T,4)-tableaux est ouvert) alors elle est K(D,T,4)-satisfiable.
Le tableau ouvert peut être transformé en un K(D,T,4)-modèle.
Exemples :
· (£pÙ£q) ®
£(pÙq) K-valide
· £pÙ£Øq
K-satisfiable
· (£pÚ£(qÚr))®((ØpÚ¯Øp)Ù ¯Øq) KT-satisfiable
Chap. 6 : Déduction automatique : la méthode des tableaux
Présentation formelle : Terminaison
Théorème de terminaison pour K(D,T) : Le calcul des K(D,T)-tableaux
pour une formule termine.
Le calcul des KD4-tableaux pour £((pÚq)Ù¯Øp) est
infini… mais conduit à une répétition.
Solution : le test de boucle
(Loop)
où dénote la relation « ancêtre »
Chap. 6 : Déduction automatique : la méthode des tableaux
Présentation formelle : Stratégies complètes et terminantes
Les règles classiques (^,ØØ,Ú,Ù), et les règles T, D et ¯ ne sont applicables que sur un
nœud non rayé.
Une stratégie est une expression régulière décrivant l’ordre dans
lequel il faut appliquer les règles pour assurer la terminaison du calcul, ou
pour améliorer ses performances.
* :
autant que possible + : union ; : séquence
Stratégie pour K(D,T) : ((Cl + T)* ; (¯+D)* ; K*)*
Stratégie pour K(D,T)4 : ((Cl + T)* ;
(¯+D)* ; (K+4)* ;Loop)*
Avec une stratégie en profondeur, la
complexité de ces systèmes est établie comme étant PSPACE-complète (Ladner 77).
Chap. 7 : Système multi-K (Kn)
Langage et Axiomatique
o
Langage : LP + [i] (+ <i> : optionnel,
car <i>= Ø[i]Ø)
Ø[i] (p Ù <i> q) ® ([i] p Ú [i] q)
o
Axiomatique :
ØToutes les tautologies de LP et
MP (|-- A®B et |-- A Þ |-- B)
Ø(Schéma
d’)Axiome K : [i] (A ® B) ® ([i]A
® [i]B)
ØRègle de Nécessitation : |-- A Þ |-- [i]A
Chap. 7 : Système multi-K
Langage et Axiomatique
o
Un théorème de Kn est une formule qu’on peut
obtenir par les axiomes et RI ci-dessus. Notation : |--K A si A
est un théorème.
o
L’ensemble des théorèmes du système K est noté Th(K).
o
Une règle d’inférence dérivée est une règle de la
forme :
|--K
A1, …, |--K An Þ |--K A t.q. si A1,…,AnÎTh(K) alors
AÎTh(K)
Chap. 7 : Système multi-K
Sémantique (de Kripke)
o
Cadre : C = (W, Â) où Â est une famille {R1,…,Rn}
de relations
ØW est un ensemble non vide (de
mondes possibles)
ØÂ
est une famille {R1,…,Rn} de relations binaires (dite
d’accessibilité)
ØC est un graphe
(éventuellement infini)
o
Modèle : M = (C,m) où
ØC est un cadre
Øm est une fonction (m: PROP
--> 2W)
ØM = (W,Â,m) repose sur C
ØM est un système de transition
(graphe + labels)
Chap. 7 : Système multi-K
Sémantique (de Kripke)
o
Soit A une formule, A est satisfaite par le monde possible
x du modèle M=(W,Â,m) (noté M,x |== A)
ssi :
ØM,x |== p ssi p
appartient à m(x)
ØM,x |== B Ù C ssi M,x |== B et M,x |== C
ØM,x |== ØB ssi non (M,x |== B)
ØM,x |== [i]B ssi "yÎW:
Ri(x,y) Þ M,y |== B
ØNB : M,x |== <i> B ssi
$y : Ri (x,v) & M,y
|== B
o
L’ensemble des formules Kn-valides est noté Valid(Kn)
o
Kn est caractérisé par la classe des Kn-modèles
Chap. 8 : Les axiomes d’interaction
Lecture des axiomes
o
Schémas d’axiome :
§ Inclusion(i,j) :
[i]A®[j]A
· Si i sait
A, alors j le sait aussi
· Si en
tous points de i on a A, alors en tous points de j aussi
§ Permutation(i,a), : [i][a]A®[a][i]A
· Si i croit
qu’après a A est vraie, alors après a, i croira que A
· Si
au-dessus de ce qui est à droite A, alors à droite de ce qui est au-dessus A
§ Confluence(i,j) :
<i>[j]A®[j]<i>A
Chap. 8 : Les axiomes d’interaction
Correspondance
o
De fait, pour chacun des axiomes X parmi Inclusion, Permutation, Confluence,
il existe une propriété P(X) du premier ordre telle que X est vraie dans tout
cadre vérifiant P(X) :
§ Inclusion(i,j) :
"x: x Rj y Þ x Ri z,
ou RjÍRi
§ Permutation(i,j) :
"x,y,z: $u: (x Rj y & y Ri z) Þ (x Ri u & u Rj z)
ou Rj o Ri
Í Ri o Rj
§ Confluence
(i,j) : "x,y,z: $u: (x Rj y & x Ri
z) Þ (y Ri u & z Rj
u)
ou (Rj)-1
o Ri Í Ri o (Rj)
-1
Il est assez facile de vérifier que correspondance Þ adéquation
Chap. 8 : Les axiomes d’interaction
Théorème (Lemmon-Scott / Sahlqvist) :
Soit S un système modal basé sur K
plus des axiomes de la famille G(k,l,m,n), plus des axiomes d’interaction, la
classe C1S des cadres vérifiant R(k,l,m,n) pour les axiomes
G(k,l,m,n) du système et vérifiant les propriétés correspondant aux axiomes
d’interaction de S caractérise S.
Þ
Th(S) = Valid(C1S).
o NB :
le théorème de Sahlqvist est beaucoup plus général.
Ce théorème peut être établi suivant les mêmes principes (modèle canonique)
que dans le cadre mono-modal (Catach 1998).
Chap. 8 : Les axiomes d’interaction : Décidabilité, complexité
De manière générale, la méthode de filtration est inapplicable dans le cas
multimodal où l’indécidabilité n’est d’ailleurs pas rare.
Leur complexité est souvent très élevée quand ils sont décidables.
Ex. de K4xK4 NEXPTIME-dur ? Par codage du pavage du plan par des quadrominos ?
Résolution
Traduction en logique des prédicats