Des logiques à la programmation

en logique

P. De Loor – deloor@enib -

1
 Programmer en Logique
• Une définition de l ’I.A. [ALL94] : faire
exécuter par l’ordinateur des tâches pour
lesquelles l ’homme est meilleur que la
machine.
• 3 courants de pensée (voire annexes)
 Approche cognitive (source de la PL)
– Approche pragmatique (utilisation de la PL)
– Approche connexionniste
2
 Plan
• 1. Programmer en logique ?
• 2. Origines des Logiques
• 3. Systèmes formels
• 4. Calcul propositionnel
• 5. Calcul des prédicats
• 6. Logiques non-classique
• 7. Démonstration automatique
• 8. Programmation en logique
3
 Programmer en Logique ?
• Paradigmes de programmation
– mémoire/instruction : impératif
– mathématique : fonctionnelle
– génie logiciel : objet
– raisonnement : logique
– ...
Un programme en PL exprimera des règles (et
des faits) l ’interpréteur « raisonnera » dessus
4
Chapitre 1. Programmer en logique ?
 2. Les origines de la logique

5
Chapitre 2. Les origines de la logique
 D ’où viennent les logiques
• Origines philosophiques
• Caractériser les raisonnements valides
• Qu’est ce qu’un savoir permet de faire
– classer, trier les « mots clés » du savoir
– trouver des règles de fonctionnement
– utiliser ces règles pour démontrer des
possibilités et impossibilités
– étudier ces règles pour discuter de leur bien-
fondé 6
Chapitre 2. Les origines de la logique
 D ’où viennent les logiques
• Aristote (384-322 avant J.C)
– l ’Organon (instrument (du savoir))
– étude des propriétés des propositions catégoriques

Certains chimpanzés sont des femelles

quantité sujet qualité « prédicat »

– énoncé déclaratif : vrai ou faux 7

Chapitre 2. Les origines de la logique
 D ’où viennent les logiques
• Les quatre propositions catégoriques :

A - L’universelle affirmative : Tout homme est mortel

E - L’universelle négative : Aucun homme n’est mortel
I - La particulière affirmative : Quelque homme est mortel
O - La particulière négative : Quelque homme n’est pas
mortel
Affirmo / nEgO

• 5 propriétés
Chapitre 2. Les origines de la logique
8
 D ’où viennent les logiques
• Exemple de propriété : l ’inférence directe

– Si A est vraie, E est fausse, I est vraie et O est

fausse
– Si O est vrai, on ne sait rien sur E et I

9
 D ’où viennent les logiques
• Exemple de propriété : la contraposition

Tous les lézards sont verts,

donc :
Tout ce qui n ’est pas vert n ’est pas un lézard

10
 D ’où viennent les logiques
• Exemple de propriété : le syllogisme
aucune vulgarisation n ’est aisée
quelques travaux sont des vulgarisations
quelques travaux ne sont pas aisés
(EIO)

– Approche systématique (64 syllogismes)

– prémisses des approches formelles
11
Chapitre 2. Les origines de la logique
 Historique
450 av. J.C - Stoïciens - logique propositionnelle inférence.
322 av. J.C - Aristote - propositions catégoriques, syllogismes (règles d ’inférences)
quantificateurs.

1565 - Cardano - théorie des probabilités (logique des propositions & incertitude)

1666 - Leibniz - logique symbolique contemporaine

1847 - Boole - logique des propositions mise sous la forme d ’algèbre

1879 - Frege - logique du premier ordre

1930 - Gödel - ∃ algorithme complet pour la logique du premier ordre

1930 - Herbrand - algorithme complet pour premier ordre
1931 - Gödel - ¬∃ algorithme complet pour l ’arithmétique
1960 - Davis/Putnam - algorithme utile pour la logique propositionnelle
1965 - Robinson -algorithme « utilisé » pour la logique du premier ordre : principe de résolution

Prolog
CLP,ILP,MOLOG...
12
Chapitre 2. Les origines de la logique
 D ’où viennent les logiques
• Clés de voûte de la logique

– modus ponens
si le premier alors le second
or le premier donc le second
– modus tollens
si le premier alors le second
or pas le second donc pas le premier

13
Chapitre 2. Les origines de la logique
 3. Systèmes formels

14
Chapitre 3. Systèmes formels
 Formaliser
théorie
formaliser

réel système
formel

prédire

fonctionne seul
15
Chapitre 3. Systèmes formels
 Limite de la formalisation
– simplification/abstraction de la réalité

– système formel logique

• formalisation du raisonnement,
• pas du sens

– paradoxe du menteur

