LIA Master 1 IFIA

Introduction à la Logique
 Introduction à la logique

Sommaire
 Historique & Introduction

 Logique des propositions

 Logique des prédicats

Introduction à la logique 2
 I. Historique & Introduction

Quelques dates de l’histoire de La logique

 En -300 : Aristote (considéré souvent comme le père de la ‘Logique’ comme
discipline) définit les concepts de la logique, il divise la logique en 3 parties :
l’étude de la conception, du jugement et du raisonnement;
 Leibniz (1646-1713) envisage q’une machine puisse raisonner : enchaîner des
propositions élémentaires pour faire des déductions;

 En 1854 : Boole reprend l’étude de Leibniz, il démontre, dans son ouvrage The
Laws of Thought (Les lois de la pensée) que tous les processus logiques peuvent
être modélisés par des opérations logiques utilisant les opérateurs de base (ET,
OU, NON) appliqués à des variables à deux états. Depuis cette date, on peut dire
que la logique a migré de la philosophie vers les mathématiques.

Introduction à la logique 3
 I. Historique & Introduction

Quelques dates de l’histoire de La logique

 Vers la fin du XIX siècle, Frege fonde la science des systèmes formels et invente
le calcul des prédicats.
 Au début du XX siècle, Tarski propose une théorie de la référence expliquant
comment relier les objets d’un système formel logique et les objets du monde
réel, autrement dit, la formalisation d’un domaine de connaissances par un
système formel devient possible. C’est la naissance de la notion de démonstration
automatique
 En 1931, Gödel montre que la logique des prédicats est seulement semi-
décidable : il existe une procédure effective pour prouver (en un temps fini) tout
énoncé vrai, mais ce n’est pas le cas pour les énoncés faux.

Introduction à la logique 4
 I. Historique & Introduction

Introduction
 La Logique est la discipline qui s'attaque à la notion de validité des
raisonnements, toutefois, la manière de traiter cette notion, les fondements,
le formalisme utilisé, etc., changent d’une logique à une autre.
 Nous avons une sorte d’arbre d’héritage entre ces différentes logiques :

Introduction à la logique 5
 I. Historique & Introduction

Introduction
 En logique: un raisonnement valide utilise des règles d’inférence valides.
 Une règle d’inférence permet le passage d’un certain nombre de prémisses à une
conclusion.
 Une règle d’inférence est valide à cause de sa forme et non pas à cause du sens
des prémisses, par exemple, la règle Modus Ponens :

A A  B
_____________
B

Introduction à la logique 6
 I. Historique & Introduction

Introduction (fin)
 Parmi les règles d’inférence valides, citons :
 Règle Modus Tollens :
¬B A  B
_____________
¬A
 Règle du Syllogisme :
A  B B  C
_____________
A  C
 Règle de Résolution :
¬X  A X  B
_____________
A  B

Introduction à la logique 7
 II. Logique des propositions

Sommaire
 Introduction
 Langage propositionnel
 Théorie des modèles
 Théorie de la preuve
 Introduction
 Méthodes axiomatiques
 Méthode des tables de vérité
 Méthode de Résolution

Introduction à la logique 8
 II. Logique des propositions

Introduction
 La logique des propositions est une branche de la Logique et plus
précisément de la logique classique.
 Dans la logique des propositions, les opérations qui lient les propositions
pour en former d’autres plus complexes sont appelées des connecteurs,
 Un connecteur binaire permet de composer deux propositions pour en
obtenir une troisième,
 un connecteur unaire permet d’obtenir une proposition à partir d’une autre .

Introduction à la logique 9
 II. Logique des propositions

Introduction
 Dans la logique de propositions, nous pouvons considérer trois niveaux
d'analyse:
 Langage propositionnel (syntaxique) : définition des formules bien formées
(fbf ou wff), i.e. les propositions correctes syntaxiquement;
 Théorie des modèles (sémantique) : définition des notions de validité des
propositions et de relation de conséquence logique entre propositions;
 Théorie de la preuve (axiomatique) : définition des notions de prouvabilité
des propositions et de déduction;

But : valide = prouvable

Introduction à la logique 10
 II. Logique des propositions

