Previous Up Next
Eléments de logique pour l’informatique 2019–20                  http://www.lri.fr/~paulin/Logique


Chapitre 1  Introduction au langage logique

La logique s’intéresse à la notion de raisonnement. Un raisonnement est un discours qui permet d’établir la vérité d’un fait. Dans ce cours, nous nous intéressons à la logique mathématique qui s’appuie sur un langage formel et un ensemble de règles fixé. Le raisonnement ne sera donc pas un discours en langue naturel mais une suite bien précise de constructions qui obéissent aux règles du jeu.

Dans ce chapitre nous introduisons le langage et les notions de base. Nous reviendrons ensuite plus en détail sur deux systèmes logiques importants : le calcul propositionnel et le calcul des prédicats.

1.1  Définition du langage

Une formule décrit une propriété (vraie ou fausse) qui parle d’objets (par exemple des entiers, des objets géométriques, mais aussi des ensembles, des fonctions …). Pour décrire les objets, on dispose de constantes comme 0, 1, ∅…, d’opérations +, ×, ∪,…On utilise également des variables d’objets qui sont des symboles permettant de nommer des objets arbitraires comme par exemple dans x+1.

On utilisera un langage formel pour écrire les propositions afin d’éviter les ambiguïtés du langage naturel ou des notations imprécises. Dans le langage naturel, le même mot peut refléter des situations logiques différentes.

Un langage formel présente également moins de redondance que le langage naturel dans lequel la même situation logique peut s’exprimer de plusieurs manières différentes. Les langages formels sont donc plus simples à étudier.

Formules atomiques

Les formules atomiques incluent (la propriété vraie) et (la propriété fausse). Ce sont des formules qui peuvent être vraies ou fausses que l’on ne peut pas décomposer sur une base logique. Il s’agit plutôt de notions que l’on observe.

Lorsqu’on étudie la logique, on introduit des symboles comme base des formules atomiques. Ces symboles peuvent être des variables propositionnelles ((xy) ⇒ x) ou bien des symboles de prédicat qui sont appliqués à des termes pour former des propositionns atomiques.

Par exemple si dans un problème on cherche à modéliser la situation textitPaul est mon ami, alors il suffit d’introduire une variable propositionnelle (qui pourra être vraie ou fausse) et qui représente le fait que Paul est (ou non) mon ami. Si par contre on veut modéliser une phrase comme textittous mes amis habitent Paris, alors il faut un symbole de prédicat unaire ami tel que ami(t) est vrai lorsque t est mon ami et un prédicat unaire paris tel que paris(t) est vrai lorsque t habite Paris, en introduisant en plus une constante Paul on peut facilement traduire la notion Paul est mon ami. Si maintenant la propriété à montrer est textitles amis de mes amis sont mes amis alors il faudra passer à un symbole de relation binaire tels que amis(t,u) est vrai si t et u sont amis et utiliser une constante self pour représenter la personne qui s’exprime.

On aura souvent un symbole de prédicat binaire pour représenter l’égalité =, on peut aussi avoir un symbole pour la comparaison . Un symbole de prédicat associé à un ou plusieurs objets (le nombre d’objets attendus s’appelle l’arité du prédicat) est une formule atomique.

Exemple 1 (Formules atomiques)   0 = 1, 2+2 = 4, x = x, x = y, x + 1 ≤ x, x est un entier pair.
Formules complexes

Les formules complexes se construisent à partir des formules atomiques à l’aide de connecteurs logiques. On distingue la partie dite propositionnelle :

Et les quantificateurs du premier ordre :

La quantification universelle peut se voir comme une conjonction généralisée sur tous les x possible (il peut y en avoir une infinité, pas forcément dénombrable). La quantification existentielle peut se voir comme une disjonction généralisée.

Exemple 2 (Formules complexes)   
Exercice 1  
Notations, règles de parenthésage

On utilisera la notation AB pour la formule (AB) ∧ (BA).

On peut introduire plusieurs variables dans un quantificateur, par exemple : x  y, P représente la formule x, ∀ y, P.

