Cours Logique et Calculabilit

L3 Informatique 2013/2014

Texte par Sverine Fratani, avec addenda par Luigi SantocanaleVersion du 14 janvier 2014

2

Table des matires

1 Introduction 51.1 Pourquoi la logique ? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.1.1 La formalisation du langage . . . . . . . . . . . . . . . . . . . . . . . . . . . 51.1.2 La formalisation du raisonnement . . . . . . . . . . . . . . . . . . . . . . . . 5

1.2 Logique et informatique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61.3 Contenu du cours . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

2 Calcul propositionnel 72.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.2 Syntaxe du calcul propositionnel : les formules . . . . . . . . . . . . . . . . . . . . 72.3 Smantique du calcul propositionnel . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2.3.1 Modles dune formule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102.3.2 La consquence logique (dun ensemble de formules) . . . . . . . . . . . . . 122.3.3 Dcidabilit du calcul propositionnel . . . . . . . . . . . . . . . . . . . . . . 16

2.4 Equivalence entre formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172.4.1 La substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172.4.2 Equivalences classiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172.4.3 Formes normales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

2.5 Le problme SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192.5.1 Dfinition du problme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192.5.2 Un problme NP-complet . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202.5.3 Modlisation - Rduction SAT . . . . . . . . . . . . . . . . . . . . . . . . 212.5.4 Algorithmes de rsolution de SAT . . . . . . . . . . . . . . . . . . . . . . . 232.5.5 Sous-classes de SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 262.5.6 Les SAT-solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 282.5.7 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 282.5.8 Sur la modlisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

2.6 Systmes de preuve . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 322.6.1 Dfinition dun systme formel . . . . . . . . . . . . . . . . . . . . . . . . . 322.6.2 La rsolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 322.6.3 Correction, compltude et dcidabilit . . . . . . . . . . . . . . . . . . . . . 352.6.4 Systmes de preuve la Hilbert . . . . . . . . . . . . . . . . . . . . . . . . . 35

2.7 Rsum . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

3 Calcul des prdicats 433.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 433.2 Prliminaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

3.2.1 Les fonctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 433.2.2 Les relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

3.3 Un exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 443.3.1 Interprtation 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 443.3.2 Interprtation 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453.3.3 Interprtation 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453.3.4 Interprtation 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

3

4 TABLE DES MATIRES

3.3.5 Interprtation 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453.3.6 Interprtation 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 463.3.7 Comparaison des interprtations . . . . . . . . . . . . . . . . . . . . . . . . 46

3.4 Expressions et formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 463.4.1 Les termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 463.4.2 Le langage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 473.4.3 Les formules du calcul des prdicats . . . . . . . . . . . . . . . . . . . . . . 483.4.4 Occurrences libres et lies dune variable . . . . . . . . . . . . . . . . . . . . 49

3.5 Smantique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 503.5.1 Structures et valuations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 503.5.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 513.5.3 Un exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 523.5.4 Vocabulaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

3.6 Manipulation de formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 543.6.1 Substitution de variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 543.6.2 Equivalences classiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 543.6.3 Formes Normales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

3.7 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 573.7.1 Substitions et MGUs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 573.7.2 Algorithme dunification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 583.7.3 Correction et completude . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

3.8 Rsolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 613.8.1 Substitution, sur les formules propostionnelles . . . . . . . . . . . . . . . . . 613.8.2 Les rgles du calcul de la rsolution . . . . . . . . . . . . . . . . . . . . . . 623.8.3 Utilisation dun dmonstrateur automatique . . . . . . . . . . . . . . . . . . 65

4 Calculabilit 714.1 Machines de Turing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 714.2 Problmes de dcision . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 724.3 Un problme indcidable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 734.4 Thse de Chruch . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 734.5 Indecidabilit de la logique du premier ordre . . . . . . . . . . . . . . . . . . . . . . 73

Chapitre 1

Introduction

1.1 Pourquoi la logique ?

1.1.1 La formalisation du langageLe mot logique provient du grec logos (raison, discours), et signifie "science de la raison". Cette

science a pour objets dtude le discours et le raisonnement. Ceux-ci dpendent bien entendu dulangage utilis. Si on prend le langage courant, on se rend compte facilement :

quil contient de nombreuses ambiguts : nous ne sommes pas toujours srs de la smantiquedun nonc ou dune phrase. Par exemple : nous avons des jumelles la maison . (Deuxfilles ou des lunettes optiques ?) Ou il a trouv un avocat (le professionnel ou le fruit ?)

quil est dicile de connatre la vracit dun nonc : il pleuvra demain , Jean estlaid , la logique cest dur .