– théorème d ’incomplétude
16
Chapitre 3. Systèmes formels
 Système formel
• Un langage formel
– mots clés, règles de grammaire (formule bien formée)
• Un modèle formel
– interprétation ≈ sens (vrai faux ou autres symboles)
– simplification de la réalité (danger !!)
– relié à un concept (propositions, temps ...)
• Un système déductif formel : axiomatique
– permet de faire du « calcul » : Calcul formel
– règles de déductions (axiomes, inférence)
– se suffit à lui même 17
Chapitre 3. Systèmes formels
 Mots clés des formalistes
Langage formel :
syntaxe

Modèle : théorie des

modèles
Interprétation sémantique

Axiomatique : théorie
de la démonstration
concept
Interprétation syntaxique
18
Chapitre 3. Systèmes formels
 Un bon système formel
• Modèle
– cohérent avec le concept que l’on s’est fixé
• Langage
– simplicité: pas d ’ambiguité
– expressivité
• Axiomatique
– cohérente avec le modèle
– minimale : pas de redondance
– exécutable « automatiquement » 19
Chapitre 3. Systèmes formels
 Les liens modèle-axiomatique
complétude

réel modèle axiomatique

adéquation

Notion de vérité {v,f} Notion de preuve :

de validité théorèmes

20
Chapitre 3. Systèmes formels
 Propriétés importantes
– consistance : avec mon langage, je ne peux pas
trouver une chose vraie et fausse à la fois
– décidabilité : mon langage peut il répondre en un
temps fini à une question ?
– complétude : lien modèle-axiomatique, tout ce que
mon modèle considère valide, mon langage peut le
prouver
– adéquation : lien axiomatique-modèle : tout ce que
je peux déduire de mon langage est valide (toujours
vrai dans mon modèle) 21
Chapitre 3. Systèmes formels
 4. Calcul propositionnel

Ou logique d ’ordre 0

22
Chapitre 4. Calcul propositionnel
 Calcul propositionnel
Langage : propositions, connecteurs,
règle d ’équivalence

Modèle : tables de vérité

Axiomatique : 3 axiomes, 1 règle
d ’inférence
Proposition
langage naturel

23
Chapitre 4. Calcul propositionnel
 Calcul propositionnel
• Exemple de cognition :
– S ’il pleut, alors la route est mouillée
– Donc si la route est sèche c’est qu’il ne pleut pas
• Eléments clés :
– propositions : la_route_est_sèche, il_pleut
– négation : sèche ⇔ mouillée, pleut ⇔ ne_pleut_pas
– règle : si alors
– une déduction : donc
• Début de formalisation
– si X alors Y, donc si non Y alors non X 24
Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
le langage
• Les mots :
– propositions dénombrables ou formules
atomiques ou atomes (p, q, r, …)
– opérateurs (connecteurs) :
¬ négation
∧ conjonction
∨ disjonction
→ implication
↔ bi-implication
false contradiction
– ponctuations : ( ) 25
Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
le langage
• Les phrases (formules)
– règles définissant les formules « bien formées »
– exemple :
• si A est une formule atomique alors A est une formule
• FALSE est une formule
• (A v B) est une formule si A et B sont des formules
• …
• énoncé mal formé : (∨ p)q
Récursif !
26
Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
le modèle
• Les propositions peuvent posséder 2 valeurs
) {0,1} ou {t,f} ou {titi, toto} …

• Les opérateurs définissent la valeur d ’une

formule
) table de vérité
) les formalistes appellent ça une Interprétation I

ps : Si I(A) = t (true), on écrit I |= A (satisfiabilité) 27

Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
le modèle
• Interprétation des connecteurs dyadiques
AB (A↔B) (A→B) (A∧B) (A∨B)
t t t t t t
t f f f f t
f t f t f t
f f t t f f

• négation A ¬A
t f
f t
28
Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
le modèle
• Exemple d'interprétation
– propositions = {p1, p2, ...}.
– interprétation I : I(p1) = v, I(p2), = I(p3) = ... = f

I(p1 v p2) = v
I((p1 ∧ p2) → (p1 ∧ p1)) = v
I(p1 ∧ (p2 v ¬p1)) = f
29
Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
le modèle
• tautologie ou formule valide
formule toujours vraie quelle que soit
l ’interprétation (on note | A)
• exemple
p → (q → p)

• formules satisfiables : au moins une

interprétation vraie.
30
Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
l ’axiomatique
• Purement syntaxique

« vérité » non discutable mécanismes déductifs

Axiomes règles d ’inférence

Nouvelles formules valides : théorèmes

