Logique math ematique
Le calcul propositionnel ou CPO
I. MOUAKHER-ABDELMOULA
2014-2015
Objectifs
La logique joue un r ole fondamental en informatique dans la
sp ecication, construction et v erication des programmes, comme
langage de programmation, dans son lien etroit avec la calculabilit e. Elle
joue aussi un r ole cl e en intelligence articielle, dans les bases de
donn ees, en probabilit es, etc. Lobjectif du cours est de donner les bases
pour son utilisation dans les di erents domaines, en mettant laccent sur
sa m ecanisation.
Plan
1
introduction
2 Syntaxique
3 Formalisation dun probl`eme
4 S emantique
5 Formes normales
6 Principe de r esolution
Calcul propositionnel
Comment ecrire les formules ?
Aspects syntaxiques
Comment d eterminer la valeur de v erit e dune formule ?
Aspects s emantiques
Comment d emontrer de nouveaux r esultats ?
Aspects d eductifs
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Langage
Formules bien form ees
Langage de la logique des propositions
D enition
Le langage L du CP0 est compos e :
des symboles propositionnels (nots usuellement en lettre minuscules
p, q, r) parmi lesquels on distingue deux symboles particuliers V et F
des connecteurs logiques :
(n egation)
' (conjonction)
( (disjonction)
(implication)
( equivalence)
des des symboles auxiliaires : (, )
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(5/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Langage
Formules bien form ees
Formules bien form ees (fbf)
D enition
Nous appellerons atomes ou variables propositionnelles ou propositions
el ementaires des enonc es dont nous ne connaissons pas la structure
interne, et qui gardent leur identit e tout au long du calcul propositionnel
qui nous occupe. Lensemble des variables propositionnelles est not e
v (L).
D enition
Nous denoterons les formules (ou formules bien form ees fbf ) par des
lettres majuscules de lalphabet latin ou grecque (A, B, ...ou , ).
Lensemble des formules, note F (L), est deni par :
les atomes sont des formules (v (L) F (L)) ;
si et sont des formules, alors ( ), ( ), ( ' ),
( ( ) et ( ) sont des formules.
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(6/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Langage
Formules bien form ees
Utilisation des parenth`eses
Les parenth`eses sont un moyen de lever lambigu 1t e.
En absence de parentheses, les connecteurs sont class es de la facon
suivante (par priorite decroissante des connecteurs) : , ', (, ,
Exemple
p q r doit se lire ((p q) ( r ))
Deux connecteurs ont meme priorite, et en absence de parentheses,
lassociativite se fait de gauche a droite.
Exemple
p q r doit se lire ((p q) r )
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(7/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Formalisation dun probl`eme
Reglement dun club On donne le reglement dun club suivant :
1 Les membres de la direction nanci`ere sont choisis dans les membres
de la direction g en erale
2 Nul ne peut etre `a la fois membre de la direction g en erale et de la
direction de la biblioth`eque, sil nest pas membre de la direction
nanci`ere
3 Aucun membre de la direction de la biblioth`eque ne peut etre
membre de la direction nanci`ere.
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(8/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Symbolisation
f a etre membre de la direction nanci`ere
g a etre membre de la direction g en erale
b a etre membre de la direction de la biblioth`eque
1
2
f g
(g ' b) f
3 b f
Il faut que 1 et 2 et 3 soient vraies : (f g ) ' ((g ' b) f ) ' (b f )
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(9/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
D enitions
D enition
On appelle valuation dun ensemble de variables propositionnelles
v v (L), une fonction m : v (L) {V , F }
D enition
Une interpr etation dune formule dans laquelle apparaissent les variables
propositionnelles v1, ..., vn est une valuation de {v1, ..., vn}.
D enition
Une interpr etation I est un mod`ele dune formule si elle est vrai.
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(10/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
Tables de v erit e des connecteurs (1/3)
On d enit linterpr etation associ ee `a chaque connecteur gr ace aux
tables de v erit e
N egation : p
p p
0
1
1
0
Conjonction : p ' q
p
1
1
0
0
q
Publicité
1
0
1
0
p ' q
1
0
0
0
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(11/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
Tables de v erit e des connecteurs(2/3)
Disjonction : p ( q
p
1
1
0
0
q
1
0
1
0
p ( q
1
1
1
0
Implication : p q
p
1
1
0
0
q
1
0
1
0
p q
1
0
1
1
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(12/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
Tables de v erit e des connecteurs(3/3)
Equivalence : p q
p
1
1
0
0
q
1
0
1
0
p q
1
0
0
1
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(13/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
Exemple : a (p ' q) (r ( s)) (24 entr ees)
p
0
0
0
0
0
0
0
0
1
1
1
1
1
1
1
1
q
0
0
0
0
1
1
1
1
0
0
0
0
1
1
1
1
r
0
0
1
1
0
0
1
1
0
0
1
1
0
0
1
1
s
0
1
0
1
0
1
0
1
0
1
0
1
0
1
0
1
s
1
0
1
0
1
0
1
0
1
0
1
0
Publicité
1
0
1
0
p ' q
0
0
0
0
0
0
0
0
0
0
0
0
1
1
1
1
r s
1
1
1
1
1
1
1
1
1
1
1
1
0
1
1
0
0
1
1
0
0
1
1
0
0
1
1
0
0
1
1
0
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(14/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
Tautologie ou formule valide
D enition
Une formule valide, ou tautologie, est une formule vraie quelles que
soient les valeurs de v erit e des atomes qui la composent (i.e. vraie dans
toute interpr etation). On la note |=
Exemple : p ( p
p p
0
1
1
0
p ( p
1
1
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(15/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
Formule insatisable
D enition
Une formule insatisable, ou s emantiquement inconsistante, ou encore
antitautologie, est une formule fausse dans toute interpr etation.
Exemple : p ( p
p p
0
1
1
0
p ' p
0
0
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(16/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
Formules satisables
D enition
Une formule satisable ou s emantiquement consistante est une formule
vraie dans au moins une interpr etation.
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(17/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
Cons equence logique
D enition
Une formule est une cons equence logique dun ensemble de formules
{ 1, 2, ..., n} not e { 1, 2, ..., n} |= ssi toute interpretation I qui
est vrai pour chaque 1, est vrai pour
Th eor`eme
{ 1, 2, ..., n} |= ssi 1 ' 2 ' ... ' n est valide
Th eor`eme
{ 1, 2, ..., n} |= ssi 1 ' 2 ' ... ' n ' est insatisable
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(18/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
Equivalence des formules bien form ees
D enition
Deux formules sont equivalentes quand elles ont meme valeur dans toutes
interpretation. On note A a B).
une formule est equivalente `a une formule , not e a si la
formule est valide.
En interpr etant la relation a comme une egalit e, on peut consid erer
les connecteurs logiques comme des op erateurs sur lensemble des
fbf.
Il est souvent n ecessaire de transformer une formule en une autre
equivalente. Certaines formes, appel ees formes normales, sont
particuli`erement int eressantes.
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(19/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Publicité
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
Equivalence des formules bien form ees
D enition
On note p la formule obtenue en substituant dans la formule (fbf)
toutes les occurrences du symbole propositionnel p par la fbf .
Th eor`eme
Soit la formule contenant les atomes p1, p2, ..., pn. Soit la formule (cid:48)
obtenue en substituant aux atomes p1, p2, ..., pn les formules
1, 2, ..., n. Alors si |= , on a |= (cid:48).
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(20/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
R`egles de transformation (1/2)
Deux formules particuli`eres not ees par
(cid:62) formule toujours valide
formule toujours fausse.
Implication
a ( ) ' ( )
a (
( ) a '
Idempotence
( a
' a
Commutativit e
( a (
' a '
Associativit e
( ( ) ( a ( ( ( )
( ' ) ' a ' ( ' )
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(21/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Interpr etation
Tables de v erit e
Tautologie, insatisable et satisable
Cons equence logique
Equivalence des formules bien form ees
R`egles de transformation (2/2)
Distributivit e
( ( ' ) a ( ( ) ' ( ( )
' ( ( ) a ( ' ) ( ( ' )
Lois de de Morgan
( ' ) a (
( ( ) a '
El ement neutre
( a
' (cid:62) a
( (cid:62) a (cid:62)
' a
Compl ementarit e
' a
( a (cid:62)
Involution
a
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(22/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Formes normales conjonctives
Formes normales disjonctives
Algorithme de transformation
Formes normales conjonctives
D enition
(Litt eral) Un litt eral est un atome ou la n egation dun atome.
D enition
(Forme normale conjonctive) Une formule est en forme normale
conjonctive (fnc) ssi elle s ecrit comme une conjonction de disjonctions
de litt eraux. a 1 ' 2 ' ... ' n, n e 1.
a (p ( q ( r ) ' ( p ( q) est fnc.
a p ( (p ( q) ' (p ( r ) nest pas en fnc.
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(23/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Formes normales conjonctives
Formes normales disjonctives
Algorithme de transformation
Formes normales conjonctives
D enition
Une clause est une formule qui a la forme dune disjonction de litt eraux
Exemple : p ( q ( r
D enition
Une clause de Horn est une clause comportant au plus un litt eral positif
Exemple : p ( q, p ( q ( r , q ( r , p
D enition
Une formule sous forme clausale pourra etre repr esent ee par un
ensemble de clauses : = C1 ' ... ' Cn ou = {C1, ..., Cn}
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(24/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Formes normales conjonctives
Formes normales disjonctives
Algorithme de transformation
Formes normales disjonctives
D enition
(Forme normale disjonctive) Une formule est en forme normale
disjonctive (fnd) ssi elle s ecrit comme une disjonction de conjonctions de
litt eraux. a 1 ( 2 ( ... ( n, n e 1.
a ( p ' q) ( (p ' q ' r ) est en fnd.
a (p ' q) ( (p ' q) nest pas en fnd.
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(25/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Formes normales conjonctives
Formes normales disjonctives
Algorithme de transformation
Algorithme de transformation
Etape 1 : Utiliser les lois suivantes pour eliminer les connecteurs logique ,
a ( ) ' ( )
a (
Etape 2 : Ramener les signes de n egation imm ediatement avant les atomes en
utilisant de maniere r ep et ee les regles :
( ) a
les lois de De Morgan
( ' ) a (
( ( ) a '
Etape 3 : Utiliser les lois pour obtenir la forme normale d esir ee
( ( ' ) a ( ( ) ' ( ( )
' ( ( ) a ( ' ) ( ( ' )
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(26/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Formes normales conjonctives
Formes normales disjonctives
Algorithme de transformation
Exemple
p (q r )
1 Remplacer l equivalence :
2 Remplacer les implications :
(p (q r )) ' ((q r ) p)
( p ( ( q ( r )) ' ( ( q ( r ) ( p)
3 Faire traverser a la n egation les parenthese :
Publicité
( p ( q ( r ) ' ((q ' r ) ( p)
4 Appliquer la distributivit e de ( :
5 Regrouper :
( p ( q ( r ) ' ((q ( p) ' ( r ( p))
( p ( q ( r ) ' (q ( p) ' ( r ( p) fnc
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(27/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Syst`eme formel
R`egle de r esolution
R esolution
Syst`eme formel (d eductif)
En logique, on cherche a d emontrer des th eoremes (tautologies) :
la s emantiqure (couteux)
Un moyen m ecanique qui ne travaille que sur la syntaxe des formules
un syst`eme d eductif (ou formel) qui permet donc de m ecaniser le
raisonnement.
Un syst`eme formel de d eduction de la logique classique est compos e :
des axiomes qui repr esentent un petit nombre de v erit es initiales
des r`egles de d eduction (dinf erence) qui sont les m ecanismes de
raisonnement pour r ev eler des v erit es cach ees.
il permet dinf erer des conclusions `a partir de pr emisses et d enit
donc une relation de d eduction entre formules
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(28/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Syst`eme formel
R`egle de r esolution
R esolution
R`egle de r esolution
Le principe de r esolution est form e dune unique r`egle dinf erence.
R`egle de r esolution
avec
c1: (P,c2: P(
c3: (
(RR)
et sont des disjonctions de litt eraux
c3 est dite r esolvante de c1 et c2
P et P sont des litt eraux compl ementaires
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(29/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Syst`eme formel
R`egle de r esolution
R esolution
Exemples
c1:P(R,c2: P(Q
c3:R(Q
(RR)
c1: P(Q(R,c2: S( Q
c3: P(R( S
(RR)
c1 : P ( Q, c2 : P ( R il ny a aucun r esolvant pour c1 et c2.
Remarque
Si on est en pr esence de deux clauses unitaires alors leurs r esolvant sil
existe est la clause vide (cid:3).
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(30/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Syst`eme formel
R`egle de r esolution
R esolution
R esolution
Th eor`eme
Etant donn e deux clauses c1 et c2, un r esolvant c de c1 et c2 est une
cons equence logique de c1 et c2. {c1, c2} |= c
D enition
Soit S un ensemble de clauses, une d eduction (r esolution) de c `a partir
de S est une s equence c1, c2, ..., ck o`u chaque ci est soit une clause de S
soit un r esolvant de clauses pr ec edent ci et c = ck
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(31/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Syst`eme formel
R`egle de r esolution
R esolution
Exemple
{p ( q ( r , p ( r ( q, q ( r } |= r
gr ace `a la d eduction :
c1 : {p ( q ( r
(HYP)
c2 : p ( r ( Q (HYP)
(HYP)
c3 : q ( r
(RR)(c1, c2)
c4 : q ( r
(RR)(c3, c4)
c5 : r
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(32/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Syst`eme formel
R`egle de r esolution
R esolution
R esolution par r efutation
Pour r esoudre un probl`eme de logique par la m ethode de r esolution,
on sappuie sur le th eor`eme de r efutation
Pour prouver que H est une consequence logique de G :
On transforme G et H en ensemble de clauses
On applique le principe de resolution a G ' H jusqu`a trouver la
clause vide
Exemple : {p ( q ( r , p ( r ( q, q ( r } |= r
revient `a monter :
{p ( q ( r , p ( r ( q, q ( r , r } |= (cid:3)
c1 : p ( q ( r
c2 : p ( r ( q
c3 : q ( r
c4 : r
c5 : q ( r
c6 : r
c7 : (cid:3)
(HYP)
(HYP)
(HYP)
(HYP)
(RR)(c1, c2)
(RR)(c3, c5)
(RR)(c4, c6)
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(33/34)
introduction
Syntaxique
Formalisation dun probl`eme
S emantique
Formes normales
Principe de r esolution
Syst`eme formel
R`egle de r esolution
R esolution
Exercice
On suppose que lon a les r`egles et faits suivants :
Si Pierre rate son tournoi alors Pierre sera d eprim e.
Sil fait beau alors Pierre ira `a la piscine.
Si Pierre ne va pas `a la piscine il sera d eprim e.
A la piscine, Pierre ne sentra 1ne pas.
Pierre ratera son tournoi sil ne sentra 1ne pas.
Questions :
1 Mod eliser l enonc e `a laide de formules de la logique propositionnelle.
2 Prouver que Pierre sera d eprim e.
I. MOUAKHER-ABDELMOULA
Le calcul propositionnel ou CPO
(34/34)