quil permet dnoncer des choses paradoxales :1. Je mens : comme pour tout paradoxe de ce type, on aboutit la conclusion que si

cest vrai alors cest faux. . . et inversement.2. Je suis certain quil ny a rien de certain 3. Un arrt enjoint au barbier (masculin) dun village de raser tous les hommes du village

qui ne se rasent pas eux-mmes et seulement ceux-ci. Le barbier na pas pu respectercette rgle car : sil se rase lui-mme, il enfreint la rgle, car le barbier ne peut raser que les hommes

qui ne se rasent pas eux-mmes ; sil ne se rase pas lui-mme (quil se fasse raser ou quil conserve la barbe), il est en

tort galement, car il a la charge de raser les hommes qui ne se rasent pas eux-mmes.4. Paradoxe de Russel : cest la version mathmatique du paradoxe du barbier : soit a

lensemble des ensembles qui ne se contiennent pas eux-mme. Cet ensemble nexiste pascar on peut vrifier que a 2 a ssi a /2 a.

Tout ceci fait que les langues naturelles ne sont pas adaptes au raisonnement formel. Cestpourquoi par exemple, on vous a appris un langage spcifique pour faire des preuves en mathma-tique. Une preuve mathmatique ne peut tre faite en utilisant tout le vocabulaire de la languenaturelle car les noncs et les preuves deviendraient alors ambigus. Le langage utilis en math-matique est celui de la logique classique (en ralit, cest un langage un peu plus souple, entre lalogique classique et la langue naturelle).

1.1.2 La formalisation du raisonnementUne fois le langage formalis, ce qui intresse les logiciens cest le raisonnement, et en particulier,

la dfinition de systmes formels permettant de mcaniser le raisonnement. Au dbut du 20imesicle, le rve du logicien est de faire de la logique un calcul et de mcaniser le raisonnement etpar suite toutes les mathmatiques. En 1930, Kurt Gdel met fin cette utopie en prsentant sonrsultat dincompltude : il existe des noncs darithmtique qui ne sont pas prouvable par un

5

6 Chapitre 1. Introduction

systme formel de preuve. Il nexiste donc pas dalgorithme qui permette de savoir si un noncmathmatique est vrai.

1.2 Logique et informatiqueMalgr ce rsultat ngatif, larrive de linformatique partir des annes 30 marque lessor de

la logique.Elle est prsente dans quasiment tous les domaines de linformatique : vous verrez par exemple en cours darchitecture que votre ordinateur est form de circuits

logiques. la programmation nest au fond que de la logique. Dans les anne 60, la correspondance

de Curry-Howard, tablie une correspondance preuve/programme : une relation entre lesdmonstrations formelles dun systme logique et les programmes dun modle de calcul.

le traitement automatique des langues, lintelligence artificielle, la logique apparait galement dans toutes les questions de suret.

On demande maintenant de plus en plus de prouver la suret des programmes et des pro-tocoles. Pour cela on modlise les excutions des programmes, on exprime les proprits desret par une formule logique, puis on vrifie que les modles satisfont bien la formule.A cette eet, dinnombrables logiques ont ts dveloppes, comme les logiques temporellesqui permettent de raisonner sur lvolution de certains systmes au cours du temps. Il existemme des logiques pour formaliser les rgles des pare-feu, afin dviter davoir des systmesde rgle incohrents.

et plein dautres que joublie.Il existe galement des logiciels qui permettent de prouver des formules logique (automatique-

ment ou semi-automatiquement). En particulier on a des logiciels permettant de gnrer du codevrifi : on entre une abstraction du programme a raliser, on prouve sur cette abstraction de faonplus ou moins automatique mais sre, les proprits de sret souhaites ; et le logiciel produit ducode certifi.

Linformatique est donc indissociable de la logique. Heureusement tout bon informaticien nestpas oblig dtre un bon thoricien de la logique, mais il doit tre capable maitriser son utilisation.

1.3 Contenu du coursOn sintressera principalement (des fragments de) la logique classique, qui est la logique

utilise pour les mathmatiques, et forme la base de presque toutes les autres logiques.Nous allons nous intresser aux fragment suivants : la logique propositionnelle ; la logique du premier ordre.

Pour chacune de ces logiques, nous nous poserons principalement les questions suivantes : Quelle est sa syntaxe ? I.e., comment crire une phrase dans le langage de la logique considr. Quel est sa smantique ? Cest--dire, tant une phrase, savoir lui attribuer un sens. Cette

question ouvre une autre qui est "de quel forme sont les modles dune formule", cest dire : mon langage parle dobjets, qui se placent dans un univers prcis : quel est cetunivers ?

La logique est elle-dcidable ? Etant donn une phrase (formule) du langage, existe-il uneprocdure eective permettant dvaluer cette formule.