technique copier/coller
substitution
31
Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
l ’axiomatique
• Les Axiomes
1) A → (B → A)
2) (A → (B → C)) → ((A →B) →(A →C))
3) (¬B → ¬A) →(A →B)

• remarque : les connecteurs (∧,∨,↔) ne sont

que des synonymes
– exemple (A∧B) est synonyme de ¬(A → ¬B)
32
Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
l ’axiomatique
• Règle d ’inférence
– modus-ponens
si A est « vraie » et si A implique B alors B est « vraie »

A, A→B prémisses

B conclusion

: Est un théorème (ou un axiome) 33

Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
l ’axiomatique
• La substitution axiome donc tautologie

– exemple
(¬P → ¬Q) →(Q →P)
substitution

a∨b→a

– remplacement d ’une proposition/formule par

une formule, préserve la tautologie
34
Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
l ’axiomatique
• Démonstration :
partant des axiomes, enchaînement de subsitution/inférence
pour déduire des théorèmes (fastidieux, exemple en annexe)

• Déduction :
démonstration à partir d ’hypothèses
supplémentaires (formules)

théorème de Herbrand (1930) : si A|-B alors |-(A→B) 35

Chapitre 4. Calcul propositionnel
 Calcul propositionnel :
propriétés importantes
• Adéquat (si |- A alors |= A)

• Complet (complétude forte : si E |=A alors E|–A )

• Consistant (il n ’existe pas de formule telle que |-A et |- ¬A)

• Décidable
36
Chapitre 4. Calcul propositionnel
 5. Calcul des prédicats

Ou logique du premier ordre

37
Chapitre 5. Calcul des prédicats
 Calcul des prédicats
• Limite des propositions

la_bière_est_blonde

• On aimerait exprimer
estBlonde(X), si X est une Leffe

38
Chapitre 5. Calcul des prédicats
 Calcul des prédicats
• Notion d ’ensemble
– Ensemble complet (pour tout)
– Eléments particuliers d ’un ensemble (il existe)

TOUT être humain est mortel

OR Socrate est un être humain
DONC Socrate est mortel

39
Chapitre 5. Calcul des prédicats
 Calcul des prédicats

• Notion d ’ordres
la_biere_est_blonde ordre 0
est_blonde(X) ordre 1
est_blonde(X(Y)) ordre 2
...

40
Chapitre 5. Calcul des prédicats
 Calcul des prédicats : le langage
• On ajoute au calcul propositionnel
– des constantes : a,b,c,..
– des symboles de fonctions (arité ≥ 0) : f,g,..
– des symboles de prédicats (arite≥0) : p,q,..
– deux quantificateurs : ∃, ∀

les prédicats d ’arité 0 sont des variables propositionnelles

Les arguments des prédicats sont des termes
Les fonctions d ’arité 0 sont des constantes
41
Chapitre 5. Calcul des prédicats
 Calcul des prédicats : le langage
• Terme
– une variable est un terme
– un symbole de constante est un terme
– si f est un symbole de fonction et t1,t2…tn sont
des termes alors f(t1,t2..tn) est un terme
– les termes sont les arguments des prédicats

Récursif !!
42
Chapitre 5. Calcul des prédicats
 Calcul des prédicat : le langage
• Atome
– si p est un symbole de prédicat et t1..tn sont des
termes, alors p(t1,t2..tn) est un atome

– un atome s ’appelle aussi une formule atomique

43
Chapitre 5. Calcul des prédicats
 Calcul des prédicats : le langage
• Formules
– toute formule atomique est une formule
– si A et B sont des formules alors A → B est une
formule
–…
– si A est une formule est si x est une variable
quelconque alors ∃x A est une formule

44
Chapitre 5. Calcul des prédicats
 Calcul des prédicats : le langage
• Variables libres et liées
– exemple, soit la formule
∀x p(x,y)
– x est liée à la formule
– y est libre
– définition complète : quelles sont les variables
libres et liées d ’une formule composée de
formules...
45
Chapitre 5. Calcul des prédicats
 Calcul des prédicats :
axiomatique
• Extension de l ’axiomatique du calcul
propositionnel
• Quelques axiomes en plus
• Règle d ’inférence supplémentaire :
généralisation |- A
|-∀x A
• Démonstration/déduction
– découle du calcul propositionnel
46
Chapitre 5. Calcul des prédicats
 Calcul des prédicats :
le modèle
• Exemple : interprétation du prédicat estBleu(x)
x I(estBleu)(x)
martien f
homme f
schtroumpf t

• Définition formelle -termes-formules : voir

littérature

47
Chapitre 5. Calcul des prédicats
 Calcul des prédicats :
