S é m a n t iq u e d e la lo g iq u e

■ Comment écrire les formules ?

● Aspects syntaxiques

■ Comment déterminer la valeur de vérité d’une formule ?

● Aspects sémantiques
● logique bivaluée : vrai, faux
● interprétation

■ Comment démontrer de nouveaux résultats ?

● Aspects déductifs
● Conséquence logique
● démonstration
● règles de déduction

Programmation Logique et Prolog 1

I n t e r p r é t a t io n ( 1 / 2 )
■ But : donner une valeur de vérité aux formules

■ Une interprétation I d'une formule F est basée sur un ensemble de

définition D, non vide, appelé domaine
● à chaque symbole de constante de F est associé un élément de D
● à chaque symbole de variable de F est associé la variable elle-même
● à chaque symbole de fonction de F est associée une fonction de Dn dans D
● à chaque symbole de prédicat de F est associé une fonction de Dn dans {0,1}
● à chaque connecteur d'arité i est associée une fonction de {0,1}i dans {0,1}

a ¬a ∨ 1 0 ∧ 1 0 ⇒ 1 0
1 0 1 1 1 1 1 0 1 1 0
0 1 0 1 0 0 0 0 0 1 1

Programmation Logique et Prolog 2

 I n t e r p r é t a t io n ( 2 / 2 )
● si F = ∀x G(x,y1,..,yn) (G formule dépendant de x et des variables libres
y1,..,yn), pour tout (a1,..,an) de Dn, I(F)(a1,..,an) vaut 1 si pour tout a de D, I(G)
(a, a1,..,an) = 1, et vaut 0 sinon

● si F = ∃ x G(x,y1,..,yn) (G formule dépendant de x et des variables libres

y1,..,yn), pour tout (a1,..,an) de Dn, I(F)(a1,..,an) vaut 1 s'il existe a de D telle
que I(G)(a, a1,..,an) = 1, et vaut 0 sinon

■ Toute formule close peut donc être interprétée dans {0,1}

■ Une interprétation d'une formule contenant i variables libres

donne une application de Di dans {0,1}. Une formule peut être
ainsi vue comme une fonction booléenne de ses variables libres
dans {0,1}.

■ Une interprétation d'une formule est un modèle de cette formule

si la formule est vraie pour cette interprétation
Programmation Logique et Prolog 3

Ex e m p le d 'in t e r p r é t a t io n
■ Interprétons F = ∀x p(x) ⇒ q(x) sur le domaine {a,b,c}
■ Une interprétation possible de la formule
x I(p)(x) I(q)(x) I(p ⇒ q)(x)
a 1 1 1
=> F est vraie
b 0 0 1
c 1 0 1

Autre exemple d'interprétation

x I(p)(x) I(q)(x) I(p ⇒ q)(x)

a 0 1 0
=> F est fausse
b 0 1 0
c 1 0 1

Programmation Logique et Prolog 4

 V a lid it é
■ Une formule est valide (tautologie) si elle est vraie quelque soit
l'interprétation (si toute interprétation est un modèle)
● exemple : ∀x ¬ p(x) ∨ p(x) est une tautologie

■ Une formule est consistante (ou satisfiable) s'il existe une

interprétation dans laquelle elle est vraie
● exemple : ∃x ¬ p(x)

■ Une formule est insatisfiable (ou inconsistante) s'il n'existe pas

d'interprétation dans laquelle elle est vraie
● exemple : ¬ p(x) ∧ p(x)

■ Note : une formule peut être invalide et consistante

Programmation Logique et Prolog 5