La définition que l’on a donnée explique une méthode de construction des formules à partir des formules atomiques. Néanmoins si on écrit simplement PQR il y a une ambiguïté: cette formule peut se construire de deux manières différentes suivant si on utilise d’abord la règle pour la disjonction puis la conjonction ou bien dans l’autre sens. Pour lever cette ambiguïté, on utilise des parenthèses et on pourra écrire (PQ) ∨ R ou bien P ∧ (QR) Les parenthèses sont importantes car les deux formules ne sont pas vraies en même temps (prendre P faux et Q et R vrai).

Comme pour les formules arithmétiques, il y a des règles de précédence pour les connecteurs logiques qui évitent l’utilisation systématique des parenthèses. La précédence de ¬ est la plus forte, vient ensuite la conjonction puis la disjonction et finalement l’implication . Ces connecteurs associent à droite.

Exemple 3   PR ∧ ¬ QPQR représente donc la même formule que (P ∧ (R ∧ (¬ Q))) ⇒ (P ∨ (QR)).

Les quantificateurs et ont une précédence plus faible que les autres opérateurs. Leur portée s’étend donc aussi loin que possible.

Exemple 4   x, PQ représente x, (PQ).
Exercice 2  
  1. Ajouter des parenthèses aux formules suivantes sans changer leur sens:
    1. Formule A définie comme étant (PQR) ⇒ PQR
    2. (PQ) ⇒ ¬ Q ⇒ ¬ P
  2. Exprimer sous une forme logique l’adage suivant: “Tout ce qui ne nous tue pas nous rend plus fort”. On se donne comme prédicat de base Tue(x) et Fort(x) Écrire la formule avec toutes les parenthèses puis avec le minimum de parenthèses.
Exercice 3   On suppose que l’on se place dans un langage avec les prédicats ami(x,y) et joue(x,y) qui représentent le fait que x est l’ami de y et que x joue avec y. On introduit également une constante self qui représente l’individu qui s’exprime. Traduire en formules logiques les expressions suivantes :
  1. les amis de mes amis sont mes amis
  2. je ne joue qu’avec mes amis
  3. je n’ai pas d’ami
  4. je n’ai qu’un ami (on pourra de plus utiliser la relation d’égalité)
  5. tout le monde a un ami

1.2  Structure des formules

Une formule peut se voir comme un arbre dont les nœuds internes sont les connecteurs (les connecteurs propositionnels sont binaires, sauf la négation qui est unaire) et les quantificateurs x, ∃ x et dont les feuilles sont les formules atomiques.

On peut ainsi dessiner sous forme d’arbre la formule (PQ ⇒ ∀ x, R) ⇒ P ∧ ∃ x, QR de l’exercice 2 :

Cette représentation arborescente pourra être utilisée si on veut représenter les formules en machine. C’est aussi elle qui va nous servir pour construire des fonctions sur les formules et aussi pour raisonner sur les formules.

Exercice 1   Donner la forme arborescente de la formule (∀ x, PQ) ⇒ ¬ Q ⇒ ¬ ∃ x, P.
Variables libres, liées.

Dans les formules x, P et x, P, la variable x est dite liée, en effet les occurrences de x sont reliées au quantificateur correspondant et on peut changer le nom de manière cohérente dans P et le quantificateur sans changer le sens de la formule:
x, ∃ y, x < y exprime la même propriété que t, ∃ u, t < u. Une variable x qui apparaît dans une formule P mais qui n’est pas dans une sous-expression de la forme x, Q ou x, Q est dite libre. Par exemple dans la formule y, x < y, la variable x est libre et y est liée.

Définition 1 (Variables libres, Vl(P))   Soit une formule P et x une variable. On dit que x est libre dans la formule P et on écrira xVl(P) si:
Attention:

une variable peut à la fois apparaître en position libre et en position liée, ou bien apparaître liée dans plusieurs quantificateurs comme y dans la formule 0<x× y ∨ (∃ y, x < y) ∧ (∃ y, y+y < x). Cependant ces trois positions ne représentent pas la même chose car on peut toujours choisir un nom nouveau pour les variables liées. La formule pourra s’écrire: 0<x× y ∨ (∃ y1, x < y1) ∧ (∃ y2, y2+y2 < x).