propriétés importantes

• Adéquat
• Complet (Gödel)
• Consistant
• Semi-décidable :
si A est valide alors la procédure s'arrête et retourne `oui'
sinon ou bien la procédure s'arrête et retourne `non', ou bien elle ne
s'arrête pas.
48
Chapitre 5. Calcul des prédicats
 6. Logiques non classiques

49
Chapitre 6. Logiques non classiques
 Logiques non-classiques
• Autres modèles (donc autre langage)
– logiques faibles
• absolue, minimale, positive, intuitionniste
– logiques modales
• aléthique
• temporelle
• déontique, connaissance, croyance
• premier ordre
– logiques multivaluées
• floues 50
Chapitre 6. Logiques non classiques
 Logiques faible
• Question sur la négation
– logique absolue, positive : pas de négation

– logique minimale : ¬ devient « est réfutable »

• p → ¬ ¬p , mais pas l ’inverse

– logique intuitionniste : ¬ devient « est absurde »

51
Chapitre 6. Logiques non classiques
 Logiques modales
• Problème du modèle de la logique classique :
l ’implication matérielle

AB (A↔B) (A→B) (A∧B) (A∨B)

t t t t t t
t f f f f t
f t f t f t
f f t t f f

Si A = f, A→B est vrai (quelque soit B) !!

52
Chapitre 6. Logiques non classiques
 Implication matérielle
et bon sens
• Lien avec le réel :
– La_bière_est_verte... est une proposition fausse : f
• donc la_bière_est_verte implique que 1 + 1 = 3 est vraie.
– Si on décide que « A→B » est faux dès que A = f
alors « → » devient la même chose que « ∧ »
– Or
• si il fait beau j’irais me promener … vraie : t
– donc s’il ne fait pas beau je n’irais pas,
– mais reste vraie

53
Chapitre 6. Logiques non classiques
 Logiques modales
• Nouvelle implication
> : implication stricte possible

A > B =def ¬◊(A∧¬B)

A implique strictement B si il est impossible que A

soit vraie et B faux
• L ’inverse de la possibilité est la nécessité :
nécessaire A =def ¬◊¬ 54
Chapitre 6. Logiques non classiques
 Logiques modales : le modèle
Si ciel_bleu est vrai alors
ciel_bleu ∨ ciel_pas_bleu est vrai
ciel_bleu est faux
(ciel_bleu ∨ ciel_pas_bleu) est vrai

• Table de vérité = impossible

• Le modèle est un graphe représentant une
évolution des propositions (mondes possibles)
55
Chapitre 6. Logiques non classiques
 Logiques temporelles
• Logiques temporelles modales
– le graphe représente l ’évolution dans le temps
• Notions représentées
– avant, après, toujours, parfois (ο,Ρ,U,…)
• Diversité
– temps discrets/continu
– temps linéaire/arborescent
– temps métré/symbolique
56
Chapitre 6. Logiques non classiques
 Autres logiques modales
• Déontique
– O : obligation
– P : permission
– informatique juridique
• Dynamique
– séquence, choix non déterministe, parallélisme

57
Chapitre 6. Logiques non classiques
 Logiques multi-valuées
• Logique multivaluée (Lukasiewicz)
– Poids à la notion de vérité (très vrai, peu probable)
– Valeur de vérité sur un intervalle [0,1]
– Exemple du ∧ : p ∧ q = min (p , q)
• Logique floue (Zadeh)
– Partition dénombrable de sous-intervalles de vérité
– Vrai, faux, pas vrai, pas faux, plus ou moins vrai, plutôt vrai…
– Exemple d ’inférence :
a petit, a et b presque semblables
b est plus ou moins petit
– certains auteurs ne la considèrent pas comme une logique (axiomatique) 58
Chapitre 6. Logiques non classiques
 7. Démonstration automatique

59
Chapitre 7. Démonstration automatique
 Démontrer ...
• Montrer que quelque chose est vrai
• calcul formel = prouver un théorème
• calcul à partir du langage
• définir un ensemble de règles d ’inférences
• définir un ensemble d ’axiomes
• répététivement choisir un règle & des axiomes pour
arriver progressivement au théorème voulu
• Long et difficile (quels règles et axiomes choisir ?)

60
Chapitre 7. Démonstration automatique
 Démonstration automatique

• Déduction en logique propositionnelle

– table de vérité - Wittgenstein - 1922
– arbres sémantiques
– algorithme de Quine efficacité,
simplicité
– algorithme de Davis/Putman
– principe de résolution de Robinson -1965
– clauses de Horn