Existe-il un systme formel de calcul permettant de "prouver" quun nonc est vrai oufaux.

Dautres questions se posent videment mais se sont principalement celles-ci qui intressent lin-formaticien.

Chapitre 2

Calcul propositionnel

2.1 IntroductionLes formules (ou phrases, ou enoncs) du calcul propositionnel sont de deux types : ou bien

une formule est une proposition atomique, ou bien elle est compose partir dautres formules laide des connecteurs logiques ^,,_,) (et , non, ou, implique, que lon appelle connecteurspropositionnels).

Considrons, par exemple, lnonce arithmtique 2+2 = 4 ou 3+3 = 5 . Cette formule peutse considrer comme construite des propositions atomiques 2+2 = 4 et 3+3 = 5 , via leconnecteur propositionnel ou. Une analyse similaire peut se faire pour les noncs du langagenaturel. On considre lnonce sil pleut, alors le soleil se cache , que lon reconnatra trequivalent il pleut implique que le soleil se cache , comme obtenu des deux propositionsatomiques sil pleut et le soleil se cache via le connecteur propositionnel implique.

Une proposition atomique est un nonc simple, ne pouvant prendre que les valeurs "vrai" ou"faux ", et ce de faon non ambigu ; elle donne donc une information sur un tat de chose. Deplus une proposition atomique est indcomposable : le ciel est bleu et lherbe est verte nestpas une proposition atomique mais la composition de deux propositions atomiques. Dans lanalysedu langage naturel, on ne peut pas considrer comme des propositions : les souhaits, les phrasesimpratives ou les interrogations.

Nous avons dj vu des exemples de formules composes. Considrons maintenant lnonc sil neige, alors le soleil se cache et il fait froid . Cest une formule compose, via le connecteurimplique, depuis la formule atomique il neige et la formule compose le soleil se cache et il faitfroid . On peut donc composer des formules partir dautres formules composes. La valeur devrit dune formule compose se calcule comme une fonction de formules dont elle est compose.

Le calcul des propositions est la premire tape dans la dfinition de la logique et du rai-sonnement. Il dfinit les rgles de dduction qui relient les phrases entre elles, sans en examinerle contenu ; il est ainsi une premire tape dans la construction du calcul des prdicats, qui luisintresse au contenu des propositions.

Nous partirons donc en gnral de faits : "p est vrai, q est faux" et essaierons de dterminer siune armation particulire est vraie.

2.2 Syntaxe du calcul propositionnel : les formulesLe langage du calcul propositionnel est form de : symboles propositionnels Prop = {p1, p2, . . .} ; connecteurs logiques {,^,_,)} ; symboles auxiliaires : parenthses et espace.

Remarque 2.1. Dans la littrature logique on utilise plusieurs synonymes pour symbole proposi-tionnel ; ainsi variable propositionnelle, proposition atomique, formule atomique, ou encore atomesont tous des synonymes de symbole propositionnel.

7

8 Chapitre 2. Calcul propositionnel

Lensemble Fcp des formules du calcul propositionnel est le plus petit ensemble tel que : tout symbole propositionnel est une formule ; si ' est une formule alors ' est une formule ; si ', sont des formules alors ' _ , ' ^ et ') sont des formules.

Les symboles auxiliaires ne sont utiliss que pour lever les ambiguts possibles : par exemple,la formule p_ q^ r est ambigu, car elle peut se lire de deux faons direntes, ((p_ q)^ r) ou bien(p _ (q ^ r)).Exemple. p, p) (q _ r) et p _ q sont des formules propositionnelles ; (_q) et f(x)) g(x) nensont pas.

A cause de la structure inductive de la dfinition, une formule peut-tre vue comme un arbredont les feuilles sont tiquets par des symboles propositionnels et les noeuds par des connecteurs.Par exemple, la formule p) (q ^ r) correspond larbre reprsent Figure 2.2.

q

p ^

)

r

Figure 2.1 Reprsentation arborescente de la formule p) (q ^ r)

Notation 2.2. On utilise souvent en plus le connecteur binaire, comme abrviation : ', estlabrviation de (') ) ^ ( ) '). De la mme faon, on ajoute le symbole ? qui correspond Faux et le symbole > qui correspond Vrai. Ces deux symboles sont aussi des abrviations, ils nesont pas indispensables au langage. (Par exemple ? peut tre utilis la place de p^p et > laplace de p _ p.)Dfinition 2.3 (Sous-formule). Lensemble SF (') des sous-formules dune formules ' est dfinipar induction de la faon suivante.

