RAPPELS DE LOGIQUE POUR PROLOG
[Link]
Logique des propositions
Logique des prédicats
Unification
LOGIQUE DES PROPOSITIONS
SYNTAXE
¢ On définit :
Les propositions : a, b, c, …
Les constantes : V et F
Les connecteurs :
¢Ù (conjonction)
¢Ú (disjonction)
¢¬ (négation)
¢É (implication)
Licence Lyon1 - UE LIFprolog N. Guin
CONSTRUCTION D’UNE FORMULE
¢ Une proposition est une formule
¢ Si a et b sont des formules, alors ¬a,
aÚb, aÙb, aÉb sont des formules
Licence Lyon1 - UE LIFprolog N. Guin
LOGIQUE DES PROPOSITIONS
SÉMANTIQUE
¢ Les formules sont interprétées dans {V,F}
¢ On définit l’interprétation associée à chaque
connecteur grâce aux tables de vérité
Licence Lyon1 - UE LIFprolog N. Guin
TABLES DE VÉRITÉ DES CONNECTEURS
A B ¬A AÙB AÚB AÉB
V V F V V V
V F F F V F
F V V F V V
F F V F F V
5
Licence Lyon1 - UE LIFprolog N. Guin
PROPRIÉTÉS DES FORMULES
¢ Une formule est valide si elle est toujours vraie
(quelque soit l’interprétation)
¢ Une formule est consistante s’il existe une
interprétation dans laquelle elle est vraie. Elle est
inconsistante dans le cas contraire
¢ Problème : étant donnée une formule, est-elle
valide ? consistante ?
¢ Exemple : que dire de la formule
(aÉb) É(¬bɬa)
Licence Lyon1 - UE LIFprolog N. Guin
DRESSONS LA TABLE DE VÉRITÉ
a b aÉb ¬b ¬a ¬bɬa (aÉb)É(¬bɬa)
V V V F F V V
V F F V F F V
F V V F V V V
F F V V V V V
Licence Lyon1 - UE LIFprolog N. Guin
RÈGLES DE TRANSFORMATION (1)
¢ aÚ¬a (loi du tiers exclu)
¢ ((aÉb) Ùa) É b (modus ponens)
¢ ((aÉb) Ù¬b) É ¬a (modus tollens)
¢ (aÉb) Û (¬b É ¬a) (contraposition)
¢ ¬¬a Û a (double négation)
¢ aÉb Û ¬a Ú b
¢ aÚa Û aÙa Û a (idempotence)
Licence Lyon1 - UE LIFprolog N. Guin
RÈGLES DE TRANSFORMATION (2)
¢ Lois de De Morgan :
• ¬(aÚb) Û ¬a Ù ¬b
• ¬(aÙb) Û ¬a Ú ¬b
¢ Commutativité et associativité de Ú et Ù
¢ Distributivité de Ú par rapport à Ù et de Ù par
rapport à Ú
¢ XÙ(XÚY) = X, XÚ(XÙY) = X (absorption)
¢ XÚ(¬XÙY) = XÚY
Licence Lyon1 - UE LIFprolog N. Guin
UNE ÉNIGME POLICIÈRE
¢ Un meurtre a été commis au laboratoire, le
corps se trouve dans la salle de conférences…
¢ On dispose des informations suivantes :
La secrétaire déclare qu’elle a vu l’ingénieur dans le
couloir qui donne sur la salle de conférences
Le coup de feu a été tiré dans la salle de
conférences, on l’a donc entendu de toutes les
pièces voisines
L’ingénieur affirme n’avoir rien entendu
¢ On souhaite démontrer que :
si la secrétaire dit vrai, alors l’ingénieur ment
10
Licence Lyon1 - UE LIFprolog N. Guin
FORMALISATION EN CALCUL DES PROPOSITIONS
¢p : la secrétaire dit vrai
¢ q : l’ingénieur était dans le couloir au moment du
crime
¢ r : l’ingénieur était dans une pièce voisine de la
salle de conférences
¢ s : l’ingénieur a entendu le coup de feu
¢ t : l’ingénieur dit vrai
11
Licence Lyon1 - UE LIFprolog N. Guin
RÉSOLUTION DE L’ÉNIGME
¢ Les informations de l’énoncé se traduisent par
les implications :
pÉq, qÉr, rÉs, tɬs
¢ Il s’agit de prouver la validité de la formule :
(pÉq Ù qÉr Ù rÉs Ù tɬs) É (pɬt)
12
Licence Lyon1 - UE LIFprolog N. Guin
DÉMONSTRATION
(pÉq Ù qÉr Ù rÉs Ù tɬs) É (pɬt)
¢ La formule ne peut être fausse que si
• (pɬt) est faux, soit p et t vrais
• la prémisse est vraie, soit toutes les implications vraies
¢ Comme t doit être vrai, s doit être faux, donc r
faux, donc q faux, donc p faux, et il y a
contradiction
13
Licence Lyon1 - UE LIFprolog N. Guin
LOGIQUE DES PRÉDICATS
SYNTAXE
¢ On définit :
Les constantes : V et F
Les connecteurs : Ù Ú ¬ É
Les variables : x, y, z, …
Les fonctions : f, g, h, …
Les prédicats : p, q, r, … dont ceux d’arité 0 : a, b, c, …
Les quantificateurs : ", $
14
Licence Lyon1 - UE LIFprolog N. Guin
DÉFINITIONS
¢ Terme :
Une variable est un terme
Une constante est un terme
Si t1, t2, …, tn sont des termes,
alors f(t1,t2,…,tn) est un terme
Exemple : fils(x)
¢ Atome :
Si t1, t2, …, tn sont des termes, et p un prédicat,
alors p(t1,t2,…,tn) est un atome
Exemple : pere(x,y)
15
Licence Lyon1 - UE LIFprolog N. Guin
CONSTRUCTION D’UNE FORMULE
¢ V, F sont des formules
¢ Un atome est une formule
¢ Si F1 et F2 sont les formules, alors ¬F1, F1ÙF2,
F1ÚF2, F1ÉF2 sont des formules
¢ Si F est une formule, "x F et $x F sont des
formule
¢ Exemples :
"x pere(x,fils(x))
"x "y "z (pere(x,y)Ùpere(y,z)) É papy(x,z)
¢ Remarque : la logique des propositions est un
cas particulier de la logique des prédicats
16
Licence Lyon1 - UE LIFprolog N. Guin
EXEMPLES DE FORMULES VALIDES
¢ "x¬A Û ¬ $xA
¢ "xA Û¬ $x¬A
¢ Comment déterminer qu’une formule
est valide ?
17
Licence Lyon1 - UE LIFprolog N. Guin
DÉFINITIONS
¢ Littéral
Un atome est un littéral (positif)
La négation d’un atome est un littéral (négatif)
¢ Une clause est une formule qui a la forme d’une
disjonction de littéraux
Exemple : P(x,y) Ú ¬Q(z)
¢ Une clause concrète est une clause sans
variable
¢ Une clause de Horn est une clause comportant
au plus un littéral positif
On peut toujours transformer une formule en un
ensemble (conjonction) de clauses
18
Licence Lyon1 - UE LIFprolog N. Guin
PRINCIPE DE RÉSOLUTION
¢ C’est une règle d’inférence qui s’applique aux
clauses
¢ Principe sur des clauses concrètes :
• G = G1ÚG2Ú…ÚGn
• H = ¬G1ÚH2Ú…ÚHm
• K = G2Ú…ÚGn Ú H2Ú…ÚHm
¢K est le résolvant de G et H, on peut l’ajouter à la
conjonction de clauses
¢ G1 et ¬G1 sont des littéraux complémentaires
19
Licence Lyon1 - UE LIFprolog N. Guin
JUSTIFICATION
(PÚA)Ù(¬PÚB)
= (PÙB)Ú(AÙ¬P) Ú(AÙB)
(PÚA)Ù(¬PÚB) Ù(AÚB)
= ((PÙB)Ú(AÙ¬P) Ú(AÙB))Ù(AÚB)
= (AÙPÙB)Ú(AÙ¬P)Ú(AÙB)Ú(PÙB)Ú(AÙ¬PÙB)Ú(AÙB)
= (AÙB) Ú(AÙ¬P) Ú(PÙB)
20
Licence Lyon1 - UE LIFprolog N. Guin
CAS PARTICULIERS
¢P et ¬PÚQ se résolvent en Q (modus ponens)
¢ ¬GÚH et ¬HÚK se résolvent en ¬GÚK
(enchaînement)
¢ ¬Q et ¬PÚQ se résolvent en ¬P (modus tollens)
21
Licence Lyon1 - UE LIFprolog N. Guin
UTILISATION
¢ Le principe de résolution est une règle
d’inférence saine, i.e. tout résolvant est une
conséquence logique des deux clauses parentes
¢ Pour appliquer le principe de résolution à des
clauses non concrètes, on définit l’unification,
afin de rechercher des littéraux complémentaires
22
Licence Lyon1 - UE LIFprolog N. Guin
UNIFICATION
¢ Deux termes t1 et t2 sont unifiables s’il existe une
substitution s des variables de t1 et t2 telle que
s t1 = s t2
¢ Exemples :
• pere(X,jean) s’unifie avec pere(Y,Z)
si X|Y et jean|Z
• pere(jean,mere(X)) s’unifie avec pere(Y,mere(pierre))
si jean|Y et X|pierre
23
Licence Lyon1 - UE LIFprolog N. Guin
RÉFUTATION PAR RÉSOLUTION
¢ Pour prouver que H est une conséquence
logique de G :
On transforme G et H en ensemble de clauses
On applique le principe de résolution à
GÙ¬H jusqu’à trouver la clause vide (faux)
¢ Ce principe est complet pour les clauses de Horn
(Prolog)
24
Licence Lyon1 - UE LIFprolog N. Guin