61
Chapitre 7. Démonstration automatique
 Principe de résolution
– Une seule règle pour montrer qu’une phrase
logique est vraie ou non (simplicité)
– Réduction des formules logiques sous forme
« normale conjonctive »
– Résolution par réfutation (raisonnement par
l ’absurde)
• prendre un système formel
• considérer le contraire du théorème à prouver
• montrer que l ’association des 2 est insatisfiable
ensemble vide
démontrer que {p→r,q →r}|=(p∨q →r)
revient à démontrer {p→r,q →r, ¬(p∨q →r)}|= Ø 62
Chapitre 7. Démonstration automatique
 Principe de résolution
• Forme Normale Conjonctive (FNC)
– que des disjonctions ∨
– négations que sur les atomes

¬hiver ∨ froid

63
 Principe de résolution
• La règle d ’inférence
– modus ponens vue d ’une autre façon

A ∨ C, ¬C ∨ B forme normale
clause A∨B

– trouver deux clauses telles que

• on y trouve une proposition positive dans l ’une
• on y trouve la même proposition négative dans l ’autre
• fusionner ces deux clauses = création d ’une clause
64
Chapitre 7. Démonstration automatique
 Principe de résolution
• Exemple

été ∨ hiver, ¬hiver ∨ froid

été ∨ froid

65
Chapitre 7. Démonstration automatique
 Principe de résolution
• Prouver que des prémisses impliquent une
proposition S.
– nier S et convertir le résultat en FNC
– convertir les prémisses en FNC
– répéter jusqu’à ce qu ’une contradiction
apparaisse
• sélectionner 2 clauses
• les résoudre mutuellement
• si le résolvent est la clause vide, une contradiction est trouvée
• sinon, ajouter le résolvent aux prémisses 66
 Principe de résolution : exemple
démontrer que {p→r,q →r}|=(p∨q →r)
revient à démontrer que {p→r,q →r, ¬(p∨q →r)}|= Ø}
négation de la conclusion
Conversion en FNC :
p→r ¬p∨r (1)
q →r ¬q ∨ r (2)
¬(p∨q →r) p∨q (3)
¬r (4)

67
Chapitre 7. Démonstration automatique
 Principe de résolution : exemple
¬p∨r (1) ¬r (4)
résolution
¬q ∨ r (2)
p∨q (3) ¬p (5)
résolution
résolution
¬q (6)
q (7)
résolution Contradiction :
le théorème est vrai
Ø Preuve par réfutation
68
Chapitre 7. Démonstration automatique
 Règles d ’obtention d ’une FNC
• Dans l ’ordre

A↔B (A→B)∧(B →A)

A →B ¬A∨B
¬(A ∧B) ¬A ∨ ¬B
¬(A ∨ B) ¬A ∧ ¬B
¬ ¬A A
A ∨ (B ∧ C) (A ∨ B) ∧ (A ∨ C)

Correspond au ‘∧’
– Exemple : p↔(q → r) donne
(¬p∨ ¬ q ∨ r),(q ∨ p) , (¬r ∨p)
clause
69
Chapitre 7. Démonstration automatique
 Clause de Horn
• Le principe de résolution est très rapide si les
clauses sont sous la forme de clauses de Horn.
(suppressions de clauses équivalentes ou « conséquences valides »)

• Une clause de Horn

– contient 1 litteral positif et au moins 1 négatif
(clause de Horn stricte)
– 1 seul litteral positif (clause de Horn positive)
– que des litteraux négatifs (clause de Horn
négative) 70
Chapitre 7. Démonstration automatique
 Résolution sur clauses de Horn
• Exemple

– inconsistance de {¬ p ∨ r, ¬r ∨ s, p, ¬ s}
– 1. Sélection de p et ¬ p ∨ r : {r, ¬r ∨ s, p, ¬ s}
– 2. Sélection de r et ¬r ∨ s : {r, s, p, ¬ s}
– 3. Sélection de ¬ s et s : {r, s, p, Ø}

inconsistance
71
Chapitre 7. Démonstration automatique
 Interprétation des clauses de
Horn
– clauses de Horn positives : p∨q∨..
• faits, vérités logiques
– clauses de Horn strictes : q∨¬p1∨¬p2∨…
• équivalent à {p1, p2, …}|= q
• règle si .. alors
– clauses de Horn négatives ¬p∨¬q∨¬r...
hypothèses

• si on cherche à prouver {H1, H2..}|=(p∧q∧r) but

• revient à prouver {H1, H2,.., ¬p∨¬q∨¬r}|=Ø
• but à atteindre, question
72
Chapitre 7. Démonstration automatique
 Démonstration automatique :