Exercice 2   Donner les variables libres de la formule : b, b > 0 ⇒ ∃ q, ∃ r, a = b × q + rr < b.
Définition récursive sur les formules.

On peut définir une fonction f de Prop dans un ensemble A en se donnant un ensemble d’équations que doit satisfaire cette fonction. Les équations sont de la forme f(t)=u. Il y a une équation pour chacune des constructions possibles de formule: formules atomiques (en particulier , ), formules propositionnelles ¬ P, PQ …formules quantifiées x, P, x, P. Dans le cas des connecteurs logiques et des quantificateurs, le membre droit u peut utiliser la valeur de f sur des sous-formules de t (comme f(P) et f(Q)). On parle de définition récursive.

On peut par exemple définir une fonction qui compte le nombre de connecteurs propositionnels dans une formule :

nbsymb(P)=0     si P atomique 
nbsymb(¬ P)=1+ nbsymb(P
   
nbsymb(P∧ Q)=1+ nbsymb(P)+nbsymb(Q
nbsymb(P∨ Q)=1+ nbsymb(P)+nbsymb(Q
nbsymb(P⇒ Q)=1+ nbsymb(P)+nbsymb(Q)
nbsymb(∀ xP)nbsymb(P
nbsymb(∃ xP)nbsymb(P

Ce qui est important dans cette définition est qu’elle est complète car elle couvre tous les cas de formules, que pour chaque formule il n’y a qu’une seule équation qui s’applique et donc que la définition est non-ambigüe et finalement on dit qu’elle est bien fondée car les références à la fonction f dans les membres droits des équations se font sur des formules strictement plus petites que le membre gauche.

Ces équations définissent également un moyen de calcul de la valeur de f pour une formule donnée. Par exemple dans le cas de la formule A de l’exercice 2 on aura nbsymb(A)=5.

Exercice 3   Donner les équations qui définissent la profondeur prof(A) d’une formule A, c’est-à-dire qui donne le nombre maximal de connecteurs imbriqués. Dans le cas de la formule A de l’exercice 2 on aura prof(A)=3.
Raisonner sur les formules.

Pour établir un résultat pour toutes les formules, on peut utiliser un raisonnement par récurrence sur la structure de la formule. Soit une propriété φ(P) qui dépend d’une formule P.

Ce principe de preuve est très utile lorsque l’on veut montrer des propriétés qui parlent de fonctions sur les formules qui sont elles-mêmes définies récursivement.

Exemple 1   On peut définir de manière récursive le nombre de formules atomiques dans une formule logique :
nbatom(p)=1     si p atomique 
nbatom(¬ P)=nbatom(P
nbatom(∀ xP)=nbatom(P
   
nbatom(P∧ Q)=nbatom(P)+nbatom(Q
nbatom(P∨ Q)=nbatom(P)+nbatom(Q
nbatom(P⇒ Q)=nbatom(P)+nbatom(Q)
nbatom(∃ xP)=nbatom(P
On peut ensuite montrer que pour toute formule P, on a nbatom(P)≤ 1+nbsymb(P).

1.3  Formule vraie

Pour définir quand une formule est vraie, il faut se placer dans un modèle qui explicite de quels objets on parle et également pour chaque symbole de prédicat, nous dit pour quels objets il est vérifié.

Par exemple 2 ≤ 4 est vrai mais 0=1 est faux. L’énoncé «Anne est l’amie de Bob» peut être vrai dans certaines situations (on parle de modèle) et faux dans d’autres. L’énoncé «Tout le monde a les yeux bleus» sera vrai ou faux en fonction de notre interprétation de «tout le monde», suivant si on se restreint a une famille donnée ou bien si on considère l’ensemble de la population française.

On représente les valeurs de vérité par un des éléments de l’ensemble B={V,F} des booléens (parfois noté {1,0}).

1.3.1  Le cas propositionnel

Une fois que l’on connaît quelles formules atomiques sans variables sont vérifiées (la formule est toujours fausse et la formule est toujours vraie), on peut définir quand une formule composée est vraie en fonction de la véracité des formules qui la composent.

 PQ¬ PP ∧ QP ∨ QP ⇒ Q 
 VVFVVV 
 FVVFVV 
 VFFFVF 
 FFVFFV 

Pour savoir si une formule propositionnelle est vraie, il “suffit” de la décomposer pour se ramener à la vérité des formules atomiques qui la composent.

Si une formule ne contient pas de variables propositionnelles et symboles de prédicats, on peut calculer sa valeur de vérité.

Dans le cas où certains symboles de prédicats ne sont pas définis, ils sont vus comme des inconnus. On pourra s’intéresser à savoir si une formule est vraie pour toutes les interprétations possibles de ces prédicats (pour tous les modèles). Si c’est le cas on dira que la formule est valide ou encore que c’est une tautologie. Si la formule est vraie pour certaines interprétations, on dit que la formule est satisfiable, si elle est fausse dans toutes les interprétations alors elle est dite insatisfiable.

Exemple 1   
Exercice 1   Les formules suivantes sont-elles valides ?
  1. ((PQ) ⇒ P) ⇒ P
  2. PP) ⇒ P
Calcul de la valeur de vérité.

Une textitinterprétation I donne la valeur de vérité d’une formule atomique p autre que et

on définit val(I,P)∈B pour toute formule propositionnelle P

val(I,⊥)F 
val(I,⊤)V 
val(I,x)I(x)x ∈  Vp 
val(I,¬ P)si val(I,P)=T alors F sinon V 
val(IP∧ Q)si val(I,P)=V alors val(I,Qsinon F 
val(IP∨ Q)si val(I,P)=V alors V sinon val(I,Q) 
val(IP⇒ Q)si val(I,P)=V alors val(I,Qsinon V 
val(IP⇔ Q)si val(I,P)=val(I,Qalors V sinon F 

Le calcul propositionnel permet de modéliser et de résoudre des problèmes. En plus de pouvoir décider si une formule est valide, on peut également répondre à la question pour quelles valeurs des formules atomiques la propriété sera-t-elle vérifiée ? ou bien à la question combien y-a-t-il de solutions différentes ?

Exercice 2 (Enigme du tigre et de la princesse)   Des prisonniers sont soumis à un test qui peut se résoudre en utilisant la logique. Ils doivent choisir entre deux portes derrière lesquelles il peut y avoir soit une princesse soit un tigre. S’ils ouvrent une porte derrière laquelle il y a un tigre, ils sont dévorés.

Des inscriptions sur les portes guident leur choix:

La porte 1 comporte la mention “Il y a une princesse derrière cette porte et un tigre derrière l’autre”, la porte 2 comporte la mention “Il y a une princesse derrière une des portes et un tigre derrière l’autre”, on sait de plus qu’une seule de ces inscriptions est vraie.

On introduit les variables propositionnelles P1 (resp. P2) pour représenter la présence d’une princesse derrière la porte 1 (resp. la porte 2).

1.3.2  Formule avec variables

On se place ici dans ce que l’on appelle un modèle, c’est-à-dire que l’on connait le “sens” des objets dont on parle dans la logique et que l’on connait pour chaque symbole de prédicat, pour quelles valeurs il est vérifié. Un modèle particulier est celui des entiers avec les opérations arithmétiques usuelles et les relations d’égalité et d’inégalité. Dans un tel modèle 2+2=4 est vrai et 1≤ 0 est faux.

Une formule logique peut contenir des variables qui représentent des objets arbitraires.

Une formule atomique P avec variables représente un ensemble de formules closes (sans variable) obtenues en remplaçant les variables par des objets du modèle.

Par exemple si notre modèle est celui des entiers xy est une formule avec deux variables x et y. Se poser la question de savoir si cette formule est vraie nécessite d’expliciter comment on traite les inconnues x et y.

Vérité d’une formule quantifiée sans variable libre.

La vérité d’une formule sans variable libre mais avec des quantificateurs du premier ordre dépend en général de l’exploration de la vérité d’un ensemble infini de formules (obtenues en remplaçant les variables par des objets arbitraires).

Exercice 3   Les formules suivantes sont-elles vraies (pour tout prédicat P)?
  1. (∀ x, P(x)) ⇒ ∃ x, P(x)
  2. ¬(∀ x, P(x)) ⇒ ∃ x, ¬ P(x)

1.4  Formule démontrable

Dans le cas des formules propositionnelles, on peut calculer si une formule sans variable propositionnelle est vraie et même si une formule avec des variables propositionnelles est valide en regardant tous les cas possibles (tables de vérité). Cela peut être fastidieux mais c’est possible.

Cependant ce n’est pas forcément la meilleure stratégie. Par exemple si la formule que l’on veut prouver valide est de la forme :

(P∧ Q1 ∧ Q2 ∧ Q3 ∧ Q4) ⇒ P

La table de vérité a 25 lignes alors que la propriété est triviale!

1.4.1  Séquents

Pour établir la validité des formules, on utilise souvent des systèmes de déduction qui permettent de déduire qu’une formule est une conséquence logique d’un ensemble de formules.

On écrit cette relation Γ ⊢ Q avec Γ un ensemble de formules {P1;…;Pn} que l’on note usuellement par simple juxtaposition P1,…,Pn et Q une formule. On appelle cet objet un séquent. Les formules de Γ sont appelées les hypothèses et la formule P est la conclusion du séquent.

Un système de déduction est un ensemble de règles du jeu qui définissent quels sont les séquents prouvables.

L’interprétation de cette relation est que si on a pu dériver Γ ⊢ P et que les formules dans Γ sont vraies alors la formule P est vraie.

Lien entre formule et séquent.

Un séquent est formé de plusieurs formules (les hypothèses P1,…,Pn et la conclusion Q) que l’on note P1,…,PnQ.

On a deux notions de vérité mais qui sont étroitement liées. Si le séquent P1,…,PnQ est vrai alors la formule associée au séquent (P1∧ … ∧ Pn)⇒ Q sera vraie. En particulier si Q est vrai (séquent sans hypothèse) alors la formule Q est vraie. Une autre manière équivalente de définir la formule associée est P1⇒ … ⇒ PnQ.

Lorsque l’on s’intéresse au calcul booléen, on privilégie les connecteurs de négation, conjonction et disjonction (qui se calculent facilement). Dans les calculs des séquents, c’est au contraire l’implication qui est un des connecteurs privilégiés. L’avantage est que lorsqu’on veut montrer une formule de la forme PQ ou encore un séquent de la forme PQ il suffit de se concentrer sur le cas dans lequel P est vrai (car dans le cas où P est faux, le séquent ou la formule sont trivialement vrais, par l’absurde).

1.4.2  Théories

Lorsqu’on s’intéresse à démontrer une formule, on travaille au niveau de la syntaxe. Les règles logiques pour les connecteurs et les quantificateurs ne nous disent rien sur la vérité des formules atomiques.

Les mathématiciens se sont intéressés depuis l’antiquité (par exemple les axiomes d’Euclide pour la géométrie) à trouver des présentations axiomatiques de théories. C’est-à-dire peut-on exhiber un ensemble de formules logiques qui caractérise l’univers dans lequel on souhaite raisonner.

Un modèle d’une théorie est un ensemble et une interprétation des symboles de fonction et de prédicat qui rend vrai toutes les formules de la théorie.

Supposons que l’on ait un ensemble de formules A tel que toutes ces formules soient vraies pour une certaine interprétation des symboles (par exemple pour les entiers naturels ). S’il est possible de prouver AP alors la formule P est également vraie dans l’interprétation .

Un ensemble de formules closes (sans variable libre) s’appelle une théorie. L’ensemble peut être infini sachant que dans les systèmes de preuve que l’on considèrera, s’il est possible de prouver AP alors il existe un sous-ensemble de formules fini Γ tel que Γ ⊢ P.

Une question intéressante est ensuite de caractériser l’ensemble des modèles d’une théorie. La théorie A est complète si pour toute formule P on peut prouver AP ou bien on peut prouver A⊢ ¬ P. Attention, on peut aussi avoir des théories incohérentes telles que on peut prouver A⊢ ⊥ et donc a fortiori n’importe quelle formule P. Une théorie incohérente n’aura pas de modèle.

La plupart des théories ne sont pas complètes.

Une théorie est décidable, si on sait pour toute formule P décider si AP ou non. La théorie vide n’est pas décidable. La théorie de l’arithmétique linéaire (sans multiplication) l’est ainsi que la théorie des réels. Le théorème d’incomplétude de Gödel nous dit que toute théorie qui contient l’arithmétique est forcément incomplète et que quelque soit les axiomes que l’on ajoute la théorie restera incomplète à moins de devenir incohérente.

Égalité

Une théorie importante est celle de l’égalité. Les axiomes nécessaires sont les suivants.

Définition 1 (Théorie de l’égalité)   Le théorie de l’égalité est donnée par les axiomes qui expriment que c’est une relation d’équivalence. Pour chaque symbole de fonction f n-aire on ajoute un axiome qui exprime le fait que c’est une congruence
∀ x1… xn y1… ynx1=y1∧…∧ xn=yn ⇒ f(x1,…, xn)=f(y1,…, yn)
et pour chaque symbole de prédicat P n-aire on ajoute un axiome qui exprime le fait que la propriété est stable par égalité :
∀ x1… xn y1… ynx1=y1∧…∧ xn=yn ⇒ P(x1,…, xn)⇒ P(y1,…, yn)

On en déduit aisément par récurrence sur la structure de la formule, une règle de substitution dans un contexte arbitraire :

t=u ⇒ P[x← t] ⇒ P[x← u]
Définition 2 (Théorie arithmétique de Peano (PA))   Le langage est composé de la constante O du symbole de fonction unaire S et des symboles binaires + et × ainsi que du symbole de prédicat d’égalité.

Les axiomes sont données par l’ensemble P0 suivant qui constitue l’arithmétique élémentaire

La théorie formée de ces 7 axiomes est notée PA0. Cette théorie n’est pas suffisante pour prouver une propriété comme la symétrie de l’addition.

Pour obtenir l’arithmétique de Peano, on lui ajoute une infinité d’axiomes pour le schéma de preuve par récurrence. Pour chaque formule P ayant comme variables libres x1,…,xn,x, on aura comme axiome la formule

∀ x1… xn,P[x← O] ⇒ (∀ xP⇒ P[x← S(x)]) ⇒ ∀ x,P

A tout entier n∈ℕ, on associe un terme de l’arithmétique de Peano Sn(0) que l’on notera ñ.

Exercice 1   On définit la propriété tu  =def  ∃ x, t+x=u. Montrer les propriétés de base de l’ordre sur les entiers.

1.5  Logique et Informatique

Plusieurs types de logique

Il y a de nombreux systèmes logiques différents. Ils offrent des langages différents qui permettent de représenter plus ou moins facilement les notions. Au delà du langage, ces formalismes proposent des règles de raisonnement adaptées qui permettent de faciliter le raisonnement avec l’objectif de le mécaniser, à savoir de fournir des outils informatiques pour résoudre des problèmes exprimés dans ces logiques.

En informatique, on utilise beaucoup des logiques temporelles qui permettent de raisonner sur l’ensemble des états possibles d’un système évolutif, possiblement non-déterministe. On pourra ainsi exprimer simplement qu’un certain évènement se produira quelle que soit l’évolution ou au contraire qu’un autre évènement ne pourra jamais se produire.

Les logiques de description ont été introduites pour aider à la représentation formelle de connaissances dans un domaine d’application donné et sont utilisés pour le Web sémantique. Elles mettent en avant les notions d’individu, de concepts (caractéristique d’un ensemble d’individu) et de rôles (relation entre individus).

Depuis une quarantaine d’années les informaticiens ont fortement contribué au renouveau de la logique en proposant de nouveaux systèmes, en les étudiant du point de vue de leur expressivité et de l’algorithmique de la résolution de problème.

Démonstration automatique.

Des outils informatiques permettent de faire des preuves sur ordinateur. Certains outils font de la démonstration automatique, ils prennent en entrée un problème (par exemple sous la forme Γ ⊢ A) et se placent dans une certaine logique. Ils établissent si oui ou non le problème donné est valide (ou satisfiable) dans la logique.

Dès que la logique est un peu expressive, le problème est indécidable, c’est-à-dire qu’il n’existe pas de programme informatique qui répond exactement à la question. On peut avoir des programmes qui répondent partiellement, c’est-à-dire que dans certains cas, ils ne pourront pas dire si le problème est valide ou non.

Si on se place dans le fragment propositionnel (pas de quantificateurs) alors on peut savoir si une formule est satisfiable, valide ou non. Les SAT-solvers sont des outils qui permettent de traiter des problèmes propositionnels. L’idée est d’avoir des variables pour des propositions atomiques qui peuvent valoir vrai ou faux, puis de décrire un problème sous la forme de contraintes sur ces variables exprimées comme des formules propositionnelles. L’outil détermine s’il existe une manière d’affecter une valeur vrai ou faux à chaque variable propositionnelle qui rende le problème vrai.

Exemple 1   On peut modéliser un problème de Sudoku sous une forme propositionnelle. Pour cela on introduit 93 variables Xijk pour i,j,k∈ [1,9]. L’interprétation est que Xijk est vrai si le chiffre k est sur la i-ème ligne et la j-ème colonne. On peut ensuite exprimer les contraintes :
  1. Un seul chiffre k par case (i,j): Xijk ⇒ ∧lk ¬ Xijl
  2. Chaque chiffre k apparaît sur chaque ligne i au moins dans une colonne j: j=1..9 Xijk
  3. Chaque chiffre k apparaît au plus une fois sur chaque ligne i (s’il est dans la colonne j, il n’est pas dans une autre colonne) : Xijk ⇒ ∧lj ¬ Xilk
  4. Même chose pour les colonnes et les carrés.
  5. Lorsque la case (i,j) est pré-remplie avec le chiffre k, on introduit la contrainte : Xijk.

Les SAT-solvers utilisent des algorithmes sophistiqués pour pouvoir traiter des formules avec un très grand nombre de variables propositionnelles. Ils sont utilisés pour vérifier des programmes, ou bien pour résoudre des problèmes de planification qui seront modélisés de manière logique.

Sur le problème du Sudoku, on voit qu’utiliser des formules du premier ordre avec des variables pour représenter les positions et les chiffres permet de factoriser la description. Au lieu des variables propositionnelles, on introduira un symbole de prédicat pos(i,j,k) qui sera vrai lorsque le chiffre k est à la position (i,j). D’autres fragments de logique sont décidables comme l’arithmétique linéaire sur les entiers (l’addition mais pas la multiplication). Cependant les procédures pour résoudre de tels problèmes ont une forte complexité.

Assistant de preuve.

Si établir la vérité d’un problème Γ ⊢ A est complexe, il est par contre élémentaire de vérifier qu’une démonstration de ce même problème suit les règles de déduction de la logique. C’est ce que font les assistants de preuve. Ils proposent des environnements qui permettent de construire interactivement des preuves. L’utilisateur indique les étapes de démonstration et l’ordinateur maintient l’état du problème : ce qui a été démontré, ce qu’il reste à résoudre. On peut ainsi construire de grosse preuves en garantissant la correction du résultat. L’environnement peut également aider à construire des preuves complexes en introduisant des étapes de preuve qui correspondent à un enchaînement de règles logiques élémentaires.

Les assistants de preuve Coq2 et Isabelle3 sont des exemples de tels outils. Ils sont utilisés à la fois pour garantir la correction de programmes (sécurité de la plateforme JavaCard, preuve de compilateurs, algorithmes de calculs sur les flottants, cryptographie …), mais aussi pour des preuves mathématiques avancées (théorème des 4 couleurs, conjecture de Kepler, classification des groupes finis …).


1
Cette affirmation peut sembler paradoxale, c’est pourtant une propriété vraie. En effet soit tout le monde a les yeux bleus et l’affirmation est vraie, soit il existe une personne qui n’a pas les yeux bleus, que l’on nomme a. La propriété yeux-bleus(a)⇒ ∀ y, yeux-bleus(y) est vraie car de la forme AB avec A est faux. On en déduit le résultat.
2
3

Previous Up Next