SF (p) = {p} ; SF (') = {'} [ SF (') ; SF (' ) = {' } [ SF (') [ SF ( ) (o dsigne un des symboles ^, _, )).

Par exemple, SF (p) (q ^ r)) = {p, q, r,q,q ^ r, p) (q ^ r)}. Quand on voit une formulecomme un arbre, une sous-formule est simplement un sous-arbre (voir Figure 2.2).

Dfinition 2.4 (Sous-formule stricte). est une sous-formule stricte de ' si est une sous-formulede ' qui nest pas '.

2.3 Smantique du calcul propositionnelIl faut maintenant un moyen de dterminer si une formule est vraie ou fausse. La premire

tape est de donner une valeur de vrit aux propositions atomiques. Lvaluation dune formule,dpend donc des valeurs choisies pour les symboles propositionnels. Ces valeurs sont donnes parune valuation.

Dfinition 2.5 (Valuation). Une valuation est une application de Prop dans {0, 1}. La valeur 0dsigne le "faux" et la valeur 1 dsigne le "vrai".

2.3 Smantique du calcul propositionnel 9

q

p ^

)

r

Figure 2.2 Reprsentation arborescente des sous-formules de p) (q ^ r)

Une valuation sera souvent donne sous forme dun tableau. Par exemple, si Prop = {p, q}alors la valuation v : p 7! 1, q 7! 0 scrit plus simplement v : p q1 0

Une fois la valuation v choisie, la valeur de la formule se dtermine de faon naturelle, parextension de la valuation v aux formules de la faon suivante :

Dfinition 2.6 (Valeur dune formule). v(') = 1 ssi v(') = 0 ; v(' _ ) = 1 ssi v(') = 1 ou v( ) = 1 ; v(' ^ ) = 1 ssi v(') = 1 et v( ) = 1 ; v(') ) = 0 ssi v(') = 1 et v( ) = 0.

La dfinition prcdente peut apparatre trompeuse car circualire : afin dexpliquer la logique,nous somme en train de lutiliser (ssi, ou, et . . . ). Par ailleurs, on peut se servir de la dfinitionsuivante qui est en eet quivalente la Dfinition 2.6 :

Dfinition 2.7 (Valeur dune formule (bis)). v(') = 1 v(') ; v(' _ ) = max(v('), v( )) ; v(' ^ ) = min(v('), v( )) ; v(') ) = v(' _ ).

Cette dernire dfinition est purement combinatoire car elle repose sur la structure de lensembleordonn fini { 0 < 1 } ; nous supposons en fait que cette structure est tellement vidente et claireper se quil ny a pas besoin de la justifier autrement.

Exercice 2.8. Proposez un algorithme qui, tant donn une formule ' du calcul propositionnel etune valuation v, calcule v('). Quel type de structure de donnes utiliser pour coder les formules ?Quel type de structure de donnes utiliser pour coder les valuations ?

Notez que la dfinition 2.7 correspond aux tables de vrit des connecteurs logiques (dont vousavez srement entendu parler) :

p p0 11 0

p q p ^ q0 0 00 1 01 0 01 1 1

p q p _ q0 0 00 1 11 0 11 1 1

p q p) q0 0 10 1 11 0 01 1 1

Remarque 2.9. Remarquez la dfinition particulire de limplication : on lentend en gnralcomme un "si ..., alors ...", on voit ici que lnonc "si 1+1=1, alors la capitale de la France estMarseille" est vrai, puisque toute phrase ') est vraie ds lors que ' est value faux. Ceci est

10 Chapitre 2. Calcul propositionnel

peu naturel, car dans le langage courant, on ne sintresse la vrit dun tel nonc que lorsquela condition est vraie : "sil fait beau je vais la pche" na dintrt pratique que sil fait beau. . .Attribuer la valeur vrai dans le cas ou la prmisse est fausse correspond a peu prs lusage du si.. alors dans la phrase suivante : "Si Pierre obtient sa Licence, alors je suis Einstein" : cest direque partant dune hypothse fausse, alors je peux dmontrer des choses fausses (ou vraies). Parcontre, il nest pas possible de dmontrer quelque chose de faux partant dune hypothse vraie.

On peut ajouter la dfinition de la valeur de labrviation , : v(' , ) = 1 ssi v(') = v( ).Ce qui correspond la table de vrit suivante :

p q p, q0 0 10 1 01 0 01 1 1

Exercice 2.10. Dfinissons lensemble Prop('), des variables propositionnelles contenues dans' 2 Fcp, par induction comme suit :

Prop(p) = { p } ,Prop(') = Prop(') ,

Prop(' ) = Prop(') [ Prop( ) , 2 {^,_,) } .Montrez que :

Prop(') = Prop \ SF ('), pour tout ' 2 Fcp ; si v(p) = v0(p) pour tout p 2 Prop('), alors v(') = v0(').