et pour la logique du premier ordre ?
• En logique propositionnelle
àLaMaison ∨ auTravail ¬àLaMaison

auTravail

• En logique des prédicats

∀x (àLaMaison(x) ∨ auTravail(x) ) ¬àLaMaison(y)

73
Chapitre 7. Démonstration automatique
 Démonstration automatique
et pour la logique du premier ordre ?
• Le Problème
– en logique propositionnelle, les propositions
sont considérées « vraies »

– en logique des prédicats :

• elles dépendent de variables
• les clauses sont formées à partir de prédicats
communs

74
Chapitre 7. Démonstration automatique
 Démonstration automatique
et pour la logique du premier ordre ?
• La solution
– mêmes principes qu ’en calcul propositionnel :
preuve de l ’inconsistance (par résolution)
– mise des formules sous forme « prénexe »
– mise des formules sous forme de skolem
– mise sous forme de clauses
– rechercher les valeurs « cohérentes » des
variables : UNIFICATION || résolution
75
Chapitre 7. Démonstration automatique
 Démonstration automatique
• La forme prénexe

∃x ∀y ∃z (¬p(x) ∨ ¬q(y)) ∨ (p(z) ∧q(z))

Plus d ’implication

Quantificateurs à
l ’extérieur

équivalent

∀x p(x) ∧ ∃y q(y) → ∃y(p(y) ∧ q(y))

76
Chapitre 7. Démonstration automatique
 Démonstration automatique
• Mise sous forme prénexe

A↔B (A→B)∧(B →A)

A →B ¬A∨B
¬(A ∧B) ¬A ∨ ¬B
¬(A ∨ B) ¬A ∧ ¬B
¬ ¬A A
A ∨ (B ∧ C) (A ∨ B) ∧ (A ∨ C)
¬∀x A ∃x ¬A
¬ ∃x A ∀x ¬A
77
Chapitre 7. Démonstration automatique
 Démonstration automatique
• Mise sous forme prénexe
– respecter l ’ordre suivant :
∀x p(x) ∧ ∃y q(y) → ∃y(p(y) ∧ q(y))
1. suppression de →, ↔ : ¬(∀x p(x) ∧ ∃y q(y)) ∨ ∃y(p(y) ∧ q(y))
2. renommage des variables : ¬(∀x p(x) ∧ ∃y q(y)) ∨ ∃z(p(z) ∧ q(z))
3. transfert des ¬ vers l ’intérieur : (∃x¬ p(x) ∨ ∀y¬q(y)) ∨ ∃z(p(z) ∧ q(z))
4. déplacement des quantificateurs :
∃x ∀y ∃z ((¬ p(x) ∨ ¬ q(y))∨ (p(z) ∧ q(z)))

78
Chapitre 7. Démonstration automatique
 Démonstration automatique
• Mise sous forme de Skolem
– suppression des quantificateurs
• existentiels : création d ’une fonction
• universels : sous-entendus

ps : la forme de skolem n ’est pas strictement équivalente

à la formule initiale, mais si une forme de skolem est
satisfiable, la formule dont elle est issue l ’est aussi

79
Chapitre 7. Démonstration automatique
 Démonstration automatique
• Forme de Skolem, exemple
– formule initiale :∀x p(x) ∧ ∃y q(y) → ∃y(p(y) ∧ q(y))
– forme prénexe : ∃x ∀y ∃z ((¬ p(x) ∨ ¬ q(y)) ∨ (p(z) ∧ q(z)))
– forme de skolem : ∀y(¬ p(a) ∨ ¬ q(y)) ∨ (p(f(y)) ∧ q(f(y))))

Constante, car x ne peut dépendre

d ’aucune variable
fonction, car z peut dépendre de y

– forme normale : idem au calcul propositionnel (distribution du ∨)

(p(f(y)) ∨ ¬ p(a) ∨ ¬ q(y)) ∧ ( q(f(y) ∨ ¬ p(a) ∨ ¬ q(y)) )))

– forme clausale :
{p(f(y)) ∨ ¬ p(a) ∨ ¬ q(y) , q(f(y) ∨ ¬ p(a) ∨ ¬ q(y)) ))} 80
Chapitre 7. Démonstration automatique
 Démonstration automatique
• Résolution par unification
– Recherche d ’un prédicat
• positif dans une clause
• négatif dans une autre

– tenter de les rendre égaux :

