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)

 

w4

 

Chap. 1 : Système K

Sémantique (de Kripke)

o 

w2

p,q

 
M = (W,R,m)

m(p) = {w1,w2,w3}

m(q) = {w2,w3,w4}

 

w3

p,q

 

Chap. 1 : Système K

Sémantique (de Kripke)

o  M = (W,R,m)

w2

p,q

 

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 Í

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      

k

 

m

 

n

 

l

 

(R-1)k o Rm Í Rl 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)

Tableau 1

 

Tableau 2

 

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

 

Zone de Texte: AZone de Texte: S, ¯AZone de Texte: ÞZone de Texte: S, ¯A

(¯)

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

Þ

 

S

 

S

 

Æ

 
 


(D)

Sauf si le nœud

a déjà un successeur

 

Þ

 

S, £A

 

S, £A,A

 
 


(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

Þ

 

S

 

S’ÍS

 

S

 
 


(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