Langage propositionnel : LP
Définition 1 : l’alphabet de LP
 L'alphabet de la logique propositionnelle est constitué de :
 un ensemble dénombrable de variables propositionnelles (ou formules
atomiques, ou encore atomes) : par exemple, p, q, r, …., il_pleut,
la_route_est_mouillée, …
 Les constantes : F (faux, ie: ‘0’ de Boole) et V (vrai, ie: ‘1’ de Boole)
(Rq1: ¬ F est équivalente à V, on peut s’en passer de V si on veut)
(Rq2: F est équivalente à (p ¬p) on peut s’en passer de F si on veut)
 les connecteurs : ¬ ,  ,  ,  et 
(Rq: on préfère ne pas utiliser : ‘ou exclusif ’)
 les séparateurs ‘(‘ et ‘)‘.

Introduction à la logique 11
 II. Logique des propositions

Langage propositionnel : LP (suite)

Définition 2 : Formules bien formées (fbf ou wff)
 L'ensemble des formules (ou propositions) de la logique propositionnelle est le
plus petit ensemble de mots construits sur l'alphabet tel que :
 si A est une formule atomique alors A est une formule;
 F (faux) est une formule ;
 ¬ A est une formule si A est une formule;
 (A  B), (A  B), (A  B) et (A  B) sont des formules si A et B sont des
formules.
 N.B: A et B qui désignent ci-dessus des formules sont des ‘metavariables’ car
ils ne font pas partie de l'alphabet de LP.
 Si on n’utilise pas des parenthèses, l’ordre de priorité des connecteurs est
comme suit : ¬ ,  , , ,  , et l’associativité est à gauche pour chaque
connecteur.

Introduction à la logique 12
 II. Logique des propositions

Langage propositionnel : LP (suite)

Définition 3 : Sous-formules
 L'ensemble des sous-formules d'une formule A est le plus petit ensemble tel