2.3.1 Modles dune formuleDfinition 2.11. Lensemble des valuations dun ensemble de variables propositionnelles Propest not Val(Prop) (ou juste Val lorsquil ny a pas dambiguit sur Prop). Val(Prop) est donclensemble des fonctions de Prop dans {0, 1}.

Par exemple, si Prop = {p, q, r}, alors Val est reprsent par la Table 2.3.1, dans lequel chaqueligne est une valuation de Prop :

p q r0 0 00 0 10 1 00 1 11 0 01 0 11 1 01 1 1

Table 2.1 Lensemble Val(Prop) des valuations de Prop = {p, q, r}

Dfinition 2.12 (Modle dune formule). Unmodle de ' est une valuation v telle que v(') = 1.On note mod(') lensemble des modles de '.

Exemple. Si Prop = {p, q, r} et ' = (p _ q) ^ (p _ r) alors lensemble des modles de ' est

mod(') =

p q r0 1 01 0 01 1 11 1 01 1 1

2.3 Smantique du calcul propositionnel 11

Dfinition 2.13 (Satisfaisabilit). Une formule ' est satisfaisable (ou consistante, ou encorecohrente) si elle admet un modle (i.e., si il existe une valuation v telle que v(') = 1, i.e. simod(') 6= ?).Dfinition 2.14 (Insatisfaisabilit). Une formule ' est insatisfaisable (ou inconsistante, ouincohrente) si elle nadmet aucun modle (i.e., si pour toute valuation v, v(') = 0, i.e., simod(') = ?)

Dfinition 2.15 (Tautologie). Une formule ' est une tautologie (ou valide) si v(') = 1 pourtoute valuation v (i.e., si mod(') = Val). On note |= ' pour dire que ' est une tautologie.

Un exemple de tautologie est ' _ ', cest dire le tiers exclus.Exercice 2.16. Montrez que les formules suivantes sont des tautologies :

p) p , p) (q ) p) , (p) (q ) r))) ((p) q)) (p) r)) , ((p) q)) p)) p .Dfinition 2.17 (Equivalence). On dit que ' est quivalente si les deux formules ont lesmmes modles (i.e. si mod(') = mod( )). On note alors ' .Exemple. Les oprateurs ^, _ sont associatifs-commutatifs. Deux formules identiques associativit-commutativit prs sont quivalentes. Remplacer une sous-formule dune formule ' par une for-mule quivalente 0 donne une formule note '[ 0]. Cette substitution prserve les modles,i.e., mod(') = mod('[ 0]).Exercice 2.18. crivons ' si v(') = v( ) pour toute valuation v (voir dfinition 2.17).Montrez :

' _ ? ' ' ^ ? ? (' ^ ) ^ ' ^ ( ^ )' _ > > ' ^ > ' (' ^ ) _ (' ^ ) _ ( ^ )' _ _ ' ' ^ ^ ' (' _ ) ^ (' ^ ) _ (' ^ )' _ ' ' (' _ ) (') ^ ( ) (' _ ) _ ' _ ( _ )' ' ' ^ ' ' (' ^ ) (') _ ( ) .

Proposition 2.19. Soient ' et deux formules, on a :1. mod(') = Val mod(') ;2. mod(' _ ) = mod( ) [ mod( ) ;3. mod(' ^ ) = mod( ) \ mod( ) ;4. |= ') ssi mod(') mod( ).

Dmonstration. 1. pour toute valuation v 2 Val,v 2 mod(') ssi v(') = 1

ssi v(') = 0ssi v /2 mod(')ssi Val mod(')

2. pour toute valuation v 2 Val,v 2 mod(' _ ) ssi v(') = 1 ou v( ) = 1

ssi v 2 mod(') ou v 2 mod( )ssi mod(') [ mod( )

3. pour toute valuation v 2 Val,v 2 mod(' ^ ) ssi v(') = 1 et v( ) = 1

ssi v 2 mod(') et v 2 mod( )ssi mod(') \ mod( )

12 Chapitre 2. Calcul propositionnel

4.

|= ') ssi pour toute valuation v 2 Val, v(') ) = 1ssi pour toute valuation v 2 Val, v(' _ ) = 1ssi pour toute valuation v 2 Val, v(') = 0 ou v( ) = 1ssi pour toute valuation v 2 Val, v(') v( )ssi mod(') mod( )

Dfinition 2.20 (Consquence logique). Une formule est consquence logique dune formule' si tout modle de ' est un modle de (i.e., si mod(') mod( )). On note alors ' |= .Remarque 2.21. Attention la confusion dans les deux notations !

v |= ' o v est une valuation, i.e., lassignation dune valeur aux propositions atomiquesde la formule ; cest un raccourcis assez frquent pour v(') = 1 ; |= ' o est une formule.

Proposition 2.22. Soient ' et deux formules propositionnelles.1. ' |= si et seulement si |= ') .2. ' si et seulement si |= ', .

Dmonstration. 1. Consquence directe du point 4 de la Proposition 2.192. |= ', ssi 8v 2 Val, v(', ) = 1 (par la dfinition de tautologie) ssi 8v 2 Val, v(') = v( )

(par la table de verit de ,) ssi 8v 2 Val, v 2 mod(') ssi v 2 mod( ) ssi mod(') = mod( )ssi '.

2.3.2 La consquence logique (dun ensemble de formules)Les formules propositionnelles peuvent tre vues comme un ensemble de contraintes sur les

propositions. Ainsi, p ^ q contraint p et q tre vraies. Il est donc trs courant de considrer desensembles de formules propositionnelles pour modliser des problmes de satisfaction de contraintes.

On tend les dfinitions vues prcdemment aux ensembles de formules.

Dfinition 2.23 (Modle). Un modle dun ensemble de formules est une valuation v telle quev(') = 1 pour tout ' 2 . On note mod() lensemble des modles de .

Cet ensemble de modles est donc lensemble des valuations quon peut attribuer aux variablessi on veut respecter toutes les contraintes de .

Dfinition 2.24 (Satisfaisabilit/Consistance). Un ensemble de formules est satisfaisable (ouconsistant, ou cohrent) si il admet au moins un modle (i.e., si mod() 6= ?)Dfinition 2.25 (Insatisfaisabilit/Contradiction). Un ensemble de formules est insatisfaisable(ou contradictoire, ou inconsistant, ou encore incohrent) si il nadmet aucun modle ( i.e.,si mod() = ?), on note alors |=?.

Un ensemble contradictoire ne peut tre satisfait : par exemple lensemble = {p,p} estinsatisfaisable.

Dfinition 2.26 (Consquence logique). Une formule ' est consquence logique de si et seule-ment si toute valuation qui donne 1 toutes les formules de donne 1 ' (i.e., si mod() mod(')),on note alors |= '. On note cons() lensemble des consquences logiques de .Remarque 2.27. Attention la confusion dans les notations !

v |= ' o v est une valuation : cette notation est souvent utilise pour dire que v rendvraie la formule ' ; elle est donc une autre notation pour v(') = 1 1 ; |= ' o est une formule ; |= ' o est un ensemble de formule.

1. Dans ce texte, nous essayerons dviter cette notation.

2.3 Smantique du calcul propositionnel 13

Remarquez, par ailleurs que ' |= si, et seulement si, {' } |= ; les derrires notations sont donccohrentes entre elles.

Une consquence logique ' dun ensemble est une nouvelle contrainte dduite directementde . Puisquelle dcoule de , elle ne peut pas apporter de contraintes supplmentaires que cellesapportes par . En particulier, les modles de et ceux de [ {'} sont exactement les mmes(cette intuition sera prouve formellement avec la Proposition 2.32).

Par exemple, si = {(p) s)_ q,q}, on peut en dduire que p) s. Bien entendu, les modlesde sont exactement les modles de [ {p) s}.

Ceci implique donc galement une mthode de simplification dun ensemble de formule, si contient une formule ' consquence logique de {'}, alors ' peut tre retire de lensemble decontraintes sans en modifier la smantique : mod() = mod( {'}).Proposition 2.28. |= ' ssi [ {'} est contradictoire.Dmonstration. |= ' ssipour toute valuation v

soit v est un modle de et v(') = 1 soit v nest pas un modle de

ssi pour toute valuation v soit v est un modle de et v(') = 0 soit v nest pas un modle de

ssi pour toute valuation v, v nest pas un modle de [ {'}ssi [ {'} est contradictoire.Proposition 2.29. Pour tous ensembles de formules , ,

mod( [ ) = mod() \ mod().En particulier, si alors mod() mod().

Cette proposition se comprend bien si on voit un ensemble de formules comme un ensemble decontraintes sur les variables propositionnelles. Plus on ajoute de contraintes, et moins il reste depossibilits pour rsoudre ces contraintes.

Dmonstration. Pour toute valuation v :

v 2 mod( [ ) ssi pour tout ' 2 [ , v(') = 1ssi pour tout ' 2 , v(') = 1 et pour tout 2 , v( ) = 1ssi v 2 mod() et v 2 mod()ssi v 2 mod() \ mod().

Les preuves des propositions suivantes sont laisses en exercice.

Proposition 2.30. Si 0 et 0 |= ', alors |= '.Proposition 2.31. {'1, . . .'n} |= ssi |= ('1 ^ . . . ^ 'n))

Cette proposition exprime le fait quun ensemble fini de formules propositionnelles peut toujourstre vu comme une seule formule forme de la conjonction des formules de lensemble. Une formuletant un objet fini, ce rsultat ne se gnralise pas au cas des ensembles de taille non borne. Dansle cas o est infini, il faudra utiliser le thorme de compacit (Thorme 2.35) qui permet deramener les problmes de satisfaisabilit et de contradiction dun ensemble de taille quelconque celle densemble finis.

Dmonstration. Remarquons que

mod({'1, . . . ,'n }) = mod({'1 } [ . . . [ {'n })= mod({'1 }) \ . . . \ mod({'n })= mod('1) \ . . . \ mod('n) = mod('1 ^ . . . ^ 'n) .

Donc, on a que mod({'1, . . . ,'n }) mod( ) si et seulement si mod('1 ^ . . . ^ 'n) mod( ) et,par la Proposition 2.19, la dernire relation est vraie ssi ('1^ . . .^'n)) est une tautologie.

14 Chapitre 2. Calcul propositionnel

Proposition 2.32. |= ' si, et seulement si, mod() = mod( [ {'}).Dmonstration. La proposition decoule du fait que mod( [ {'}) = mod() \ mod({'}), et que larelation mod() mod(') est equivalenete mod() \ mod({'}) = mod().Exemple. Avec cet exemple, nous allons tirer avantage des propositions et remarques prcdentespour rsoudre un ensemble de contraintes ayant une certaine complexit.