Eq u iv a le n ce
■ Deux formules f et f' sont sémantiquement équivalentes si pour
toute interprétation I, I(f) = I(f'), c'est à dire que leur tables de
vérité sont les mêmes (on note f ≡ f')

■ Quelques équivalences utiles :

● p ⇒q≡¬p∨q
● p ∧ ¬ p ≡0

● p ∨ ¬ p ≡1

● ¬ (¬ p) ≡ p

● ¬ (p ∧ q) ≡ ¬ p ∨ ¬ q (loi de Morgan)
● ¬ (p ∨ q) ≡ ¬ p ∧ ¬ q (loi de Morgan)
● p ∧ q ≡ q ∧ p et p ∨ q ≡ q ∨ p (symétries de ∧ et ∨)

● associativités de ∧ et ∨
● p ∨ 1 ≡ 1 et p ∧ 0 ≡ 0 (absorption)
● p ∧ 1 ≡ p et p ∨ 0 ≡ p (élément neutre)

Programmation Logique et Prolog 6

 S a t isf a ct io n
■ Un ensemble de formules {f1, .. , fn} satisfait une formule f si pour
toute interprétation I, pour tout i=1..n, si I(fi) = 1 alors I(f) = 1,
c'est-à-dire si tout modèle de {f1, .. , fn} est aussi modèle de f. On
note {f1, .. , fn} ╞ f. On dit aussi que f est conséquence logique de
{f1, .. , fn}

■ Si f est une formule valide, on note ╞ f

■ {f1, .. , fn} ╞ f équivaut à ╞ (f1 ∧ .. ∧ fn) ⇒f

ou ╞ ¬ (f1 ∧ .. ∧ fn) ∨ f
ou, si les formules sont closes, f1 ∧ .. ∧ fn ∧ ¬ f est
inconsistante (preuve par réfutation ou par l'absurde)
Programmation Logique et Prolog 7

S y st è m e f o r m e l e t p r e u v e
■ La notion de conséquence logique oblige, pour vérifier qu'une
formule est satisfaite par des hypothèses, à utiliser un domaine
et à assigner des valeurs de vérités : il s'agit d'une méthode
sémantique

■ La notion de démonstration (ou de preuve) est purement

syntaxique : on applique formellement des règles pour passer
mécaniquement des hypothèses à la formule
● on introduit un cadre formel pour les démonstrations

■ Un système formel S est constitué de :

● F un ensemble de formules
● A un ensemble d'axiomes A ⊂ F
● un ensemble fini de règles de déduction valides

Programmation Logique et Prolog 8

 D é d u ct io n
■ Une preuve dans un système formel S est une suite finie
d'énoncés A1, .. An telle que pour tout i, Ai est un axiome de S ou
une conséquence des Aj (j<i) par application d'une règle de
déduction.

■ Un théorème de S est le dernier énoncé d'une preuve. Si A est un

théorème, on note ├ A

■ Une formule A est déductible d'un ensemble de formules {f1, .. , fn}

ssi il existe une suite finie A1, .. , An d'énoncés telle que An = A et
pour tout i<n, Ai est un axiome ou Ai ∈ {f1, .. , fn} ou Ai découle
des Aj (j<i) par application d'une règle de déduction.
On note {f1, .. , fn} ├ A

Programmation Logique et Prolog 9

Rè g le s d e d é d u ct io n
■ Modus ponens : {(f ⇒ g), f} ├ g

■ Modus tollens : {(f ⇒ g), ¬g} ├ ¬f

■ Syllogisme : {(f ⇒ g), (g ⇒ h)} ├ (f ⇒ h)
■ Généralisation : f├ ∀x f

■ ...

■ Propriété : F et G étant deux formules, {F} ├ G si et seulement si

F ⇒
G est un théorème (├ (F G)) ⇒
Programmation Logique et Prolog 10
 Co m p lé t u d e e t co r r e ct io n ( 1 / 2 )
Théorie des Théorie de la
modèles démonstration
Interprétation sémantique Interprétation syntaxique
sur un domaine
Tables de vérité des Axiomes, règles d'inférence
connecteurs et prédicats
Tautologie Théorème
Conséquence ╞ Déduction ├

■ Un système est complet ssi ╞ g implique ├ g (on peut démontrer

toutes les tautologies)

■ un système est correct ssi ├ g implique ╞ g (tous les théorèmes

sont des tautologies)

Programmation Logique et Prolog 11

Co m p lé t u d e e t co r r e ct io n ( 2 / 2 )
■ Théorème : le calcul des prédicats est correct et complet (Gödel,
1929)

■ En particulier pour le système suivant (dit système minimal)

■ axiomes du calcul propositionnel (a,b et c étant des formules)

⇒ ⇒
⇒ ⇒ ⇒ ⇒ ⇒ (a ⇒ c))
● a (b a)

⇒ ⇒ ⇒
● (a (b c)) ((a b)
● (¬ b ¬ a) (a b)
■ axiomes du calcul des prédicats (a,b étant des formules et x une
variable)
⇒ a(t)
∀x a(x)
⇒ ⇒ (a ⇒ ∀x b)
●
● (a b)

■ régles : modus ponens et généralisation

Programmation Logique et Prolog 12
 D é cid a b ilit é

■ Un système est décidable s'il existe un algorithme permettant de

décider à coup sur si une formule est vraie ou fausse

■ Théorème : le calcul des propositions est décidable (méthode

des tables de vérité)

■ Théorème : le calcul des prédicats est indécidable (Church 1936)

● en fait il est semi-décidable : on peut toujours prouver en un temps fini
qu'une formule est vraie (complétude) mais pas qu'une formule est fausse

Programmation Logique et Prolog 13

P r in cip e d e r é so lu t io n
■ Le principe de résolution (Robinson 1965) est une règle de
déduction en logique propositionnelle :
A ∨ B, ¬A ∨ C ├ B ∨ C

■ Le principe de résolution est valide

● il faut montrer (A ∨ B) ∧ (¬ A ∨ C) => B ∨ C
● Si A est vrai, alors C est vrai donc B ∨ C aussi
● Si A est faux, alors B est vrai et donc B ∨ C aussi

■ Pour utiliser le principe de résolution, il faut identifier un littéral et

sa négation dans une formule (A et ¬A) et à fabriquer la formule
résultante ne dépendant plus du littéral

■ Le principe de résolution permet, par réfutation, de démontrer

une formule à partir d'un ensemble de formules, si toutes ces
formules sont sous forme clausales
Programmation Logique et Prolog 14
 Ré so lu t io n e t r é f u t a t io n
■ Procédure de résolution par réfutation pour prouver une formule F
sous forme clausale à partir d'un ensemble de formules clausales
{F1,..,Fn}
● on prend la négation de F
● on prouve par résolution que {F1,..,Fn, ¬ F} est inconsistant en calculant les
résultantes jusqu'à obtenir la clause vide

A ├reso B si et seulement si A ∧{¬

¬B} ├reso □

■ Théorème :
● si un ensemble de clauses est insatisfiable, alors il admet une réfutation par
résolution (complétude)
● si un ensemble de clauses admet une réfutation par résolution, il est
insatisfiable (correction)

Programmation Logique et Prolog 15

Ex e m p le d e r é so lu t io n
■
⇒ ⇒ ⇒r
Formule propositionnelle à démontrer :
{p r, q r} ╞ (p ∨ q)

■ La négation de (p ∨ q) ⇒ r est ¬ (¬ (p ∨ q) ∨ r) ≡ (p ∨ q) ∧ ¬r
■ {¬ p ∨ r, ¬ q ∨ r , p ∨ q, ¬r} est l'ensemble de clauses de départ

■ ¬ p ∨ r et ¬r sont résolues en ¬p
■ ¬ q ∨ r et ¬r sont résolues en ¬q
■ ¬ p et p ∨ q sont résolues en q
■ q et ¬q sont résolues en □

Programmation Logique et Prolog 16

 Ré so lu t io n e t cla u se s d e H o r n
■ La résolution par réfutation n'est pas toujours efficace si on ne
choisit pas les bonnes clauses
● en particulier, dans le cas général, il n'est pas plus efficace que les méthodes
sémantiques consistant à construire des interprétations (algorithme de Quine,
de Davis & Putnam)

■ Dans un système de démonstration automatique, il faut pouvoir

choisir les bonnes clauses pour avoir un calcul efficace

■ Solution => utiliser des clauses de Horn

Programmation Logique et Prolog 17

Ré so lu t io n e n ca lcu l d e s
p r é d ica t s
■ On veut résoudre des formules du calcul des prédicats à l'aide
du principe de résolution en calcul propositionnel

■ Pour utiliser la réfutation par résolution en calcul des prédicats, il

faut transformer les formules en clauses
● Première étape : on transforme la formule en formule normale conjonctive
(conjonction de clauses)
● Deuxième étape : on tranforme les formules normales conjonctives en
formules normales prénexes (avec les quantificateurs en tête)
● Troisième étape : on skolémise la formule obtenue pour éliminer les
quantificateurs

Programmation Logique et Prolog 18

 F o r m e n o r m a le co n jo n ct iv e
■ Forme normale conjonctive : conjonction de disjonctions

■ Règles de transformation en forme normale conjonctive :

● on transforme les ⇒ par équivalence p ⇒ q ≡ ¬ p ∨ q
● on accole les négations aux atomes en utilisant ¬ ¬ F ≡ F et les lois de
Morgan
● on utilise la distributivité de ∧ et ∨ pour obtenir une conjonction de clauses
● on renomme les variables si nécessaire

■ Théorème : toute formule admet une forme normale conjonctive

équivalente

Programmation Logique et Prolog 19

Form e p ré ne xe
■ Forme prénexe : les quantificateurs sont en tête de formule

■ Règles pour transporter les quantificateurs en tête de formule :

¬ ∀x F ≡ ∃x ¬ F ¬ ∃x F ≡ ∀x ¬ F
∀x ∀y F ≡ ∀y ∀x F ∃x ∃y F ≡ ∃y ∃x F
∀x F ∧ ∀x H ≡ ∀x (F ∧ H) ∃x F ∨ ∃x H ≡ ∃x (F ∨ H)

● Si H ne contient aucune occurence de x :

(∀x F) ∨ H ≡ ∀x (F ∨ H) (∃x F) ∧ H ≡ ∃x (F ∧ H)
∀x F ≡ F ∃x F ≡ F
● Renommer les variables si besoin est

■ Théorème : toute formule admet une forme prénexe équivalente

Programmation Logique et Prolog 20

 Ex e m p le
■
⇒
Mise sous forme normale prénexe de la formule
∀x p(x) ∧ ∃y q(y) ∃y (p(y) ∧ q(y))

■ Suppression de ⇒:
● ¬ (∀x p(x) ∧ ∃y q(y)) ∨ ∃y (p(y) ∧ q(y))

■ Renommage des variables :

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

■ Transfert de la négation :
● (∃x ¬ p(x) ∨ ∀y ¬ q(y)) ∨ ∃z (p(z) ∧ q(z))

■ Déplacement des quantificateurs :

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

■ Forme normale :
● ∃x ∀y ∃z ((¬ p(x) ∨ ¬ q(y) ∨ p(z)) ∧ (¬ p(x) ∨ ¬ q(y) ∨ q(z))
Programmation Logique et Prolog 21

F o r m e d e S k o le m
■ On élimine les quantificateurs existentiels :
● remplacer toute variable quantifiée existentiellement par une fonction ayant
pour arguments les variables quantifiées universellement précédant la
première variable
● cette fonction est celle qui prend sur le domaine d'interprétation la valeur
qui rend la formule vraie

■ Théorème : si F est une formule, il existe F' forme de Skolem de

F et ╞ F ssi ╞ F' (ce n'est pas une équivalence logique!)

■ Une fois les quantificateurs existentiels supprimés, toutes les

variables restantes sont quantifiées universellement (dans une
formule close), on peut donc supprimer les quantificateurs
universels

Programmation Logique et Prolog 22

 Ex e m p le
■ Skolémisons la formule normale prénexe
∃x ∀y ∃z ((¬ p(x) ∨ ¬ q(y) ∨ p(z)) ∧ (¬ p(x) ∨ ¬ q(y) ∨ q(z))

■ La variable z est tranformée en f(y)

● ∃x ∀y ((¬ p(x) ∨ ¬ q(y) ∨ p(f(y))) ∧ (¬ p(x) ∨ ¬ q(y) ∨ q(f(y)))

■ La variable x est transformée en g (fonction d'arité nulle ou

constante)
● ∀y ((¬ p(g) ∨ ¬ q(y) ∨ p(f(y))) ∧ (¬ p(g) ∨ ¬ q(y) ∨ q(f(y)))

■ Démontrer une formule c'est prouver que sa négation est

inconsistante ou que la forme de Skolem de sa négation est
inconsistante

■ On peut donc se limiter à travailler sur des formes de Skolem

Programmation Logique et Prolog 23

Th é orè m e d e H e rb ra n d ( 1 /4 )
■ Pour appliquer le principe de résolution à des formes de
Skolem, il faut donner des valeurs aux variables universelles
■ Impossible en pratique de résoudre une formule pour toutes les
valeurs possibles des variables sur un domaine

■ Intérêt du théorème de Herbrand : Quand on a une formule sous

forme de Skolem, on peut se limiter pour étudier sa satisfiabilité
à son univers de Herbrand

■ Termes de base et atomes de base d'un ensemble de clauses E

● un terme de base est un terme qui ne contient pas de variable
● un atome de base est un atome qui ne contient pas de variable

Programmation Logique et Prolog 24

 Th é orè m e d e H e rb ra n d ( 2 /4 )
■ Univers de Herbrand d'un ensemble de clauses E : l'univers de
Herbrand de E est l'ensemble des termes de base que l'on peut
construire à partir des symboles de fonctions et des constantes
qui apparaissent dans E

■
⇒
Exemple : l'univers de Herbrand de l'ensemble
{p(f(x)) q(a),r(g(x))} est {a,f(a),g(a), f(f(a)), f(g(a)), g(f(a)), ...}

■ Base de Herbrand d'un ensemble de clauses E : la base de

Herbrand de E est l'ensemble des atomes de base qui peuvent
être construits à partir des symboles de prédicats de E appliqués
aux termes de l'univers de Herbrand de E

■
⇒
Exemple : la base de Herbrand de l'ensemble
{p(f(x)) q(a),r(g(x))} est
{p(a),q(a),r(a),p(f(a)),q(f(a)),r(f(a)),p(g(a)),q(g(a)),r(g(a)),...}
Programmation Logique et Prolog 25

Th é orè m e d e H e rb ra n d ( 3 /4 )
■ Interprétation de Herbrand : l'ensemble de définition est l'univers
de Herbrand. Une interprétation de Herbrand d'un ensemble E
de clauses est obtenue en remplaçant les variables de E par des
éléments de l'univers de Herbrand de E

■ Une interprétation de Herbrand est une interprétation mais pas le

contraire.
■
⇒ ⇒
Exemple : une interprétation de Herbrand de l'ensemble
{p(f(x)) q(a),r(g(x))} est {p(f(a)) q(a),r(g(f(a)))}

■ Modèle de Herbrand d'un ensemble de clauses E : c'est une

interprétation de Herbrand de E qui est un modèle de E

Programmation Logique et Prolog 26

 Th é orè m e d e H e rb ra n d ( 4 /4 )
■ Théorème de Herbrand (Herbrand 1929) : un ensemble de
clauses E est insatisfiable si et seulement si il existe un
ensemble fini d'interprétations de Herbrand de E qui soit
insatisfiable

■ Conséquence : montrer une formule sous forme clausale revient

à trouver une interprétation de Herbrand qui soit insatisfiable

■ Pour montrer qu'une formule F est valide :

● on construit F', la forme normale de Skolem de sa négation
● on trouve une interprétation de Herbrand
● on montre par résolution que cette interprétation est insatisfiable
● => F' est donc insatisfiable et donc F est valide

■ Le principe de résolution doit être étendu au calcul des prédicats

à travers le mécanisme d'unification
Programmation Logique et Prolog 27

S u b st it u t io n
■ Exemple : soient les clauses C1 = p(x) ∨ q(x) et C2 = ¬ p(f(y)) ∨
r(y)
● on ne peut appliquer la résolution, car aucun littéral de C1 n'est la négation
d'un littéral de C2 ou l'inverse
● on voudrait pouvoir substituer f(y) à x dans C1, ce qui donnerait par
résolution q(x) ∨ r(y)

■ Une substitution consiste à remplacer un nombre fini de variables

par des termes. On note {t1/v1, .. , tn/vn} la substitution qui
remplace toute variable vi par le terme ti.

■ L'application d'une substitution S à un ensemble de clauses E est

appelé instance de E selon S

Programmation Logique et Prolog 28

 U n if ica t e u r
■ Composition de substitution : la composition de deux
substitutions s1 et s2, notée s1o s2, est obtenue en 3 étapes
● appliquer s2 aux termes de s1
● retirer de s2 les couples ti/vi tels que vi est une variable de s1
● rassembler les couples obtenues en 1 et 2

■ Exemple : s1 = {f(y)/x , z/y} et s2 = {a/x , b/y , y/z}

● la première étape donne {f(b)/x , y/y}
● la deuxième donne {y/z}
● la troisième étape donne {f(b)/x , y/z} (on supprime y/y qui ne change rien)

■ Unificateur : une substitution S unifie un ensemble de clauses

E = {c1, .. , cn} si S(c1) = .. = S(c2)

■ Exemple : {f(a)/x , a/y} unifie {p(a,x), p(a,f(y))}

Programmation Logique et Prolog 29

U n if ica t e u r le p lu s g é n é r a l
■ Unificateur le plus général : l'unificateur le plus général d'un
ensemble de clauses E est un unificateur U de E tel que pour
tout autre unificateur V de E, il existe une substitution S telle que
V=SoU

■ Cet unificateur le plus général n'existe pas forcément (pas plus

qu'un unificateur) et s'il existe, il n'est pas forcément unique

■ Trouver un unificateur le plus général permet d'appliquer le

principe de résolution à des clauses issues de formules du
premier ordre

Programmation Logique et Prolog 30

 Alg o r it h m e d 'u n if ica t io n
■ Algorithme d'unification
● Données : deux expressions E1 et E2

● si E1 ou E2 est un atome alors échanger les données de façon à ce que

E1 soit un atome et passer à 2
sinon passer à 3
● si E1 et E2 sont identiques alors retourner Ø
sinon si E1 est une variable
si E1 a une occurence dans E2 alors retourner échec
sinon retourner {E2/E1}
sinon si E2 est une variable alors retourner {E1/E2}
sinon retourner échec
● F1 := le premier élément de E1, T1 := le reste de E1 F2
:= le premier élément de E2, T2 := le reste de E2
● U1 := unification(F1,F2)
● si U1 = échec alors retourner échec
sinon G1 := U1(T1), G2 := U1(T2)
● U2 := unification(G1,G2)
● si
Programmation U2 =etéchec
Logique Prolog alors retourner échec sinon retourner U1oU2 31

R é ca p it u la t if
■ Pour démontrer qu'une formule F du calcul des prédicats peut
être déduite d'un ensemble E de clauses
● on procède par réfutation en créant G = ¬ F
● la skolémisation de G permet de ramener le problème de l'inconsistance de
G U E à celui de l'inconsistance d'un ensemble de clauses {C1,..,Cn} U E
● le théorème de Herbrand permet de ramener la démonstration de
l'inconsistance de {C1,..,Cn} U E à la découverte d'une instanciation des
variables dans l'univers de Herbrand qui rende l'ensemble de clauses
insatisfiable
● le principe de résolution permet de montrer l'insatisfiabilité de l'instance
construite

■ En Prolog, on n'a que des clauses de Horn

● La skolémisation est inutile mais elle garantit que ce qu'on écrit en Prolog est
quasiment aussi expressif que la logique des prédicats
● Le mécanisme de Prolog consiste à construire une instanciation de la clause
but et de clauses de la base de connaissance tout au long d'une procédure
de résolution par réfutation
Programmation Logique et Prolog 32