[Plan | Introduction | Logique propositionnelle (langage, théorie des modèles, théorie de la preuve, propriétés, FNC, démonstration automatique) | Logique des prédicats | Logiques non-classiques]

LOGIQUE PROPOSITIONNELLE


Logique propositionnelle : langage

Introduction

Définition (alphabet). L'alphabet de la logique propositionnelle est constitué de

Notation. Nous utilisons p, q, r, p1, p2 ,... pour des variables propositionnelles.

Définition (formule). L'ensemble FOR des formules (ou formules bien formées) de la logique propositionnelle est le plus petit ensemble de mots construits sur l'alphabet tel que

Exemples de formules

Notation. Nous utilisons A , B , C , A1 , A2,... pour des formules (strictement parlant, A,B,... sont des metavariables, car ils ne font pas partie de l'alphabet de la logique). S , S1 , S2 ,... dénotent des ensembles de formules.

Remarque. Notre jeu de connecteurs primitifs consiste en FALSE , ~ , ∧ , ∨ , -> . D'autres connecteurs peuvent être définis en tant que abréviations :
TRUE abrévie (~FALSE) et l'équivalence (A <-> B) abrévie ((A -> B) ∧ (B -> A)) .
(Annexe : remarque sur des jeux de connecteurs alternatifs)


suite : notions de substitution uniforme et de sous-formule






























                                                      


[Plan | Introduction | Logique propositionnelle (langage, théorie des modèles, théorie de la preuve, propriétés, FNC, démonstration automatique) | Logique des prédicats | Logiques non-classiques]

Logique propositionnelle : langage (suite)

Définition (sous-formule). L'ensemble des sous-formules d'une formule A est le plus petit ensemble tel que

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

Définition (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. (A)[p\B] est appelé une instance de A.

Exemples de substitutions

Notation. On omet toujours les parenthèses les plus à l'extérieur. En général, l'omission de parenthèses peut être source d'ambiguïtés : ainsi, ~p ∧ q peut correspondre à (~p) ∧ q et à ~(p ∧ q) . Cependant, on peut omettre la plupart des parenthèses en donnant des priorités aux connecteurs, dans l'ordre suivant : <-> , -> , ∧ , ∨ , ~ . La négation ~ est le connecteur le plus fort : il `attire plus les parenthèses' que , etc. Ainsi, ~p ∨ q correspond à (~p) ∨ q , etc.

Annexe : remarque sur une définition plus constructive de FOR

Annexe : rappel sur les démonstrations par induction


suite : section sur la théorie des modèles




































                                                      


[Plan | Introduction | Logique propositionnelle (langage, théorie des modèles, théorie de la preuve, propriétés, FNC, démonstration automatique) | Logique des prédicats | Logiques non-classiques]

Logique propositionnelle : théorie des modèles

Introduction

Définition (interprétation). Une interprétation I (ou valuation) est une application de l'ensemble des variables propositionnelles ATM dans l'ensemble des valeurs de vérité {0,1}.

Définition (interprétation des formules). Une interpretation donnée I peut être étendue à l'ensemble des formules FOR par :

I est un modèle pour A (ou I satisfait A) ssi I(A) = 1.
I(A) = 1 est parfois 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.
Exemples

Définition (validité, satisfiabilité). Soit A une formule.
A est valide (ou tautologique ; noté |= A) si I(A) = 1 pour toute interpretation I. Sinon A est invalide ou falsifiable.
A est satisfiable ssi il existe une interpretation I t.q. I(A) = 1. Sinon A est insatisfiable ou contradictoire.
Exemples

Définition (conséquence logique). Une formule A est conséquence logique de A1, ... ,An (noté A1, ... ,An |= A) ssi tout modèle de A1, ... ,An est un modèle de A.
Exemples ; plus sur la conséquence logique


suite : section sur la théorie de la preuve





































                                                      


[Plan | Introduction | Logique propositionnelle (langage, théorie des modèles, théorie de la preuve, propriétés, FNC, démonstration automatique) | Logique des prédicats | Logiques non-classiques]

Logique propositionnelle : théorie de la preuve

Introduction

Définition (axiomatique à la Hilbert). Les schémas d'axiome de la logique propositionnelle sont

A -> (B -> A)

(A -> B) -> ((A -> (B -> C)) -> (A -> C))

A -> (B -> A ∧ B)

(A ∧ B) -> A

(A ∧ B) -> B

A -> A ∨ B

B -> A ∨ B

(A -> C) -> ((B -> C) -> (A ∨ B -> C))

(A -> B) -> ((A -> ~B) -> ~A)

~~A -> A

~FALSE


et la règle d'inférence est le Modus Ponens :

A    A -> B
_____________
B

A et A -> B sont appelées prémisses, et B est appelée conclusion de la règle.
(Rappel : on omet les parenthèses selon les priorités suivantes : <-> , -> , ∧ , ∨ , ~ .)

Chaque formule qui a la forme d'un schéma est appelée un axiome. Ainsi, un axiome est une instance d'un schéma. P.ex. (p ∧ q) -> (r -> (p ∧ q)) est un axiome, obtenu à partir du premier schéma A -> (B -> A).
Annexe : remarque sur une axiomatisation qui n'a pas besoin de la notion de schéma (nécessitant une règle de substitution uniforme)


suite : notion de preuve et de déduction

































                                                      


[Plan | Introduction | Logique propositionnelle (langage, théorie des modèles, théorie de la preuve, propriétés, FNC, démonstration automatique) | Logique des prédicats | Logiques non-classiques]

Logique propositionnelle : théorie de la preuve (suite)

Définition (preuve). Soit A une formule. Une preuve de A est une liste finie de formules (A1, ... ,An) t.q.

Exemples

Définition (prouvabilité, consistance). Soit A une formule.
A est prouvable (noté |- A) si il existe une preuve de A.
A est consistante si ~A n'est pas prouvable. Sinon A est inconsistante.
Exemples

Définition (déduction). Une déduction d'une formule A à partir d'hypothèses B1,...,Bm (noté B1,...,Bm |- A) est une liste finie de formules (A1, ... ,An) t.q.

Exemples

Donc une preuve est une déduction à partir d'un ensemble vide d'hypothèses.
Parfois les axiomes sont appellées `axiomes logiques', et les hypothèses `axiomes non-logiques'.

Annexe : remarque sur des ensembles d'hypothèses infinis


suite : section sur les propriétés importantes






























                                                      


[Plan | Introduction | Logique propositionnelle (langage, théorie des modèles, théorie de la preuve, propriétés, FNC, démonstration automatique) | Logique des prédicats | Logiques non-classiques]

Logique propositionnelle : propriétés importantes

Introduction

Adéquation et de complétude

Lemme (la règle de modus ponens préserve la validité). Si |= A et |= A -> B alors |= B.

Lemme (la substitution uniforme préserve la validité). Soient A et B des formules et p un atome. Si |= A alors |= A[p\B].
(cf. la remarque sur une axiomatisation avec une règle de substitution uniforme dans la section sur la théorie de la preuve)

Théorème d'adéquation. Si |- A alors |= A.
(la démonstration utilise les lemmes précédents, et le fait que les axiomes sont valides)

Théorème de complétude. Si |= A alors |- A.
(la démonstration est difficile)

Théorème de déduction

Théorème de déduction. A |- B ssi |- A -> B.

Donc le problème de déduction A |- B peut être réduit au problème de prouvabilité |- A -> B .

Théorème de la conséquence logique (version sémantique du théorème de déduction). A |= B ssi |= A -> B.

Donc le problème de conséquence logique A |= B peut être réduit au problème de validité |= A -> B .
Annexe : théorèmes d'adéquation et de complétude forte (non pas entre validité et prouvabilité, mais entre conséquence logique et déduction)

Décidabilité

Théorème (existence d'une procédure de décision). 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.

Un exemple de procédure de décision est la méthode des tables de vérité. Une méthode plus efficace est la méthode de balayage.
L'axiomatique est une caractérisation finie des formules valides : elle peut être `rendue opérationelle' comme procédure énumerant l'ensemble des formules prouvables. Mais ceci ne nous donne qu'une procédure de semi-décision : si la formule en question est valide, cette procédure va la trouver un jour, mais si elle ne l'est pas alors la procédure ne s'arrêtera jamais.


suite : quelques équivalences utiles





































                                                      


[Plan | Introduction | Logique propositionnelle (langage, théorie des modèles, théorie de la preuve, propriétés, FNC, démonstration automatique) | Logique des prédicats | Logiques non-classiques]

Logique propositionnelle : propriétés importantes (suite)

Remarque. Étant donné les théorèmes d'adéquation et de complétude, les propriétés qui suivent peuvent être formulées et en termes de prouvabilité (avec |-) et en termes de validité (avec |=).

Remplacement des équivalences logiques

Théorème (remplacement des équivalences). Soit B une sous-formule de A, et soit |- B <-> C . Si A' est obtenue à partir de A par le remplacement de cette occurrences de B par C alors |- A <-> A'.
Exemples d'application

Remarque. Le remplacement en question n'est pas une substitution uniforme (cette dernière ne s'applique qu'aux atomes, et non à des formules ; de plus, elle s'applique à toutes les occurrences, et non à une ou plusieurs).

Ëquivalences permettant d'éliminer des connecteurs

élimination de l'implication :
|- A -> B <-> ~A ∨ B
élimination de l'équivalence :
|- (A <-> B) <-> (A -> B) ∧ (B -> A)
élimination de FALSE :
|- FALSE <-> p ∧ ~p    (pour un p quelconque)
élimination de la négation :
|- ~A <-> A -> FALSE
éliminations de la disjonction :
|- A ∨ B <-> ~(~A ∧ ~B)
|- A ∨ B <-> (A -> FALSE) -> B
éliminations de la conjonction :
|- A ∧ B <-> ~(~A ∨ ~B)
|- A ∧ B <-> (A -> (B-> FALSE)) -> FALSE
(v. aussi l'annexe sur des jeux de connecteurs alternatifs)

Ëquivalences correspondant aux propriétés algébriques des connecteurs

idempotence de ~ :
|- ~~A <-> A
idempotence de et :
|- A ∧ A <-> A
|- A ∨ A <-> A
associativité de et :
|- A ∧ (B ∧ C) <-> (A ∧ B) ∧ C
|- A ∨ (B ∨ C) <-> (A ∨ B) ∨ C
commutativité de et :
|- A ∧ B <-> B ∧ A
|- A ∨ B <-> B ∨ A
distributivité (lois de De Morgan) :
|- (A ∨ B) ∧ C <-> (A ∧ C) ∨ (B ∧ C)
|- (A ∧ B) ∨ C <-> (A ∨ C) ∧ (B ∨ C)

(Rappel : on omet les parenthèses selon les priorités suivantes : <-> , -> , ∧ , ∨ , ~.)
suite : section sur la forme normale conjonctive

































                                                      


[Plan | Introduction | Logique propositionnelle (langage, théorie des modèles, théorie de la preuve, propriétés, FNC, démonstration automatique) | Logique des prédicats | Logiques non-classiques]

Logique propositionnelle : forme normale conjonctive

Introduction et motivation

Définition (littéral, clause, forme normale conjonctive).
Un littéral est une formule atomique ou la négation d'une formule atomique.
Une clause est une disjonction de littéraux.
Une formule est en forme normale conjonctive si elle est une conjonction de clauses.
Exemples

Notation. Nous utilisons L, L1 , L2 ... pour des littéraux, et C, C1 , C2 ... pour des clauses.

Notation. On suppose que les disjonctions et conjonctions sont parenthésées à gauche :
une clause L1 ∨ L2 ∨ ... ∨ Ln est ((...(L1 ∨ L2) ∨ ...) ∨ Ln), et
une conjonction de clauses C1 ∧ C2 ... ∧ Cm est ((...(C1 ∧ C2) ...) ∧ Cm).
Ceci est justifié par l'associativité de la conjonction et de la disjonction (v. aussi les exemples).
Par convention, une disjonction de 0 littéraux est FALSE (la clause vide), et une conjonction de 0 clauses est TRUE.
Notation. Nous confondons une conjonction de clauses avec un ensemble de clauses, et une clause avec un ensemble de littéraux. Ceci est justifié par la commutativité et l'idempotence de la conjonction et de la disjonction. Ainsi, la formule en forme normale conjonctive (p ∨ q) ∧ (~p ∨ r) sera confondu avec l'ensemble { {p ∨ q} , {~p ∨ r} }. La clause vide FALSE sera confondu avec l'ensemble vide {}.

Algorithme de mise en forme normale conjonctive
entrée : une formule A
sortie : une formule en forme normale conjonctive
début
     éliminer -> , <-> , FALSE ;
     appliquer autant que possible les équivalences suivantes (en remplaçant le membre gauche par le membre droit), dans n'importe quel ordre :
fin
Exemples

Théorème. Pour toute entrée A, l'algorithme de mise en forme normale conjonctive s'arrête. Il retourne une formule en forme normale conjonctive équivalente à l'entrée.
(la démonstration utilise le théorème de la substitution des équivalents : les remplacements effectués par l'algorithme correspondent à des équivalences prouvables)

Théorème. Une formule en forme normale conjonctive est valide ssi toute clause contient deux littéraux contradictoires, c-à-d chaque clause est de la forme L1 ∨ ... ∨ p ∨ ... ∨ ~p ∨ ... ∨ Ln.


suite : section sur la démonstration automatique































                                                      


[Plan | Introduction | Logique propositionnelle (langage, théorie des modèles, théorie de la preuve, propriétés, FNC, démonstration automatique) | Logique des prédicats | Logiques non-classiques]

Logique propositionnelle : démonstration automatique

Introduction

La méthode de balayage (résolution non-clausale)

Algorithme de balayage
entrée : une formule A
sortie : TRUE ou FALSE
début
éliminer -> , <-> ;
tant que non(A = TRUE) et non(A = FALSE) faire
choisir une variable propositionnelle p apparaîssant dans A ;
remplacer A par la formule A[p\TRUE] ∧ A[p\FALSE] ;
appliquer autant que possible les équivalences suivantes (en remplaçant le membre gauche par le membre droit), dans n'importe quel ordre :
fin tant que
fin

Remarque. La liste des équivalences utilisées n'est pas complète : on a supposé tacitement que la commutativité de et de est exploité.

Exemples

Remarque. Les exemples montrent que le choix de l'atome à substituer est crucial (une heuristique possible est de choisir l'atome qui a le plus d'occurrences dans A).

Théorème. Pour tout entrée A, l'algorithme de balayage s'arrête. Il retourne TRUE si A est valide, et FALSE sinon.
Démonstration. La terminaison est assurée par le fait que chaque passage de la boucle élimine un atome. Ensuite, comme |= A ssi |= (A[p\TRUE] ∧ A[p\FALSE]), la deuxième étape préserve la validité. Finalement, les simplifications correspondent à des équivalences valides.

Remarque. L'équivalence A <-> (A[p\TRUE] ∧ A[p\FALSE]) n'est pas valide (exemple : A = p).


suite : chapitre sur la logique des prédicats



































                                                      

https://www.irit.fr/~Andreas.Herzig