que :
 A est une sous-formule de A.
 Si (¬ B) est une sous-formule de A alors B est une sous-formule de A.
 Si (B  C) (respectivement (B v C) ou (B  C) ou(B  C)est une sous-
formule de A alors B et C sont des sous-formules de A.

 L'endroit où une sous-formule apparaît est son occurrence.

 Une ss-formule peut avoir plusieurs occurrences dans une formule.

Introduction à la logique 13
 II. Logique des propositions

Langage propositionnel : LP (suite)

Définition 4 : Substitution uniforme
 Une substitution (ou substitution uniforme) associe à une variable
propositionnelle p une formule A . Elle est notée [p\A].
 L'application de [p\A] à une formule B , notée B[p\A], est le résultat du
remplacement simultané de toutes les occurrences de p dans B par A.
 B [p\A], est appelé une instance de B.

Introduction à la logique 14
 II. Logique des propositions

Théorie des modèles :

Définition 1: Interprétation
 Une interprétation I (ou valuation) est une application de l'ensemble des variables
propositionnelles dans l'ensemble des valeurs de vérité {V,F} (ou {0,1}).
Définition 2: Interprétation des formules
 Une interprétation donnée I peut être étendue à l'ensemble des formules comme
suit (A et B étant des formules) :
 I(F) = F (ou 0 ) et I(V) = V (ou 1)
 I(¬A) = V si I(A)= F et I(¬A) = F sinon
 I(A  B) = V si I(A)= V et I(B) =V et I(A  B) = F sinon (ou min(I(A),I(B)))
 I(A v B) = V si I(A)= V ou I(B) =V et I(A  B) = F sinon (ou max(I(A),I(B)) )
 I(A  B) = V si I(A) = F (ou 0) ou I(B) =V (ou 1) et I(A  B) = F sinon.
 I(A  B) = V si I(A  B) =V (ou 1) et I(B A) =V (ou 1) et I(A  B) = F sinon.

Introduction à la logique 15
 II. Logique des propositions

Théorie des modèles (suite):

Définition 3 : Modèle
 I est un modèle pour une formule A (ou I satisfait A) ssi I(A) = V , noté |=I A.
 I est un modèle pour un ensemble de formules S ssi I est un modèle pour
toute formule A de S.
Définition 4 : Validité, Satisfaisabilité
 Soit A une formule: Exemples
 A est valide (ou tautologique ; noté |= A) si I(A) = V pour toute
interprétation I. Sinon A est invalide ou falsifiable.
 A est satisfaisable ssi il existe une interprétation I t.q. I(A) = V. Sinon
A est non satisfaisable ou contradictoire.

Introduction à la logique 16
 II. Logique des propositions

Théorie des modèles (suite):

Définition 5 : consistance.
 Soit S un ensemble de formules.
 S est inconsistant s’il n'existe aucun modèle pour S, autrement dit, un
modèle pour lequel toutes les formules de S ont simultanément la valeur
vrai. Si un tel modèle existe S est dit consistant ou satisfaisable.
Définition 6 : Conséquence logique.
 Une formule A est conséquence logique de n formules A1, ... ,An, noté {A1, ...
,An} |= A, ssi tout modèle de {A1, ... ,An } est un modèle de A.
Définition 7 : Équivalence tautologique
 Soit A1 et A2 deux formules, elles sont dites tautologiquement équivalentes
si A1 |= A2 et A2 |= A1 .
Exemples

Introduction à la logique 17
 II. Logique des propositions

Théorie des modèles (suite):

Théorème 1 : Conséquence logique et implication

 Soient A et B deux formules et S un ensemble de formules contenant A :

 A |= B ssi |= (A  B).
 S |= B ssi S /{A} |= (A  B).

Introduction à la logique 18
 II. Logique des propositions

Théorie de la preuve : Introduction

 L’intérêt pratique de la théorie de la preuve est qu’elle répond à l’un des buts
recherchés en intelligence artificielle, qui est la démonstration automatique de
théorèmes (formules valides).
 Dans la théorie de la preuve, il existe différentes méthodes (appelées aussi
systèmes formels) qui permettent de prouver la validité –ou seulement la
satisfiabilité- d’une formule propositionnelle.
 Ces méthodes peuvent être utilisées pour déduire une proposition à partir
d’un certain nombre de propositions (hypothèses).

Introduction à la logique 19
 II. Logique des propositions

Théorie de la preuve : Introduction (suite)

 Parmi ces méthodes, on trouve :
 Méthodes axiomatiques
 Exemples:
 Axiomatique de Kleene
 Axiomatique de Hilbert

 Méthode des tables de vérité

 Méthode des tableaux sémantiques
 Méthode de résolution

Introduction à la logique 20
 II. Logique des propositions

Théorie de la preuve : Introduction (fin)

 Les méthodes de preuve formelles, peuvent, en effet, être classifiées selon
différents critères, dont :
 Méthodes directes ou par réfutation,
 Méthodes axiomatiques ou sémantiques,
 Méthodes nécessitant une forme normale ou pas, etc.
 Toutefois, ces méthodes de preuve doivent toutes répondre au critère de
correction, i.e, toute proposition prouvable est valide.
 Un autre critère important est la complétude, i.e, toute proposition valide est
prouvable.

Introduction à la logique 21
 II. Logique des propositions

Théorie de la preuve : Méthodes axiomatiques

Définition 1 : Axiome & Schéma d’axiomes
 Un axiome est une formule propositionnelle valide (à cause de sa forme et non
pas à cause de l’interprétation de ses propositions atomiques).
 L’ensemble d’axiomes étant infini, on utilise plutôt des schémas d’axiomes de
nombre fini pour représenter la forme générale d’une famille d’axiomes.
 Un axiome est donc une instance (par substitution uniforme) d'un schéma.
Exemple :
A B A
A  (B  A) (p q )  ( (r  s) (p q ) )

Schéma d’axiome Axiome

Introduction à la logique 22
 II. Logique des propositions

Théorie de la preuve : Méthodes axiomatiques (suite)

Définition 2 : Méthode de preuve axiomatique.
 Une méthode axiomatique est une méthode formelle se basant sur un certain nombre
de schémas d’axiomes (valides) et de règles d’inférence valides et qui pour une
proposition (fbf) donnée (à prouver), elle peut donner une suite finie de propositions,
constituant une preuve, telle que :
 La 1ère proposition de la suite soit un axiome instance d'un des schémas
d’axiomes retenus par la méthode.
 Chacune des propositions qui suivent soit un axiome ou soit directement dérivable
de quelques unes des propositions qui la précèdent dans la suite, en vertu des
règles d’inférences.
 La dernière proposition de la suite (de propositions) est la proposition à prouver.

Introduction à la logique 23
 II. Logique des propositions

Théorie de la preuve : Méthodes axiomatiques (suite)

Définition 3 : Prouvabilité
 Soit A une formule.
 A est prouvable (noté |- A) s’il existe une preuve de A.

Introduction à la logique 24
 II. Logique des propositions

Théorie de la preuve : Méthodes axiomatiques (suite)

Définition 4 : Déduction.
 Une déduction d'une formule A à partir d'hypothèses (propositions) B1,...,Bm
(notée {B1,...,Bm } |- A) est une liste finie de formules (A1, ... ,An) t.q :
 An = A
 pour i = 1, ...,n, la formule Ai est :
 soit un axiome,
 soit égal à une des hypothèses Bj,
 soit obtenue par application de la règle de Modus Ponens à partir de deux
prémisses Aj, Ak précédant Ai dans la liste.
 Rq: Une preuve n’utilisant que la règle Modus Ponens est une déduction sans
hypothèses.

Introduction à la logique 25
 II. Logique des propositions

Théorie de la preuve : Méthodes axiomatiques (suite)

Lemme 1 :
 La règle de Modus Ponens préserve la validité :
 Si |= A et |= (A ⇒ B) alors |= B .
Lemme 2 :
 La substitution uniforme préserve la validité :
 Soient A et B des formules et p une proposition atomique:
 Si |= A alors |= A[p\B].

Introduction à la logique 26
 II. Logique des propositions

Théorie de la preuve : Méthodes axiomatiques (suite)

Théorème 1 : Adéquation d’une preuve
 Si A est prouvable alors A est valide :
 Si |- A alors |= A.
Théorème 2 : Complétude
 Si A est valide alors A est prouvable :
 Si |= A alors |- A.

But : valide = prouvable

Introduction à la logique 27
 II. Logique des propositions

Théorie de la preuve : Méthodes axiomatiques (suite)

Théorème 3 : Déduction et implication
 A |- B ssi |- (A  B). (A et B étant des formules)
 S |- B ssi S /{A} |- (A  B). (S ensemble de formules contenant A)
Problème : Décidabilité
 Si une formule est valide alors elle est prouvable par une méthode axiomatique
(complétude), mais si elle ne l'est pas alors la méthode ne s'arrêtera jamais.
Théorème 4 : Procédure décidable
 La logique propositionnelle est décidable : il existe une procédure effective qui pour
toute formule A en entrée s'arrête et retourne `oui' si A est valide, et `non' sinon.

Introduction à la logique 28
 II. Logique des propositions

Théorie de la preuve : Méthodes axiomatiques (fin)

Exemple : Axiomatique de Kleene
 Schémas d’axiomes (10):
A  (B  A)
(A  ( B C))  ((A  B)  (A  C))
A  (B  (A  B) )
(A  B)  A
(A  B)  B
AAvB
BAvB
 Règle d’inférence :
(A  C) ((B  C)  ((A v B)  C))
 Modus Ponens (A  B)  ((A  ¬B) ¬A)
 Propriété : ¬¬A  A ¬ F (toujours vraie)
 Complétude.

Introduction à la logique 29
 II. Logique des propositions

Théorie de la preuve : Méthode des Tables de vérité

Définition 5 :
 Elle permet de donner les valeurs de vérité possibles d’une formule composée F pour
chaque combinaison possible des valeurs de vérité des propositions atomiques qui sont
sous-formules de F.
Construction :
 On commence par définir, pour chaque connecteur c, une table qui associe une valeur
de vérité à une formule de type ‘A c B’ pour chaque attribution de valeurs de vérité à ces
sous-formules (A et B dans ce cas). C'est ce qu'on appelle les tables de vérité des
connecteurs tvc.
 Étant donné une formule quelconque, il est alors possible de construire sa table de
vérité, en calculant sa valeur de vérité pour chaque combinaison possible des valeurs de
vérité de ces variables propositionnelles moyennant les tables de vérité des connecteurs.

Introduction à la logique 30
 II. Logique des propositions

Théorie de la preuve : Méthode des Tables de vérité (suite)

Validité d’une formule :
 Chaque ligne d'une table de vérité d’une formule A correspond à une
combinaison possible des valeurs de vérité de toutes les variables
propositionnelles apparaissant dans A. Ceci peut être vue comme la
description d’une interprétation de l'ensemble des n variables propositionnelles de
la formule dans l'ensemble des valeurs de vérité {F, V}.
 L’ensemble des lignes (2n) de la table représente, donc, toutes les
interprétations possibles de l'ensemble des variables propositionnelles de la
formule dans l'ensemble des valeurs de vérité {F, V}.
 Si pour chaque ligne la valeur de la formule A est V alors, chaque interprétation
-de l'ensemble des variables propositionnelles de la formule dans l'ensemble des
valeurs de vérité {F, V} - est un modèle pour A, et donc A est valide.

Introduction à la logique 31
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution

Formes normales et clausales :
Définition 6 : littéral, forme normale disjonctive
 Un littéral est une formule atomique ou la négation d'une formule atomique
(exps : p et ¬ q avec p et q atomes).
 Une formule est une Forme Normale Disjonctive (FND) si elle est une
disjonction de conjonctions de littéraux.
Définition 7: clause, forme normale conjonctive
 Une clause est une disjonction de n (n≥0) littéraux (exp: ¬p1 v p2v p3).
 Une formule est une forme normale conjonctive (FNC) si elle est une
conjonction de clauses .

Introduction à la logique 32
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (suite)

Théorème 6 : Équivalence et formes normales
 Toute formule propositionnelle est équivalente à une forme normale
conjonctive et à une forme normale disjonctive
Algorithme de mise en forme normale conjonctive
Entrée : une formule A1 Sortie : une fnc A’1 équivalente à A1
Début Eliminer  et  et F (si il est utilisé);
Appliquer à A1 les remplacements suivants autant de fois que nécessaire:

¬ ¬ A --> A
A et B des sous
¬ (A v B) --> ¬ A  ¬B ¬
formules de A1
(A  B) --> ¬ A v ¬B
A v (B  C) --> ( A v B)  (A v C)
Fin
Introduction à la logique 33
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (suite)

Théorème 7 : Validité d’une clause
 Une formule en fnc est valide ssi toutes ses clauses sont valides.
 Une clause est valide ssi elle contient deux littéraux opposés, c-à-d , de la forme L1 v
... v p v ... v ¬p v ... v Ln.
Définition 8 : Notation ensembliste/ Forme clausale
 Une clause C = L1 v ... v Li v ... v Ln peut s’écrire comme étant l’ensemble de ces
littéraux : C = {L1 , ... , Li , ... , Ln } .
 Une forme normale conjonctive A= C1 …  Ci …  Cn est écrite en forme clausale
sous la forme d’un ensemble de clauses A = {C1 , ... , Ci , ... , Cn } ou d’une suite de
clauses C1 , ... , Ci , ... , Cn.
 A est donc valide ssi toutes les clauses qu’elle contient sont valides.

Introduction à la logique 34
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (suite)

Conséquence 1: clause vide
 La clause vide est équivalente à F, elle est contradictoire.
 En effet, elle ne contient pas deux littéraux opposés vu qu’elle n’en contient pas du
tout.
Conséquence 2 : ensemble vide de clauses
 L’ensemble vide de clauses est équivalent à ¬F, il est donc valide.
 En effet, on peut dire que toutes ses clauses sont valides puisque il n’en contient pas
du tout.

Introduction à la logique 35
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (suite)

Théorème 8 : Principe de Résolution
 Soient C1 et C2 deux clauses :
Si il existe un littéral L1 tel que L1  C1 et son opposé L2  C2 (ie l’équivalent
de L1) alors, la clause C3 = (C1 - L1)  (C2 – L2) est une conséquence logique de
C1 et C2 : {C1 , C2} |= C3.
 C3 est dite un résolvant de C1 et C2.
Rappel : Règle de résolution
¬X  A X  B
_____________
{¬X, A} {X, B}
A  B _____________
{A, B}
Introduction à la logique 36
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (suite)

Conséquence
 Les clauses C1={ p } et C2= {¬p } ont pour résolvant la clause vide { }.
 Or, une formule A= p  ¬p est équivalente à l’ensemble de clauses S={C1,C2}
qui est tel que S |= { } d’après le théorème 8.
 Or A est équivalente à F (toujours fausse) ou encore S inconsistant.
 D’où le théorème qui suit :
Théorème 9 : Ensemble de clauses inconsistant
 Soit S un ensemble de clauses, S est inconsistant ssi S |= { } .

Introduction à la logique 37
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (suite)

Théorème 10 : Réfutation
 Soit une formule A et S un ensemble de formules, S|= A est équivalent à
S  {¬A} est inconsistant (i.e. S {¬A} |= F) .
Preuve par réfutation
 Soit S un ensemble de clauses et G une clause à montrer comme
conséquence logique de S (S |= G) ;
 On considère S  { G} et on montre qu’il est inconsistant, c-à-d,
S  {G} |= { }, d’après le théorème précédent ceci est équivalent à S|=G.

Introduction à la logique 38
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (suite)

Algorithme de résolution par réfutation
Soit S= {C1, C2,…., Cn} un ensemble fini de clauses :
Soit G une clause à prouver:
1/ Remplacer S par S  {G} (S S  {G}) .
2/ Si on peut choisir une nouvelle paire de clauses C1 et C2
dans S telqu’il existe p atome avec p  C1 et  p C2 alors
calculer le résolvant R de C1 et C2.
3/ a/ Si R ={ }, la preuve est faite.
b/ Sinon, S S  {R} et retourner à l’étape 2
4/ Sinon (plus de choix possibles) alors S est consistant.

Introduction à la logique 39
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (suite)

Exemple de résolution par réfutation

H1 : P  Q H1 : P  Q  C1: {P , Q }
H2 : Q  R  H2 : Q  R  C2 : {Q , R }
B : P  R? B :  (P  R)  P  R
 C3= {P}
C1: {P , Q } 2 clauses
 C4= {R}
C2 : {Q , R }
R1 : {P, R }
C3 : {P}
R2 : {R}  R3 : { } C.Q.F.D
C4 : { R} Introduction à la logique 40
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (suite)

Théorème 11 : Conséquence logique et clauses
 Soient C1 et C2 deux clauses (en notation ensembliste),
 Si C1  C2 alors C1 |= C2.
Théorème 12 : Élimination des clauses valides
 Soit S un ensemble de clauses et C une clause valide ,
S  {C} est valide (resp. satisfaisable) ssi S est valide (resp. satisfaisable) .
Remarque :
 Ce théorème stipule que pour montrer la validité (resp. satisfaisabilité) d’un
ensemble de clauses, on peut toujours ignorer les clauses tautologiques.

Introduction à la logique 41
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (suite)

Définition 9: déduction par résolution
 Soit S un ensemble de clauses et C une clause ,
Une déduction par résolution de C à partir de S est une suite de clause C1, …, Cn
telle que :
 Cn = C et ∀ i / 0< i< n, on a :
 Soit Ci ∈ S ;
 Soit, ∃ k,l / 1≤ k < l < i tels que Ci est un résolvant de Ck et Cl.

 Lorsque une telle preuve existe on peut la noter : S |- res C

Introduction à la logique 42
 II. Logique des propositions

Théorie de la preuve : Méthode de Résolution (fin)

Théorème 13: Validité d’une preuve par résolution
 Soit S un ensemble de clauses et C une clause ,
 Si S |- res C alors S |= C.
Remarque :
 La preuve par réfutation d’une clause C à partir d’un ensemble de clauses S est
une déduction par résolution de la clause vide à partir de l’ensemble S  {¬ C}
qu’on appelle, plus brièvement, réfutation.
Théorème 13: Complétude de la résolution par réfutation
 Soit S un ensemble de clauses et C une clause ,
 Si S {¬C} |= { }, alors S {¬ C} |- res { } .

Introduction à la logique 43