• Une variable peut être remplacée par une constante
• Une variable peut être remplacée par une variable
• Une variable peut être remplacée par une fonction qui ne la contient pas
• Une substitution/instanciation qui rend réductible deux clauses est une
UNIFICATION
81
Chapitre 7. Démonstration automatique
 Démonstration automatique
• L ’unification, exemple :

b
a
table

Sachant que b est sur a et a est sur table, déduire

que b est au-dessus de la table
82
Chapitre 7. Démonstration automatique
 Démonstration automatique
• Note : les variables s ’écrivent désormais X, Y , … les constante a, b, table

• Axiomes :
∀ X ∀ Y [sur(X,Y)→auDessus(X,Y)]
∀ X ∀ Y ∀ Z [auDessus(X,Y) ∧auDessus(Y,Z)→auDessus(X,Z)]

• Mis sous forme normale

¬sur(U,V) ∨ auDessus(U,V) (1)
¬auDessus(X,Y) ∨ ¬auDessus(Y,Z) ∨ ¬auDessus(X,Z) (2)

• Deux axiomes supplémentaires spécifiques à l ’exemple

sur(b,a) (3)
sur(a,table) (4) 83
Chapitre 7. Démonstration automatique
 Démonstration automatique
• On veut démontrer : auDessus(b, table)
• déduction / résolution
¬sur(U,V) ∨ auDessus(U,V) (1)
¬auDessus(X,Y) ∨ ¬auDessus(Y,Z) ∨ auDessus(X,Z) (2)
sur(b,a) (3)
sur(a,table) (4)
¬auDessus(b, table) (5)

réfutation

¬auDessus(b,Y) ∨ ¬auDessus(Y,table) (2) et (5) -> (6)

84
Chapitre 7. Démonstration automatique
 Unification

¬auDessus(X,Y) ∨ ¬auDessus(Y,Z) ∨ auDessus(X,Z) (2)

¬auDessus(b, table) (5)
unification : X=b
Z=table

¬auDessus(b,Y) ∨ ¬auDessus(Y,table) (6)

¬sur(U,V) ∨ auDessus(U,V) (1)

unification : U=Y
V=table

¬sur(Y,table) ∨ ¬ auDessus(b,Y) (7)

85
Chapitre 7. Démonstration automatique
 Unification

¬sur(Y,table) ∨ ¬ auDessus(b,Y) (7) ¬sur(U,V) ∨ auDessus(U,V) (1)

unification : U=b
V=Y

¬sur(b,Y) ∨ ¬sur(Y,table) (8) sur(b,a) (3)

unification : Y=a

¬ sur(a,table) (9) sur(a,table) (4)

Preuve par déduction/réfutation

86
Chapitre 7. Démonstration automatique
 8. Programmer en logique

87
Chapitre 8. Programmer en logique
 Un premier programme
PROLOG
% l ’exemple des blocs

sur(a,table).
sur(b,a).
auDessus(X,Z):- sur(X,Z).
auDessus(X,Z):- auDessus(X,Y), auDessus(Y,Z).

Question à prolog
-? auDessus(b,table).

Yes
...
88
Chapitre 8. Programmer en logique
 Bibliographie
• Ouvrages
• Intelligence artificielle & informatique théorique, J.M. Alliot & T. Schiex, cepadus edition, 1994.
• Approche logique de l ’intelligence artificielle, A. Thayse et al, Dunod Informatique, 1988.
• Introduction à la calculabilité, Pierre Wolper, Interedition, 1991.
• Outils logiques pour l ’Intelligence Artificielle, J.P. De lahaye, 1986.

• Web :
• [Link]
• [Link]

89
 Limite du calcul propositionnel

• il fait beau ou il pleut

pareil
• il pleut ou il fait beau

• il prit peur et il tua l ’intrus

pas pareil
• il tua l ’intrus et il pris peur

90
Calcul propositionnel : le modèle
• Conséquence valide
Soit A = (p→q)∧(p∨r)
B = (q ∨ r)
C = (p → r)
• Si A est vraie B est vraie (C ?) (table de vérité)
• B est une conséquence valide de A, (A B)
• Utile lors des démonstrations
91
 Calcul propositionnel :
axiomatique
• Exemple démonstration de |- (A→A)
1. |- ((A → (B → C)) → ((A → B) → (A → C))) - axiome 2
2. |- ((A → ((A →A) →A)) →((A →(A →A)) → (A →A)))
subtitution de B par A →A et de C par A
3. |- A →(B →A) - axiome 1
4. |- A → ((A → A) →A) - substitution de B par (A → A) dans 3
5. |- ((A →(A →A)) →(A →A)) : inférence entre 4 et 2
6. |- A → (A → A) - axiome 1 avec substitution de B par A
7. |- A → A inférence entre 5 et 6