On dispose de 4 variables propositionnelles, pA, pB , pC , PD, qui obissent aux contraintes sui-vantes :

'1 : pB ^ pC'2 : pA ) (pC _ pD)'3 : pC ^ (pB _ pA)

Soit 1 = {'1,'2,'3}, cet ensemble forme lensemble des prmisses partir desquelles nousallons essayer de dduire les valeurs que les variables propositionnelles peuvent prendre.

On se pose les questions suivantes :1. Peut-on simplifier lensemble 1 de faon ne pas changer lensemble de ses modles, et donc

de ses consquences ?(a) On remarque que la contrainte '3 est une consquence logique de la contrainte '1.

En eet, pour toute valuation v, v satisfait '1 ssi v(pC) = 0 et v(pB) = 1, v satisfait '3 ssi v(pC) = 0 et (v(pA) = 1 ou v(pB) = 1).Do, mod('1) mod('3).

(b) Soit 2 = {'1,'2}, on a mod(2) = mod(1). En eet, par dfinition,mod(1) = mod('1) \ mod('2) \ mod('3) = mod('1) \ mod('2) = mod(2).Donc les consquences de 1 et 2 sont les mmes et on peut alors simplifier 1 par 2.

2. Quel est lensemble des modles de 2 ?Modles de '1 :pA pB pC pD0 1 0 00 1 0 11 1 0 01 1 0 1

Modles de '2 :pA pB pC pD0 0 0 00 0 0 10 0 1 00 0 1 10 1 0 00 1 0 10 1 1 00 1 1 11 0 0 11 0 1 01 0 1 11 1 0 11 1 1 01 1 1 1

Lensemble M des modles de 2 est lintersections des modles de '1 et '2 :pA pB pC pD0 1 0 11 1 0 1

3. 2 est-il consistant ? contradictoire ?2 admet un modle, il est donc consistant et non contradictoire.

4. Quelles consquences logiques pouvons nous tirer de lensemble 2 ?Les consquences logiques de 2 sont toutes les formules dont lensemble des modles contientM . On a donc entre autres :pC , pB , pB ^ pC 2 cons()

5. Ajoutons maintenant une nouvelle contrainte : 3 = {pB ^ pD} [ 2. On a mod(3) =mod(2) \ mod(pB ^ pD) = ?. Donc mod(3) = ? et 3 est contradictoire.

2.3 Smantique du calcul propositionnel 15

2.3.2.1 Compacit

Le thorme de compacit sert caractriser la consquence logique dans les cas o lensembledes formules est infini en ne considrant que des sous-ensembles finis. Par ailleurs, ce thormejouera un rle cruciale plus tard, dans la preuve du thorme de compltude pour la calcul de larsolution (Thorme ??).

Le thorme de compacit Pour commencer, nous avons besoin du lemme suivant appelLemme de Knig.

Lemme 2.33. Tout arbre infini branchement fini possde une branche infinie.

Dmonstration. Supposons que T , qui est branchement fini, soit infini. On dfinit une brancheinfinie dans T , ce qui mnera la conclusion.

Pour cela, on montre par induction la proprit suivante :

P(n) : := il existe une branche e0, . . . en telle que le sous arbre issu de en est infini.

Pour n = 0, on choisit e0 = r (la racine de larbre) qui par hypothse est racine dunarbre infini. On suppose P(n) et on montre P(n+1) : Par hypothse, il existe une branche e0, . . . en telleque le sous arbre issu de en est infini. Considrons les successeurs immdiats de en, disonsen1 , . . . , enk : si tous taient racines de sous-arbres finis, disons de cardinaux p1, . . . , pk, alorsil en serait de mme de en (avec un cardinal dau plus p1 + ...+ pk+1), contradiction. Donclun dentre eux est le en+1 recherch.

Nous aurons besoin du Lemme dans la forme suivante :

Lemme 2.34. Tout arbre a branchement fini et dont toutes les branches sont finies, est fini.

Thorme 2.35 (Compacit). Un ensemble de formules propositionnelles est satisfaisable ssitout sous-ensemble fini de est satisfaisable.

Par contrapose, le thorme de compacit peut snoncer de la faon suivante :

Thorme 2.36 (Compacit). Un ensemble de formules propositionnelles est contradictoire ssiil existe un sous-ensemble fini de contradictoire.

Remarquons que limplication si un sous-ensemble fini de est contradictoire, alors estcontradictoire est trivialement vraie. Nous nous limiterons prouver limplication inverse.

Dmonstration. On fait la preuve dans le cas dnombrable.Nous avons besoin dune construction importante appele "arbre smantique" ou "arbre de

Herbrand". Considrons un ensemble dnombrable datomes {p0, p1, p2, . . . , pn, . . .}. Larbre s-mantique associ est un arbre binaire infini dont toutes les artes gauches sont tiquetes "faux"et celles droites sont tiquetes "vrai". Chaque niveau de larbre est associ une proposition.La racine (le niveau 0) est associ p0 : chaque fois que lon descend dun noeud de niveau pi, cecirevient poser pi faux si lon descend gauche, et pi vrai si lon descend droite.

Chaque chemin infini partant de la racine correspond une valuation de lensemble despropositions. Chaque noeud e profondeur n correspond une valuation ve des variables {p0, . . . pn1}. Nous appelons un noeud e noeud dchec si sa profondeur est n et il existe une formule'e 2 telle que Prop('e) { p0, . . . pn1 } et ve('e) = 0.

On suppose que est inconsistante et on montre quil existe un sous-ensemble 0 fini etinconsistant.

On commence par remarquer que chaque branche contient un noeud dchec. En eet, si unebranche nen contient pas, elle dfinit un modle de , ce qui est contradictoire lhypothse.

On peut donc faire la construction suivante : Prenons le premier noeud dchec de chaquebranche et tiquetons le par une formule de fausse sur ce noeud, puis coupons larbre au niveaudu noeud dechec.

16 Chapitre 2. Calcul propositionnel

Larbre obtenu en tronquant ainsi toutes les branches est un arbre branchement fini, sesbranches sont finies donc il est fini. Le sous-ensemble 0 des formules de tiquetant les feuilles delarbre est donc fini. Or toutes les feuilles de larbre sont des noeuds dchec et donc chacune desvaluations rend fausse au moins une des formules de 0. Lensemble 0 est fini et inconsistant

Corollaire du thorme de compacit :

Corollaire 2.37. Une formule ' est consquence dun ensemble de formules si et seulement siil existe un sous-ensemble fini fini de tel que fini |= '.Dmonstration.

|= ' ssi [ {'} est contradictoiressi il existe f [ {'} fini et contradictoiressi il existe f fini tel que f [ {'} est contradictoiressi il existe un sous-ensemble fini f tel que f |= ' .

2.3.3 Dcidabilit du calcul propositionnelUne logique est dcidable sil existe un algorithme (calcul ralisable sur un ordinateur qui

termine toujours pour toute donne) qui permet de savoir pour chaque formule si elle est unetautologie (i.e. si |= ') ou pas.Thorme 2.38. Le calcul propositionnel est dcidable.

Dmonstration. Mthode des tables de vrit : calculer la table de vrit prenant en argument lessymboles propositionnels de ' et calculer pour chaque valuation possible la valeur de '.

Cot : O(2n) avec n la taille de ' (nombre de propositions).

Nous verrons par la suite quil y a de meilleurs algorithmes, mais quil ont tous un cot ex-ponentiel. La plupart de ces algorithmes dbutent par une premire phase de normalisation de laformule, cest dire quon modifie la syntaxe de la formule de manire la mettre sous une formenormalise, tout en conservant la smantique de la formule, cest--dire lensemble de ses modles.