c ’est fastidieux

92
 Calcul propositionnel :
propriétés importantes

• Adéquation
tout ce que je peux déduire de ma logique est valide

– si |- A alors |= A
– tout théorème est une formule valide
– le calcul propositionnel est adéquat

93
 Calcul propositionnel :
propriétés importantes
• Consistance

avec ma logique, je ne peux pas trouver une chose vraie et fausse à la

fois

– il n ’existe pas de formule telle que |-A et |- ¬A

– le calcul propositionnel est consistant

94
 Calcul propositionnel :
propriétés importantes
• Complétude
lien modèle-langage, tout ce que mon modèle
considère valide, mon langage peut le prouver

– le calcul propositionnel est complet

ps : différentes familles de complétude

– forte : si E |=A alors E|–A
– faible : quand |=A alors |–A (les règles de raisonnement permettent de démontrer
toutes les formules valides)
– syntaxique : pour tout A on a soit |–A soit |–¬A
95
 Calcul propositionnel :
Propriétés fondamentales
• Décidabilité

Une logique est décidable si on connaît une

procédure permettant de savoir, en un temps fini,
si une formule donnée est ou n’est pas un
théorème

– Le calcul propositionnel est décidable

96
 Calcul des prédicats : le langage
• Exemple de traduction d ’énoncés en formules
– tout est relatif
∀x relatif(x)

– Il y a des peines, il y a des plaisirs, mais aucune peine n'est un plaisir

(∃x peine(x)) ∧ (∃x plaisir(x)) ∧ (∀x (peine(x)→¬plaisir(x)))

– il existe un plus grand entier

(∃x entier(x)) ∧ (∀y(entier(y) → plusgrand(x,y)))
97
 Calcul des prédicats : le langage
• Les variables libres sont sources de
sophisme logique

– différence entre identité et égalité conditionnelle

• (x + 1)^2 = x^2 + 2x + 1
• x^2 - 4x + 4 = 0

98
 Approche cognitive
• noms et dates
• arguments :
– fonctions cognitives humaines = algorithmes
• proposition :
– formaliser ces fonctions ↔ langages / calculs
• base :
– logiques formelles
• résultats :
– PROLOG, d ’autres langages expérimentaux
99
 Approche pragmatique
• noms et dates
• arguments :
– fonctions cognitives humaines trop complexe
– machine = contrainte matérielle
• proposition :
– faire au mieux pour que ça marche / bon sens
• base :
– programmation logique, calcul de complexité
• résultats :
– systèmes experts, heuristiques, Allen, SHDRLU ... 100
 Approche connexionniste
• noms et dates
• arguments :
– fonctions cognitives humaines = trop complexe
• proposition :
– imitons le cerveau au niveau « hard »
• base :
– biologie
– mathématiques
• résultats :
– réseau de neurones, ... 101
 Calcul de prédicats : le langage
• Preuve par réfutation
• Preuve par résolution

102
 Logique propositionnelle :
le langage
• Les synonymes (règles d ’équivalence)
– exemple :
si on prend juste {¬ , ∨ , ∧} comme connecteurs
primitifs

• FALSE peut être défini comme p ∧ ¬ p

• A → B peut être défini comme ¬ A v B.

103
 Logique propositionnelle :
axiomatique
• La substitution
– F est une formule contenant des atomes p1,
p2,..pn
– si | F
– si F* est F dans laquelle on remplace p1, p2..
par des formules A1, A2…
– alors : | F*
• Utiliser pour les démonstrations
104
 Calcul des prédicats : le langage
• Formule fermée : toutes les variables sont liées
∀ x ∀ y ((p(x) ∨ ∃ x p(x)) ∧ q(y))

• Formule ouverte
∀ y ((p(x) ∨ ∃ x p(x)) ∧ q(y))

105
 Note sur les systèmes formels
• Prouver la complétude et décidabilité…??
• Outil : Machines de Turing
• exemple :
– incomplétude de l ’arithmétique formelle
– indécidabilité de l ’arithmétique formelle

106
 Langage naturel : syntaxe,
sémantique, pragmatique
Il avait le nez collé à un mur haut, large et épais ...

• Il avança à un cha : lexicalement incorrect

• il avança à un chat : lexicalement correct, mais syntaxiquement
incorrect ;
• il avança d'un chat : syntaxiquement correct, mais sémantiquement
incorrect ;
• il avança d'un pas : sémantiquement correct, mais pragmatiquement
incorrect (à cause du mur) ;
• il recula d'un pas : pragmatiquement correct.

107