Cours d'informatique en ligne gratuit


Télécharger Cours d'informatique en ligne gratuit
55 étoiles sur 5 a partir de 1 votes.
Votez ce document:

Télécharger aussi :


Cours de logique pour l’informatique

Prof. Jean-Franc¸ois Raskin

Département d’Informatique Faculté des Sciences

Université Libre de Bruxelles

Année académique 2007-2008

0-0

Organisation pratique du cours :

Références – Logic in Computer Science : Modeling and Reasoning about Systems, M. R. A. Huth and M. Ryan, Cambridge University Press, 1999.

–    Mathematical Logic for Computer Science, M. Ben-Ari,Prentice Hall, 1993.

Matériel Les slides utilisés lors des cours seront disponibles sur la page web du cours.

Travaux pratiques Assistant : Mr Cédric Meuter

Contact – email :

–    tel : 650 55 92

–    http :

Introduction - Motivations

Les logiques sont utilisées en informatique pour

Modéliser de manière formelle des “objets” rencontrés par les informaticiens;

Ex : Bases de données, bases de connaissances, pré-post conditions d’une procédure, etc.

Raisonner Après une phase de modélisation, l’informaticien doit être cable de se servir du modèle et raisonner sur celui-ci. Ex : validation d’un modèle de données, prise de décision à partir de faits et d’une base de connaissances, preuve de correction d’une procédure/d’un programme;

La logique est à la base de l’étude des raisonnements, c’est-à-dire des déductions que l’on peut faire sur les modèles formels.

Introduction - Motivations

Bénéfices à l’utilisation des formalismes logiques :

–    modèles précis et non-ambigus, demarche rigoureuse, etc.

–    possibilité d’automatiser/semi-automatiser l’analyse des modèles.

Introduction - Motivations

Exemples

Considérons la situation décrite par les affirmations suivantes :

1.    Si le train arrive en retard et il n’y a pas de taxis à la gare alors l’invité arrive en retard.

2.    L’invité n’est pas en retard.

3.    Le train est arrivé en retard.

Et la déduction suivante :

donc, il y avait des taxis à la gare.

Introduction - Motivations

Exemples

Pourquoi peut-on déduire qu’il y avait des taxis à la gare? Premièrement, si on met l’affirmation 1 et l’affirmation 3 ensemble, on peut affirmer que s’il n’y avait pas eu de taxis à la gare, alors l’invité serait arrivé en retard. Deuxièmement, cette dernière affirmation n’est compatible avec le fait 2 que s’il y avait des taxis à la gare. Donc il est consistant de déduire qu’il y avait des taxis à la gare.

Introduction - Motivations

Exemples

Considérons un autre exemple :

1.    Si il pleut et l’invité a oublié son parapluie alors l’invité est trempé.

2.    L’invité n’est pas trempé.

3.    Il pleut.

Et la déduction suivante :

donc, l’invité n’a pas oublié son parapluie.

Introduction - Motivations

Exemples

Pour justifier la déduction“l’invité n’a pas oublié son parapluie”, on peut“réutiliser” le raisonnement fait précédement.

Pourquoi?

Les deux situations décrites ont la même structure logique. Cela est reflété par les opérateurs logiques utilisés dans les phrases : sialors, alors, donc,

Malheureusement les langages naturels comme le franc¸ais, l’anglais ou encore certains langages graphiques (UML par exemple), manquent de précision et sont ambigus. C’est pourquoi il y a un besoin pour des langages mathématiques capables de modéliser et d’aider au raisonnement.

Introduction - Motivations

Exemples

Voyons comment on pourrait formaliser les situations décrites dans les deux exemples précédents. On peut les formaliser à l’aide de la logique propositionnelle. Considérons que

–    la proposition p est utilisée pour représenter la situation “le train arrive en retard”,

–    q pour “il y a des taxis à la gare”

–    r pour “l’invité est en retard”

Introduction - Motivations

Exemples

Alors nous pouvons formaliser la situation décrite dans le premier exemple par la formule logique suivante :

                                                                                           ((p ?  ¬ q) ? r) ?  ¬ r ? p

Et nous pouvons formaliser la déduction par :

                                                                                  ((p ?  ¬ q) ? r) ?  ¬ r ? p |= q

Ou` “|=” se lit : “q est une conséquence logique de ((p ? ¬ q) ? r) ? ¬ r ? p”.

Introduction - Motivations

Exemples

Considérons le test suivant :

if (x ? 3 andz ? 3) or (y ? 2 andz ? 3) then

Il peut-être remplacé par

if (x ? 3 ory ? 2) andz ? 3 then

Car (p ? q) ? r est logiquement équivalent à (p ? r) ? (q ? r).

Introduction - Motivations

Un autre exemple

Considérons les règles suivantes :

1.    les parents d’un enfant sont des ancètres de cet enfant;

2.    les ancêtres d’une personne qui est l’ancêtre d’une deuxième personne sont également ancètres de cette deuxième personne;

3.    deux personnes sont d’une même famille si et seulement si elles ont un ancêtre commun.

Introduction - Motivations

Un autre exemple

–    à la différence des deux exemples précédents, on parle ici de propriétés qui sont vraies pour des catégories : les enfants, les personnes,

–    la logique propositionnelle n’est pas suffisante pour modéliser cette situation, c’est pourquoi nous étudierons une extension de la logique propositionnelle qui est la logique du premier ordre.

Introduction - Motivations

La logique du premier ordre

Les objets sont représentés par des variables (du premier ordre) : x,y,z,

Formalisation de la règle : 1.

? x,y : Parent(x,y) ? Ancetre(x,y)

2.

3.

? x,y :

? z : Ancetre(x,z) ? Ancetre(z,y)

? Ancetre(x,y)

? x,y :

Apparente(x,y)

                                                                                           ?     ? z : Ancetre(z,x) ? Ancetre(z,y)

Introduction - Motivations

La logique du premier ordre

La formalisation de cet exemple permet maintenant de faire des

“calculs” pour raisonner sur cette règle. Par exemple, il est possible de poser de manière précise des questions comme :

– est-ce qu’un parent x et son enfant y sont apparentés?

SpecApparente |=?

? x,y : Parent(x,y) ? Apparente(x,y) – est-ce que la relation Apparente est symétrique?

SpecApparente |=?

? x,y : Apparente(x,y) ? Apparente(y,x)

Note : répondre à ces questions de manière formelle revient à faire une preuve qui établit la propriéte ou à construire un contre-exemple.

Considérons le situation suivante :

Jean

Ancetre             Parent

Marie

On n’a pas Apparente(Jean,Marie). C’est assez contre-intuitif, il faut peut-être ajouter :

? x : Ancetre(x,x)

Donc une formalisation ne représente pas toujours ce que l’on veut vraiment, et on est parfois amené à l’améliorer.

Introduction - Motivations

Programmation logique

La formule SpecApparente peut être vue comme une spécification d’une requête sur une base de données qui peut-être traduite en COBOL, par exemple.

Mais étant donnée une base de faits, établir la liste des personnes apparentées à un individu revient à faire des preuves.

Donc si on peut automatiser ces preuves, on a une alternative à la traduction en COBOL : le résultat de la requête est simplement l’ensemble des paires (x,y) pour lesquelles, le theorem prover peut

établir :

SpecApparente ? Faits |= Apparente(x,y)

Introduction - Motivations

Prolog : programmation logique

Il y a un langage qui est basé sur cette idée : Prolog. Quelques caractéristiques de Prolog : – programmation déclarative;

–       beaucoup de “calculs à la ligne”;

–       permet de développer rapidement des prototypes;– utilisé pour construire des systèmes experts, etc.

Introduction - Motivations

Le but de ce cours est d’étudier en détails les fondements de la logique et vous donner une formation suffisante pour que vous puissiez vous familiariser avec d’autres logiques que vous rencontrerez plus tard. Et également vous sensibiliser au fait que la logique peut être très utile pour automatiser/semi-automatiser les taˆches de raisonnement rencontrées lors de la construction/analyse de modèles et de programmes.

Plan du cours

–       la logique propositionnelle;

–       la logique du premier ordre;– la programmation logique; – questions avancées.

La logique propositionnelle

Plan

–       Syntaxe de la logique propositionnelle;

–       Sémantique de la logique propositionnelle;

–       Procédure de décision : tableaux sémantiques;

–       La déduction naturelle;

–       La résolution propositionnelle.

La logique propositionnelle

Syntaxe - Construction des formules (I)

Le vocabulaire du langage de la logique propositionnelle est composé :

–       d’un ensemble, fini ou dénombrable, de propositions notées p,q,r,

Dans la suite, nous notons un sous-ensemble de propositions par les lettres P, Q, ;

–       de deux constantes : vrai (notée ? ) et faux (notée ? );

–       d’un ensemble de connecteurs logiques : et (noté ? ), ou (noté ? ), non (noté ¬ ), implique (noté ?), équivalent (noté ?); – les parenthèses : (,).

La logique propositionnelle

Syntaxe - Construction des formules (II)

Les formules de la logique propositionnelle respectent la règle de formation BNF suivante :

? ::= ?   |  ?    | p | ?1 ? ?2 | ?1 ? ?2

                                                                               | ?1 ? ?2 | ?1 ? ?2 |     ¬ ?1 | (?1)

Ou` ? , ? sont respectivement les constantes vrai et faux, p ? P est une proposition et ?1, ?2 sont des formules propositionnelles bien formées. L’ensemble des formules propositionnelles bien formées sera noté FormulesProp.

La logique propositionnelle

Quelques exemples de formules

Voici quelques exemples de formules et leur lecture intuitive :

–    la formule propositionnelle ”p ? (q ? r)”, peut être lue de la fac¸on suivante ”p implique q et r”, ou peut être également lue comme ”si p est vrai alors q et r doivent être vrais”;

–    la formule propositionnelle ”¬ (p ? q)”, peut-être lue de la fac¸on suivante ”il est faux que p et q soient vrais (en même temps)”.

La logique propositionnelle

Ambigu¨?tés (I)

L’utilisation de la notation infixe s’accompagne de problèmes de parsing :

e1op1e2op2e3

=? (e1op1e2)op2e3

=? e1op1(e2op2e3)

La logique propositionnelle

Ambigu¨?tés (II)

Pour lever les ambigu¨?tés, on utilise les parenthèses ou des règles de priorité entre opérateurs :

–    si op1 a une plus grande précédence (priorité) que op2 alors

e1op1e2op2e3 est équivalent à ((e1op1e2)op2e3)

–    si op est associatif à gauche alors

e1ope2ope3 est équivalent à ((e1ope2)ope3)

Une fois ces règles fixées, à chaque formule correspond un et un seul arbre de parsing.

La logique propositionnelle

Règles de précédence

Ordre de précédence sur les opérateurs :

¬

?

?

?

?

et associativité à gauche.

Les parenthèses permettent de contrecarrer ces règles, si elles ne conviennent pas. Elles permettent aussi de rendre une formule plus lisible, ou de ne pas devoir retenir les règles de précédence.

La logique propositionnelle

Arbre correspondant à une formule

La formule p ? q ? r est donc équivalente à

((p ? q) ? r)

et donc son arbre de parsing est :

?

r

p              q

La logique propositionnelle

Profondeur d’une formule

La profondeur d’une formule ? est la profondeur de l’arbre de parsing A? associé à la formule.

Elle se définit de manière inductive comme suit :

–    cas de base : si ? = p, ? , ? ou` p est une proposition alors

Prof (?) = 0;

–    cas inductif : si ? = ?1op?2 alors Prof (?) = 1 + max(Prof (?1),Prof (?2)); si ? = (?1) alors Prof (?) = Prof (?1).

Nous notons FormulesPropi les formules propositionnelles de profondeur i. Notons que

FormulesProp = Si?0 FormulesPropi

La logique propositionnelle

Rappel : l’induction mathématique (I)

Il est bien connu que pour n ? 1, on a

Pour démontrer que cette égalité, notée M(n), est valide pour n’importe quel n ? 1, on applique le principe d’induction mathématique .

La logique propositionnelle

Rappel : l’induction mathématique (II)

SI

–    Cas de base : on établit que la propriété est vraie pour n = 1, c’est-à-dire que l’on prouve que M(1) est vraie.

–    Cas inductif : en faisant l’hypothèse que la propriété est vraie pour n = i (ou pour n ? i), on établit que la propriété est également vraie pour n = i + 1.

ALORS

Le principe d’induction affirme que M(n) est vraie pour tout n ? 1.

La logique propositionnelle

Rappel : l’induction mathématique (III)

Nous utiliserons le principe d’induction mathématique pour prouver des propriétés qui sont vraies pour toutes formules de la logique propositionnelle, et ce en raisonnant par induction sur la profondeur des formules.

La logique propositionnelle

La sémantique (I)

Etant donné un ensemble de propositions P, une fonction d’interprétation V pour P est une fonction du type

V : P ?  {vrai,faux}, c’est-à-dire une fonction qui assigne à chaque proposition de P la valeur vrai ou la valeur faux. L’ensemble des fonctions d’interprétation propositionnelle sera noté FonctInterProp.

Dans la suite, nous utiliserons parfois le terme valuation ou bien de

fonction d’interprétation.

La logique propositionnelle

La sémantique (II)

La valeur de vérité d’une formule propositionnelle ? formée à partir (d’une des propositions de l’ensemble P, évaluée avec la fonction d’interprétation V , est notée [[?]]V . Formellement,

[[ · ]]· : FormulesProp × FonctInterProp ? {vrai,faux}. La fonction [[?]]V est définie par induction sur la syntaxe de ? de la fac¸on suivante :

–    ? = ? , dans ce cas, [[?]]V = vrai;

–    ? = ? , dans ce cas, [[?]]V = faux; – ? = p, dans ce cas, [[?]]V = V (p).

                                                                                ?? faux     si [[?1]]V = vrai

–    ? = ¬ ?1, [[?]]V =

                                                                                              vrai      si [[?1]]V = faux

?


? = ?1 ? ?2,

[[?]]V = vrai ssi

[[?1]]V = vrai ou [[?2]]V = vrai

? = ?1 ? ?2,

[[?]]V = vrai ssi

[[?1]]V = vrai et [[?2]]V = vrai

? = ?1 ? ?2,

[[?]]V = vrai ssi

[[?1]]V = faux ou [[?2]]V = vrai

–    ? = ?1 ? ?2,

[[?]]V = vrai ssi

[[?1]]V = faux et [[?2]]V = faux ou [[?1]]V = vrai et [[?2]]V = vrai

–    ? = (?1), [[?]]V = [[?1]]V .

Nous notons V |=?si et seulement si [[?]]V = vrai.

La logique propositionnelle

La sémantique (III)

L’information contenue dans la définition précédente est souvent présentée sous forme de tables, appelées tables de vérité :

?

?

vrai

faux

p

¬ p

(p)

vrai

faux

vrai

faux

vrai

faux

La logique propositionnelle

La sémantique (IV)

p

q

p ? q

p ? q

p ? q

p ? q

vrai

vrai

vrai

vrai

vrai

vrai

vrai

faux

faux

vrai

faux

faux

faux

vrai

faux

vrai

vrai

faux

faux

faux

faux

faux

vrai

vrai

La logique propositionnelle

La sémantique (V)

Voici deux définitions importantes :

–    Une formule propositionnelle ? est validesi et seulement si pour toute fonction d’interprétation V pour les propositions de ?, on a V |=?.

–    Une formule propositionnelle ? est satisfaisablesi et seulement si il existe une fonction d’interprétation V pour les propositions de ?, telle que V |=?.

Une conséquence directe de ces deux définitions est que :

Une formule propositionnelle ? est valide ssi sa négation ¬ ? n’est

pas satisfaisable.

Theorème : Une formule propositionnelle ? est valide ssi sa négation ¬ ? n’est pas satisfaisable.

Preuve. On applique simplement les définitions. Par définition ? est valide si, pour toute fonction d’interprétation V , V |=?, ce qui est équivalent à V 6       |= ¬ ?, par définition de la sémantique de ¬ et donc si ? est valide, il n’existe pas de fonction d’interprétation V telle que V |= ¬ ? et donc ¬ ? n’est pas satisfaisable. L’autre direction est laissée comme exercice.

?

La logique propositionnelle

La sémantique (VI)

Une formule propositionnelle ? est une conséquence logique d’un ensemble de formules propositionnelles {?1, ,?n } si et seulement si on a que pour toute fonction d’interprétation V (sur les propositions de ?,?1, ,?n), telle que V |=?i pour tout i, 1 ? i ? n, on a également V |=? ; ce fait est noté ?1, ,?n |= ?.

Deux formules ? et ? sont equivalentessi et seulement si on a ? |= ?et? |= ?.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (I)

Algorithme pour établir la satisfaisabilité/validité de formules de la logique propositionnelle.

Le principe est très simple : pour prouver la satisfaisabilité d’une formule de la logique propositionnelle, on cherche systématiquement un modèle pour cette formule.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (II)

On a besoin de quelques nouvelles définitions :

Une formule propositionnelle ? est un littéralsi et seulement si? est une proposition ou la négation d’une proposition.

Deux formules ? et ¬ ? sont des formules complémentaires .

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (III)

Considérons la formule ? = p ? ( ¬ q ?  ¬ p)

Essayons de construire systématiquement une fonction d’interprétation V telle que

[[?]]V = vrai

Par définition on a

[[?]]V = vrai

ssi

                                                                      [[p]]V = vrai et [[ ¬ q ?  ¬ p]]V = vrai

et

                                                                                                  [[ ¬ q ? ¬ p]]V = vrai

ssi

[[ ¬ q]]V = vrai ou [[ ¬ p]]V = vrai

et donc,

[[?]]V = vrai

ssi

[[p]]V = vrai et [[ ¬ q]]V = vrai ou [[p]]V = vrai et [[ ¬ p]]V = vrai

Pour ?, on construit la fonction d’interprétation V de la fac¸on suivante :

V (p) = vrai; – V (q) = faux. et on a bien que V |=?.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (IV)

Nous avons réduit le problème de satisfaction de ? à un problème de satisfaction d’ensembles de littéraux.

Un ensemble S de littéraux est satisfaisable ssi il ne contient pas une paire de littéraux complémentaires .

Vu que chaque formule contient un ensemble fini de propositions, et donc un ensemble fini de littéraux, il y a un nombre fini d’ensembles de littéraux.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (V) Un autre exemple : ? = (p ? q) ? ( ¬ p ? ¬ q).

Par définition, on a

[[?]]V = vrai

ssi

                                                               [[p ? q]]V = vrai et [[ ¬ p ?  ¬ q]]V = vrai

et donc,

[[?]]V = vrai

ssi

[[p ? q]]V = vrai et [[ ¬ p]]V = vrai et [[ ¬ q]]V = vrai et donc,

[[?]]V = vrai

ssi

soit [[p]]V = vrai et [[ ¬ p]]V = vrai et [[ ¬ q]]V = vrai

ou [[q]]V = vrai et [[ ¬ p]]V = vrai et [[ ¬ q]]V = vrai

Vu que les deux ensembles de littéraux ont des paires complémentaires, la formule ? n’est donc pas satisfaisable.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (VI)

L’information présente dans les développements précédents est plus facilement représentée sous forme d’un arbre.

Exemple : ? = (p ? q) ? ( ¬ p ?  ¬ q) (tableau donné au cours)

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (VII)

Remarques :

–    quand on applique le ”pas de simplification”à un noeud ou` on sélectionne une conjonction, alors on obtient un seul fils; on appelle ces règles, des ?-règles;

–    quand on applique le ”pas de simplification”à un noeud ou` on sélectionnne une disjonction, alors on obtient deux fils; on appelle ces règles, des ?-règles.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (VIII)

?

?1

?2

                  ¬ ¬ ?

?

?1 ? ?2

?1

?2

¬ (?1 ? ?2)

¬ ?1

¬ ?2

¬ (?1 ? ?2)

?1

¬ ?2

?1 ? ?2

?1 ? ?2

?2 ? ?1

?-règles .

Remarque : toutes les formules ? peuvent être considérées comme équivalentes à des conjonctions. Par exemple :

                                                             ¬ (?1 ? ?2) est équivalent à ¬ ?1 ? ¬ ?2

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (IX)

?

?1

?2

?1 ? ?2

?1

?2

¬ (?1 ? ?2)

¬ ?1

¬ ?2

?1 ? ?2

¬ ?1

?2

¬ (?1 ? ?2)

¬ (?1 ? ?2)

¬ (?2 ? ?1)

?-règles .

Remarque : toutes les formules ? peuvent être considérées comme équivalentes à des disjonctions. Par exemple :

                                                             ¬ (?1 ? ?2) est équivalent à ¬ ?1 ? ¬ ?2

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (X)

Algorithme de construction d’un tableau sémantique , quelques notations :

–    un arbre représentant le tableau sémantique d’une formule ? sera noté T? ;

–    l,n,m représentent des noeuds d’un arbre;

–    Lab(l) dénote l’étiquette du noeud l, c’est un ensemble de formules;

–    Status(l) est le statut du noeud l, ce statut est ? pour tout noeud qui n’est pas une feuille et Status(l) ?  {ouvert,ferm } si l est une feuille;

–    Q,R dénotent des ensembles de noeuds.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XI)

Algorithme :

–    Initialisation : R := {l}; Lab(l) := {?}; – Itérer tant que R 6= ? : choisir l ? R :

–    si Lab(l) est un ensemble de littéraux alors :

–    Si Lab(l) contient une paire de littéraux complémentaires :

Status(l) := ferm et R := R \ {l};

–    Si Lab(l) ne contient pas de paires de littéraux complémentaires :

Status(l) := ouvert et R := R \ {l};

–    si Lab(l) n’est pas un ensemble de littéraux alors : choisir ? ? Lab(l) qui n’est pas un littéral,

–    si ? est une ?-formule alors créer un fils m pour l et :

–    R := R ? {m} \ {l};

–    Lab(m) := (Lab(l) \ {?}) ? {?1,?2};

–    si ? est une ?-formule alors créer deux fils, m et n, pour l et :

–    R := R ? {m,n} \ {l};

–    Lab(m) := (Lab(l) \ {?}) ? {?1};

–    Lab(n) := (Lab(l) \ {?}) ? {?2};

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XI)

Un tableau dont la construction est terminée est appelé un tableau

complet .

Un tableau fermé est un tableau complet dont toutes ses feuilles sont étiquettées avec fermé. C’est un tableau ouvert sinon.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XII)

Théorème : Si T? est le tableau complet de la formule ?, alors ? est non satisfaisable ssi T? est fermé.

Avant de prouver la correction de l’algorithme par rapport au théorème ci-dessus observons quelques conséquences de ce théorème :

–    ? est satisfaisable ssiT? est ouvert; – ? est valide ssiT¬? est fermé.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XII)

Correction de l’algorithme : qu’est-ce que cela veut dire?

–    terminaison : l’algorithme termine pour toutes les formules de la logique propositionnelle;

–    adéquation : si l’algorithme construit un tableau qui ferme pour une formule ? alors la formule ? est non satisfaisable;

–    complétude : pour toute formule ? non satisfaisable, l’algorithme construit un tableau fermé.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XIII)

Terminaison de l’algorithme :

On définit une fonction de “poids” qui associe à chaque ensemble de formules un nombre naturel; on note Poids(l) le poids de l’étiquette du noeuds l.

On montre que si m est un fils de l alors

Poids(m) < Poids(l).

Vu que Poids() est une fonction des ensembles de formules vers les naturels alors la profondeur de tout tableau sémantique est finie et donc l’algorithme termine.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XIII)

Définition de la fonction Poids(?). On définit d’abord cette fonction pour une formule ? par induction sur la structure de la formule.

–     Poids(p) = 1.

–     Poids(¬?) = 1 + Poids(?);

–     Poids(?1 ? ?2) = 2 + Poids(?1) + Poids(?2);

–     Poids(?1 ? ?2) = 2 + Poids(?1) + Poids(?2);

–     Poids(?1 ? ?2) = 2 + Poids(?1) + Poids(?2); – Poids(?1 ? ?2) = 2 × (Poids(?1) + Poids(?2)) + 5 et finalement, Poids(?) = P??? Poids(?).

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XIII)

Propriétés :

–     la fonction Poids() attribue un poids fini et strictement positif à chaque formule;

–     le poids de l’étiquette d’un noeud l est toujours strictement supérieur aux poids des étiquettes de ses fils.

Preuves laissées comme exercices.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XIV)

Adéquation de l’algorithme :

On doit montrer que “Si T? est fermé alors ? est non satisfaisable”.

On montre une propriété plus forte : “Si un sous-arbre de racine l est fermé alors l’ensemble de formules Lab(l) est non satisfaisable”. Pour établir cette propriété, on raisonne par induction sur la profondeur du sous-arbre.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XIV)

Lemme : Si un sous-arbre de racine l est fermé alors Lab(l) est non satisfaisable.

Preuve : Par induction sur la profondeur du sous-arbre.

CB : Prof(l) = 0. Alors Lab(l) est un ensemble de littéraux. Si l est fermé, Lab(l) contient une paire de littéraux complémentaires et donc Lab(l) est non satisfaisable.

CI : dans ce cas Prof(l) > 0, et l’algorithme a sélectionné ? ? Lab(l). Deux cas sont possibles :

1.     ? est une ?-formule. Traitons le cas ? ? ¬ ¬ ?. Dans ce cas, l a un fils m. On a Lab(m) = Lab(l) \ {¬ ¬ ? } ? {? }. On sait que le sous-arbre de racine m est fermé (dans le cas contraire l ne pourrait pas l’être). Par HI, on a que Lab(m) est non satisfaisable et donc pour toute valuation V , on a soit V 6|= Lab(l) \ {¬ ¬ ? } ou V |6 = ?. Donc pour chaque valuation V

on sait que V 6|= Lab(l) \ {¬ ¬ ? } ou V 6|= ¬ ¬ ?. Par conséquent, nous avons bien que pour toute valuation V , V 6|= Lab(l), et Lab(l) est non satisfaisable.

2.     ? est une ?-formule. Traitons le cas ? ? ?1 ? ?2. Dans ce cas, l a deux fils m et n. On a Lab(m) = Lab(l) \ { ?1 ? ?2 } ? {?1 } et Lab(n) = Lab(l) \ {?1 ? ?2 } ? { ?2 } . Par HI on sait que Lab(m) et Lab(n) sont non satisfaisables. Donc toute valuation V qui satisfait Lab(l) \ {?1 ? ?2 } ne satisfait ni ?1 ni ?2, et donc ne satisfait pas ?1 ? ?2. On a donc bien que

                        Lab(l) \  {?1 ? ?2 }  ?                  {?1 ? ?2 } = Lab(l) est non satisfaisable.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XV)

Complétude de l’algorithme :

On doit montrer que “Si ? est non satisfaisable alors T? est fermé”.

Prouver cette propriété revient à établir la contraposée : “Si T? est ouvert alors la formule ? est satisfaisable”.

Pour établir cela, nous avons besoin de quelques notions supplémentaires.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XVI)

Un ensemble de formules ? (on considère des littéraux, conjonctions ou disjonctions) a la propriété de Hintikkassi les trois propriétés suivantes sont vérifiées :

1.    pour toute proposition p, on a soit p 6? ? ou ¬ p 6? ?;

2.    si {?1 ? ?2 } ? ? alors on a ?1 ? ? ou ?2 ? ?;

3.    si {?1 ? ?2 } ? ? alors on a ?1 ? ? et ?2 ? ?.

Propriété des ensembles de Hintikka :

Tout ensemble de formules ? qui a la propriété de Hintikka est satisfaisable.

Lemme Tout ensemble de formules ? qui a la propriété de

Hintikka est satisfaisable.

Preuve. On construit une valuation V de la fac¸on suivante :

V (p) = V rai si p ? ?

V (p) = Faux si ¬ p ? ?

et (arbitrairement) V (p) = V rai si p /? ? et ¬ p 6? ?.

Montrons que toute formule ? ? ? est satisfaite par V .

On raisonne par induction sur la structure de ? :

CB :

CI :

–    ? = ?1 ? ?2.

Par définition des ensembles de Hintikka on sait que soit ?1 ? ?, soit ?2 ? ?. Par HI, si ?1 ? ? on a [[?1]]V = vrai, et si ?2 ? ? on a [[?2]]V = vrai. Donc [[?1 ? ?2]]V = vrai.

–    ? = ?1 ? ?2. On sait que ?1 ? ? et ?2 ? ?. Par HI on a

[[?1]]V = [[?2]]V = vrai et donc [[?1 ? ?2]]V = vrai.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XVII)

On appelle l’ensemble des noeuds que l’on parcourt depuis la racine d’un arbre jusqu’a` une feuille l la branche de l; on note Branche(A,l) la branche qui mène de la racine de l’arbre A à la feuille l.

On a le lemme suivant :

Soit l une feuille ouverte de T? alors

S

m?Branche(A,l) Lab(m)

est un ensemble de formules qui a la propriété de Hintikka.

Preuve. on montre que chaque propriété est vérifiée :

1.    Pour tout p, p /? ? ou ¬ p /? ?. En effet l est une feuille ouverte et donc elle ne contient pas de littéraux complémentaires.

2.    Si ?1 ? ?2 ? ? alors on a appliqué une ?-règle et soit ?1 ? ? ou ?2 ? ?.

3.    Si ?1 ? ?2 ? ? alors on a appliqué une ?-règle et ?1 ? ? ainsi que ?2 ? ?.

La logique propositionnelle

Procédure de décision - Tableaux sémantiques (XVIII)

On obtient la preuve de complétude par le raisonnement suivant : Si T? est ouvert alors il contient une feuille l qui est ouverte et donc

S

m?Branche(A,l) Lab(m)

est un ensemble de formules qui a la propriété de Hintikka. Donc toutes les formules de

S

m?Branche(A,l) Lab(m)

sont satisfaisables et en particulier

? ? Sm?Branche(A,l) Lab(m).

La logique propositionnelle

Déduction naturelle (I)

L’algorithme introduit précédemment ne convient pas bien pour faire des raisonnements“a` la main” sur des formules propositionnelles. Quand on fait des preuves en mathématique, on utilise des règles qui nous permettent, pas par pas, de déduire des conclusions à partir de prémisses.

La déduction naturelle est une formalisation de ce type de raisonnement.

La logique propositionnelle

Déduction naturelle (II)

Supposons données un ensemble de formules ?1, ,?n que nous appelons prémisses et une formule ? que nous appelons conclusion . Et que l’on désire montrer que ? peut être dérivée de ?1, ,?n ; on notera cette intention ?1, ,?n ? ?, cette dernière expression est appelée un séquent . Cette notion de dérivation syntaxique sera intimement liée à la notion sémantique de conséquence logique ( |=), en effet, on aura :

?1, ,?n ? ?ssi?1, ,?n |= ?

La logique propositionnelle

Déduction naturelle (III)

Règles pour la conjonction : – Introduction :

–    Elimination :

La logique propositionnelle

Déduction naturelle (IV)

Exemples d’utilisation de ces règles pour la conjonction :

–    p ? q,r ??q ? r.

1    p ? q        prémisse

2    r       prémisse

3    q       ? e2,1

4    q ? r ? i,3,2

–    (p ? q) ? r,s ? t ? q ? s;

Laissé comme exercice.

–    (p ? q) ? r ? p ? (q ? r);

Laissé comme exercice.

La logique propositionnelle

Déduction naturelle (IV)

Règles pour la (double) négation : – Introduction :

? ¬¬? ¬ i – Elimination :

¬¬?

? ¬ e

Exemple : p, ¬   ¬ (q ? r) ?  ¬ ¬ p ? r

La logique propositionnelle

Déduction naturelle (V)

Règle pour l’élimination de l’implication (Modus Ponens ) :

                                                                                                                  ?         ???

?              ?e

Illustration :

1.    il pleut;

2.    si il pleut alors la route est mouillée.

alors on peut déduire que la route est mouillée.

La logique propositionnelle

Déduction naturelle (VI)

Etant données les prémisses

1.    p;

2.    p ? q ;

3.    p ? (q ? r)

Peut-on déduire r?

La logique propositionnelle Déduction naturelle (VII)

Supposons que p ? q et ¬ q soient vraies, si p est vrai alors par la règle du modus ponens on peut dériver q ce qui est en contradiction avec le fait que ¬ q est vrai, donc on en déduit que ¬ p est vrai. Ce raisonnement est résumé dans la règle suivante, appelée règle de

Modus Tollens :

La logique propositionnelle

Déduction naturelle (VIII)

Prouvons le séquent suivant :

p ? (q ? r),p, ¬ r ?   ¬ q

1    p ? (q ? r)    prémisse

2    p       prémisse

3    ¬ r prémisse 4 q ? r ?e 1et2

                                                                                    5    ¬ q                         MT4,3

La logique propositionnelle

Déduction naturelle (XI)

MT nous a permis de montrer :

p ? q, ¬ q ? ¬ p

et le séquent

p ? q ?  ¬ q ? ¬ p

semble d’une certaine fac¸on dire la même chose. Mais jusqu’a` présent, nous n’avons pas de règles pour introduire le connecteur “implication”.

La logique propositionnelle

Déduction naturelle (XII) Le raisonnement à partir d’hypothèses :

On sait que p ? q est vrai. Si on suppose (on fait l’hypothèse) que q est faux alors on peut déduire grâce à la règle MT que p est faux. Donc en supposant ¬ q on peut déduire ¬ p donc “¬ q implique ¬ p”, exprimé de manière symbolique ¬ q ?     ¬ p est déduit.

L’argument pour p ? q ?     ¬ q ?    ¬ p peut être résumé de la fac¸on

suivante :

1

p ? q

prémisse

2

¬ q

hyp.

3

¬ p

MT1,2, fin hyp.2

4

¬ q ?     ¬ p

?i,2 ? 3

La logique propositionnelle

Déduction naturelle (XIII)

Règle pour l’introduction de l’implication :

?     hyp.

·

· ·

?     fin hyp.

La logique propositionnelle Déduction naturelle (XIV) Prouvons le séquent ¬ q ? ¬ p ? p ? ¬ ¬ q :

1     ¬ q ?  ¬ prémisse

2     p   hyp.

3     ¬   ¬ ¬      ¬ i,2

4     ¬   ¬ q  MT,1,3, fin hyp.2

5     p ?      ¬      ¬ ?i,2 ? 4

La logique propositionnelle

Déduction naturelle (XV)

Preuves de formules vraies sans prémisse :

1    p   hyp.

2    ¬   ¬ ¬      ¬ i,1, fin hyp.1

3    p ?      ¬      ¬ ?i,1 ? 2

Donc on a établi ? p ?     ¬ ¬ p

Note : les formules que l’on peut établir sans prémisses sont les formules valides.

La logique propositionnelle Déduction naturelle (XVI)

Prouvons le séquent suivant :

                                                                  ?? (q ? r) ? ((¬ q ?     ¬ p) ? (p ? r))


1

q ? r

hyp.

2

¬ q ?  ¬ p

hyp.

3

p

hyp.

4

¬ ¬ p

¬ ¬ i,3

5

¬ ¬ q

MT2,4

6

q

¬ ¬ e5

7

r

?e 1,6, fin hyp.3

8

p ? r

?i 3 ? 7, fin hyp.2

9

( ¬ q ?  ¬ p) ? (p ? r)

?i 2,8, fin hyp.1

10

(q ? r)

  ? ((¬ q ?   ¬ p) ? (p ? r))

?i 1,9

La logique propositionnelle

Déduction naturelle (XVII)

Règle pour introduire la disjonction :

La logique propositionnelle

Déduction naturelle (XVIII)

Comment éliminer la disjonction?

Imaginons que l’on puisse :

1.     établir une formule ? sous hypothèse que ?1 est vrai,

2.     et que l’on puisse également établir ? sous hypothèse que ?2 est vrai,

3.     et qu’il existe une preuve pour ?1 ? ?2 alors on devrait pouvoir déduire ?.

Cette stratégie de preuve est formalisée dans la règle suivante :

?1hyp.         ?2hyp.

                                                                                                                ·                     ·

                                                                                                                ·                     ·

·       · ?1 ? ?2          ?fin hyp.    ?fin hyp.

?                                               ? e

Attention : dans chacun des deux cas, on ne peut pas utiliser l’hypothèse temporaire faite pour l’autre cas, sauf si cette hypothèse a été établie avant.

La logique propositionnelle Déduction naturelle (XIX)

Prouvons le séquent

p ? q ? q ? p

1    p ? q      prémisse

2    p     hyp.

3    q ? p      ? i2, fin hyp.2

4    q     hyp.

5    q ? p      ? i1, fin hyp.4

6    q ? p      ? e1,2 ? 3,4 ? 5

La logique propositionnelle

Déduction naturelle (XX)

Règle de copie pour conclure un raisonnement sous-hypothèse.

copie

Considérons le séquent :

? p ? (q ? p)

Et la preuve suivante :

                                                                   1    p

hyp.

                                                                   2    q

hyp.

                                                                   3    p

copie1, fin hyp.2

                                                                   4     q ? p

?i 2,3, fin hyp.1

                                                                   5           p ? (q ? p)

?i 1 ? 4

La logique propositionnelle

Déduction naturelle (XXI) Règles pour la négation.

Les contradictions sont des formules de la forme :

                                                                                                     ¬ ? ? ? ou ? ? ¬ ?

Notons qu’aucune valuation ne satisfait une contradiction. Donc on a ¬ ? ? ? |= ? pour n’importe quel ?. Donc si la méthode de déduction est complète, on devrait avoir : ¬ ? ? ? ? ? pour n’importe quel ?.

On peut également voir ce phénomène sous l’angle suivant : l’information contenue dans ? ? ? est au moins le contenu de ? et de ? ensemble, alors que l’information contenue dans ? ? ? a au plus l’information contenue dans ? et au plus l’information contenue dans ?, et si ? a au moins autant d’information que ? alors on devrait pouvoir dériver ? ? ?. Mais quelle est la quantitée d’information détenue dans ? ?    ¬ ?. Intuitivement il y a surcharge d’information, ce qui nous permet de dériver toutes les formules à partir d’une contradiction.

Vu que toutes les contradictions sont équivalentes, on utilisera ? pour représenter une contradiction.

Le fait que l’on peut tout déduire à partir d’une contradiction est formalisé par la règle suivante :

Le fait que ? represente une contradiction est formalisé par la règle suivante :

Comment introduire une négation?

Supposons que l’on fasse une hypothèse et que l’on arrive a déduire une contradiction, dans ce cas l’hypothèse est fausse. Ceci est formalisé par la règle de preuve suivante :

?      hyp.

·

·

·

                                                                                                             ?     fin hyp.

                                                                                                                               ¬?                  ¬ i



La logique propositionnelle Déduction naturelle (XXI)

On est maintenant en mesure de prouver le sequent de l’exemple introductif (taxi-train-invité) :

p ?  ¬ q ? r, ¬ r,p ? q


1

p ?  ¬ q ? r

prémisse

2

¬ r

prémisse

3

p

prémisse

4

¬ q

hyp.

5

p ? ¬ q

? i3,4

6

r

?e 1,5

7

?

¬ e6,2, fin hyp.4

8

¬ ¬ q

¬ i4 ? 7

9

q

¬ ¬ e8

Règles pour l’équivalence

?1 ? ?2 ? ?2 ? ?1

( ?i)

?1 ? ?2

?1 ? ?2

( ?e1)

?1 ? ?2

?1 ? ?2

( ?e1)

?2 ? ?1

La logique propositionnelle

Déduction naturelle (XXII)

Règles dérivées :

Notons que MT

est une règle dérivée. En effet :

1      ? ? ?      prémisse 2      ¬ ?      prémisse

3    ?   hyp.

4    ?   ?e 1,3

5    ?   ¬ e4,2, fin hyp.3

6    ¬ ?        ¬ i3 ? 5

La logique propositionnelle

Déduction naturelle (XXIII)

Autres règles dérivées :

                                                                                                     ¬ ?    hyp.

·

·

·

                                                                                                       ?        fin hyp.

?                       RAA

RAA=reductio ad absurdum

LEM

La logique propositionnelle

Déduction naturelle (XXIII)

A la fin du cours, nous prouverons que les règles de la déduction naturelle forme une méthode de preuves adéquate et complète.

La logique propositionnelle

Les formes normales (I)

Une formule est en forme normale conjonctive (FNC) ssi c’est une conjonction de disjonctions de littéraux, c’est-à-dire une formule de la forme :

Vi(Wj( ¬ )pi,j)

Une formule est en forme normale disjonctive (FND) ssi c’est une disjonction de conjonctions de littéraux, c’est-à-dire une formule de la forme :

Wi(Vj( ¬ )pi,j)

La logique propositionnelle

Les formes normales (II)

Exemples :

p ? (q ? ¬ r) ? ( ¬ p ? r)

est une formule en forme normale conjonctive. Tandis que

p ? (q ? ¬ r) ? ( ¬ p ? r)

est une formule en forme normale disjonctive.

La logique propositionnelle

Les formes normales (III)

Notons Prop(?) l’ensemble des propositions qui apparaˆ?ssent dans la formule ?.

Fonction associée à une formule :

F? : Valuation ?     {0,1} ou encore

F? : {0,1}Prop(?) ?      {0,1}

F? assigne à chaque valuation possible pour les propositions de ? la valeur 0 ou 1. On définit F? de la fac¸on suivante :

F?(V ) = [[?]]V

La logique propositionnelle

Les formes normales (III)

Proposition : deux formules ? et ? sont équivalentes ssi elles définissent la même fonction, c’est-à-dire F? = F?.

(Preuve laissée comme exercice)

Proposition : il existe au plus 22n formules, deux à deux non

équivalentes, du calcul propositionnel construit sur n propositions.

La logique propositionnelle Les formes normales (IV)

Théorème : Toute fonction F de {0,1}n dans {0,1} peut être représentée par une formule propositionnelle à n variables.

Preuve. Preuve par induction sur le nombre n de propositions. (i) n = 1 : les 4 fonctions possibles sont équivalentes à :

p, ¬ p, ¬ p ? p, ¬ p ? p. (ii) n > 1. Par HI, la propriété est vraie pour n-1. P = {p1, ,pn } et F : {0,1}P ? {0,1} peut être exprimée comme :

Par HI on a ?F|pn=1 et ?F|pn=0 et on construit la formule recherchée de la fac¸on suivante :

CQFD

Théorème : Toute formule de la logique propositionnelle est équivalente à une forme normale disjonctive et à une forme normale conjonctive.

Preuve. On raisonne par induction sur le nombre de propositions :

(i) |Prop(?) | = |   {p }| = 1

4 fonctions possibles exprimées par les formules suivantes : p, ¬ p, ¬ p ? p, ¬ p ? p, formules qui sont à la fois FNC, FND.

(ii) | Prop(?) | = |      {p1, ,pn }| = n > 1

Par HI le théorème est vrai pour n-1.

F?

=

pn ? ?1) ? (pn ? ?2)

=

pn ? ?1) ? (pn ? ?2)

ou`

?1

=

?11 ? ? ?1k

?2

=

?21 ? ? ?2l

de plus ¬ pn ? ?1 = (¬ pn ? ?11) ? ? ( ¬ pn ? ?1k) est en FND, et pn ? ?2 = (pn ? ?21) ? ? (pn ? ?2l) est en FND.

Pour la FNC, on utilise l’équivalence :

F?

=

pn ? ?1) ? (pn ? ?2)

=

(pn ? ?1) ? ( ¬ pn ? ?2)

CQFD

La logique propositionnelle

Les formes normales (V)

En pratique, on utilise les transformations successives suivantes pour obtenir les formes normales :

1.    élimination des connecteurs ? et ? grâce aux équivalences suivantes :

(? ? ?) ? ( ¬ ? ? ?)

                                                                                   (? ? ?) ? ( ¬ ? ? ?) ? (? ?  ¬ ?)

2.    entrer les négations le plus à l’intérieur possible :

                                                                                                    ¬ (? ? ?) ? ( ¬ ? ? ¬ ?)

                                                                                                    ¬ (? ? ?) ? ( ¬ ? ? ¬ ?)

3.    utilisation des distributivité de ? et ? l’un par rapport à l’autre :

(? ? (? ? ?)) ? (? ? ?) ? (? ? ?)

(? ? (? ? ?)) ? (? ? ?) ? (? ? ?)

Exercices :

–    appliquer ces transformations à :

¬ (p ? (q ? r))

–    prouver l’adéquation des équivalences;

–    prouver la complétude des règles de transformation.

La logique propositionnelle

Résolution (I)

Rappel : Une formule propositionnelle ? est un littéralsi et seulement si? est une proposition ou la négation d’une proposition.

Donc, p et ¬ p sont des littéraux.

Une formule propositionnelle ? est une clausesi

? = ?1 ? ?2 ? ? ?n ou` n ? 1 et chaque ?i, 1 ? i ? n, est un littéral .

Par exemple, p ?    ¬ q ? r est une clause.

La logique propositionnelle Résolution (II)

Une clause

                                                       ¬ a1 ?   ¬ a2 ? ?      ¬ am ? b1 ? b2 ? ? bn

ou` a1,a2, ,am,b1,b2, ,bn sont des propositions peut être écrite comme l’implication :

a1 ? a2 ? ? am ? b1 ? b2 ? ? bn

ou encore comme une paire d’ensembles (?,?) ou`

? = {a1,a2, ,am } et ? = {b1,b2, ,bn }. Donc ? contient l’ensemble des propositions qui apparaissent négativement dans la clause, alors que ? contient l’ensemble des propositions qui apparaissent positivement dans la clause.

Proposition : Pour toute formule ?, il existe un ensemble fini de

clauses equivalentes.

(preuve laissée comme exercice. Indice : utiliser la résultat sur les formes normales.)

La logique propositionnelle

Résolution (IV)

Une clause (?,?) est

–    une clause négativesi ? = ? ;

–    une clause positivesi ? = ? ;

–    une clause videsi ? = ? = ? ;

–    une clause tautologiquesi ? ? ? 6= ?.

La logique propositionnelle

Résolution (V)

La fonction d’interprétation V satisfait la clause C = (?,?) si et seulement si il existe a ? ? tel que V (a) = faux ou si il existe b ? ? tel que V (b) = vrai. Formellement [[(?,?)]]V = vrai ssi ? a ? ? : V (a) = faux ou ? a ? ? : V (a) = vrai.

Et donc,

Une clause vide n’est satisfaite par aucune fonction d’interprétation.

Une clause tautologique est satisfaite par toutes les fonctions d’interprétation.

La logique propositionnelle Résolution (VI)

Nous étendons maintenant les notions de satisfaction, satisfaisabilité, validité et conséquence logique aux ensembles de clauses :

Un ensemble de clauses S est satisfait par la fonction d’interprétation Vsi et seulement si on a que V |=C pour toute clause C ? S.

Un ensemble de clauses S est satisfaisable si et seulement si il existe une fonction d’interprétation qui satisfait S.

Un ensemble de clauses S est valide si et seulement si toute fonction d’interprétation V satisfait S.

Une clause C est une conséquence logique d’un ensemble de clauses S, ce que l’on note S |= Csi et seulement si pour toute valuation V qui satisfait S, V satisfait C.

La logique propositionnelle

Résolution (VII)

Et donc,

L’ensemble vide de clause est valide et donc satisfaisable.

Soit S un ensemble de clauses et C une clause tautologique, S ? {C } est satisfaisable (respectivement valide) si et seulement siS est satisfaisable (respectivement valide).

Ce dernier corollaire nous indique que, lorsque l’on veut vérifier la satisfaisabilité ou la validité d’un ensemble de clauses, on peut toujours supprimer les clauses tautologiques.

La logique propositionnelle

Résolution (VIII) : Règle de coupure

Etant données deux clauses C1 = (?1,?1) et C2 = (?2,?2) et une proposition p telles que p ? ?1etp ? ?2, c’est-à-dire p apparaˆ?t positivement dans C1 et négativement dans C2, on obtient la clause C3 = (?3,?3) par coupure avec p ou` :

– ?3 = ?1 ? (?2 \        {p }); – ?3 = (?1 \       {p }) ? ?2.

On note par  le fait que C3 est déductible de C1,C2 par coupure sur la proposition p.

La logique propositionnelle

Résolution (IX) : Règle de coupure (suite)

Théorème : SiC3 = (?3,?3) est une clause obtenue par la règle de coupure à partir des clauses C1 = (?1,?1) et C2 = (?2,?2) alorsC3 est une conséquence logique de C1 et C2.

Preuve. Pour montrer que la règle de coupure est adéquate, nous devons montrer que

.

Par définition de |=, cela revient à montrer que pour toute fonction d’interprétation V telle que V |=C1 et V |=C2, on a V |=C3. Par contraposition, cela revient à montrer que si V 6 |=C3 alors soit V 6 |=C1 soit V 6 |=C2. Par définition de , nous savons que ?3 = ?1 ? (?2 \ {p }) et ?3 = (?1 \ {p }) ? ?2. On sait également que siV ne satisfait pas C3, alors

? q ? ?3 : V (q) = vrai et ? q ? ?3 : V (q) = faux

Par définition de ?3 et ?3, on a en particulier :

–    ? q ? ?1 : V (q) = vrai (2);

–    ? q ? ?2 \ {p } : V (q) = vrai;

–    ? q ? ?1 \ {p } : V (q) = faux; – ? q ? ?2 : V (q) = faux (1).

Il suffit maintenant de considérer les deux valeurs possibles pour V (p) :

–    siV (p) = vrai alors on a ? q ? ?2,V (q) = vrai et (1), donc on a

V 6  |=C2 ;

–    siV (p) = faux alors on a ? q ? ?1,V (q) = faux et (2), donc on a V 6 |=C1 ;

?

La logique propositionnelle

Résolution (X)

Soit S un ensemble de clauses et C une clause. Une preuve de C par coupure à partir de S est une suite finie de clauses

C1,C2, ,Cn ou` Cn = C et pour tout i, 1 ? i ? n, on a que :

–    soit Ci ? S ;

–    ou il existe k,l, 1 ? k < l < i et une proposition p tels que

.

On note par S ?cC le fait que C est déductible de S par coupure.

La logique propositionnelle

Résolution (XI)

Théorème : Pour tout ensemble de clauses S et pour toute clause C, siS ?cCalorsS |= C.

Preuve. La preuve est laissée en exercice. Indices : utiliser la validité de la règle de coupure et raisonner par induction sur la longueur de la preuve.

?

La logique propositionnelle

Résolution (XII) : Complétude de la méthode de preuve

par coupure

Une réfutation d’un ensemble S de clauses par coupure est une dérivation de la clause vide à partir de S.

Théorème : Si il existe un réfutation de S par coupure alors l’ensemble de clauses S est non satisfaisable.

Preuve. La preuve de cette propriété est laissée comme exercice.

?

La logique propositionnelle

Résolution (XIII)

Comment peut-on se servir de la notion de réfutation pour vérifier qu’une formule ? est une conséquence logique d’un ensemble fini de formules ?1,?2, ,?n ? Il suffit de procéder de la fac¸on suivante : 1. transformer la conjonction

?1 ? ?2 ? ? ?n

en un ensemble fini S de clauses (cette transformation est toujours possible);

2.    de la même fac¸on, transformer ¬ ? en un ensemble S? de clauses;

3.    construire l’ensemble de toutes les clauses D déductibles par coupure de S ? S?.

La logique propositionnelle

Résolution (XIV)

Si la clause vide appartient à l’ensemble D alors l’ensemble D n’est pas satisfaisable et donc l’ensemble S ? S? ne l’est pas non plus, ce qui revient à dire que la formule ?1 ? ?2 ? ? ?n ? ¬ ? n’est pas satisfaisable et donc ? est une conséquence logique de l’ensemble {?1,?2, ,?n }.

La logique propositionnelle Résolution (XV)

Théorème : Si un ensemble S de clauses est non satisfaisable et ne contient pas la clause vide, alors il existe une proposition p et deux clauses C1,C2 ? S telles que p ? ?2 et p ? ?1.

Preuve. Nous établissons ce lemme en raisonnant par l’absurde. Faisons l’hypothèse que S est non satisfaisable, ne contient pas la clause vide et ne contient pas une proposition p avec la propriété requise. Par conséquent, on sait que toute proposition p apparaissant dans S a la propri été suivante : – pour toute clause Ci ? S, p ? ?i ou p 6? ?i ? ?i ;

– ou pour toute Ci ? S, p ? ?i ou p 6? ?i ? ?i ;

Autrement dit, p apparaˆ?t soit toujours négativement ou toujours positivement. Notons que c’est exactement la négation de la propriété que l’on veut établir. Montrons maintenant que l’on peut établir la satisfaisabilité de S, ce qui constitue une contradiction.

Pour satisfaire S, il suffit de prendre la fonction d’interprétation V tel que V (p) = vrai si p apparaˆ?t toujours positivement dans S et V (p) = faux si p apparaˆ?t toujours négativement dans S.

Une fois que V est définie pour chaque proposition comme expliqué ci-dessus et vu que S ne contient pas la clause vide, il est facile d’établir que V |=S, ce qui est une contradiction avec l’hypothèse de départ qui dit que S est non satisfaisable.

?

La logique propositionnelle

Résolution (XVI)

Les propositions d’une clause C = (?,?) sont l’ensemble des propositions qui apparaissent dans l’ensemble ? ? ?; cet ensemble est noté Prop(C). Les propositions d’un ensemble S de clauses est l’ensemble SC?S Prop(C); cet ensemble est noté Prop(S).

Etant donné un ensemble S de clauses et une proposition p, on note Sp le sous-ensemble de clauses de S qui contiennent la proposition p, c’est-à-dire, Sp = {C ? S | p ? Prop(C) }.

La logique propositionnelle

Résolution (XVII)

Soit S un ensemble de clauses qui ne contient pas de clauses tautologiques et une proposition p telle qu’il existe C1,C2 et p ? ?1 et p ? ?2, donc p apparaˆ?t négativement dans C1 et positivement dans C2. On définit le résolvant de S par p comme l’ensemble des

clauses

c’est-à-dire l’ensemble des clauses que l’on peut obtenir à partir de deux clauses de S par coupure sur p; nous notons par Res(S,p) cet ensemble de clauses et par RRes(S,p) le sous-ensemble de clauses non tautologiques de Res(S,p).

La logique propositionnelle

Résolution (XVII)

Etant donné un ensemble S de clauses et une proposition p, l’ensemble de clauses S? = S \ {Sp } ? RRes(S,p) est l’ensemble obtenu par un pas de résolution sur p à partir de S.

La logique propositionnelle

Résolution (XVIII)

Proposition : Si S? est un ensemble de clauses obtenu à partir de S (qui ne contient pas de clauses tautologiques) par un pas de résolution sur p alors :

1.    S? ne contient pas de clauses tautologiques;

2.    S? est satisfaisable si et seulement siS est satisfaisable;

3.    Prop(S?) = Prop(S) \  {p }.

(preuve laissée comme exercice)

La logique propositionnelle

Résolution (XVIII)

Proposition : Si un ensemble S de clauses est non satisfaisable, alors on peut déduire la clause vide à partir de S avec un nombre fini de pas de résolution.

(preuve laissée comme exercice)

Et donc,

Pour tout ensemble de clauses S et pour toute clause C tel que S |= C alors on a S ?cC.

La logique du premier ordre

Introduction (I)

Les situations suivantes ne sont pas “modélisables”en logique propositionnelle :

–    certains étudiants assistent à tous les cours;

–    aucun étudiant n’assiste à un cours non intéressant;

–    dans toute salle d’examen, il y a un étudiant qui, s’il échoue, alors tout le monde échoue.

La logique du premier ordre

Introduction (II)

Ce qui manque à la logique propositionnelle, c’est de pouvoir parler d’objets, de propriétés d’objets et de mettre en relation des objets.

Par exemple :

–    tel cours est intéressant;

–    tel étudiant assiste au cours de logique.

La logique du premier ordre

Introduction (III)

La logique propositionnelle ne permet pas de quantifier sur les objects. On ne peut pas par exemple exprimer : – tous les cours sont intéressants; – il existe des cours intéressants.

La logique du premier ordre nous permettra de modéliser ces situations. Par exemple, l’énoncé“tous les cours sont intéressants” sera modélisé par :

? x : Cours(x) ? Interessant(x)

La logique du premier ordre

Plan

1.     Langages du premier ordre

–     construction des termes

–     construction des formules

–     variables libres, variables liées

2.     Sémantique

–     structures et langages

–     structures et satisfaction des formules

–     formules valides, formules équivalentes

–     substitution

3.     Formes prénexes et formes de Skolem

4.     Déduction naturelle pour le premier ordre

5.     Procédure de résolution pour le premier ordre

–   mise sous forme de clauses

–   unification

–   méthode de résolution

–   modèles de Herbrand

Logique du premier ordre

Langages du premier ordre (I)

Pourquoi “langages” du premier ordre?

–   car ils partagent des caractéristiques avec beaucoup de langages comme les langages de programmation, les langues naturelles, les langages d’interrogation de bases de données,

–   il existe une grande variété de langages du premier ordre, chacun

étant déterminé par son vocabulaire;

–   ces langages permettent de représenter des relations mais également des fonctions.

Logique du premier ordre

Langages du premier ordre (II)

L’expression“premier ordre” différencie ces langages des langages “d’ordre supérieur”, dans lesquels il est possible de quantifier sur d’autres objects que les variables. (par ex. sur les fonctions, prédicats, )

Logique du premier ordre

Langages du premier ordre (III) : alphabet

L’alphabet d’un langage du premier ordre comporte d’abord les symboles suivants qui sont communs a` tous ces langages :

–   les connecteurs ¬ , ? , ? , ?, ? ;

–   les parenthèses (,);

–   le quantificateurs universel ? et le quantificateur existentiel ? ; – un ensemble infini V de symboles de variables x,y,z, .

Logique du premier ordre

Langages du premier ordre (IV) : alphabet

Un langage L de la logique du premier ordre est caractérisé par :

–   des symboles de relations ou prédicats , p,q,r,s ;

–   des symboles de fonctions , f,g,h, ; – des symboles de constantes , c,d,e,

A chaque prédicat p, respectivement fonction f, on associe un entier strictement positif appelé l’arité de p, respectivement de f, c’est-à-dire le nombre d’arguments de p, respectivement f.

On utilise le prédicat “=” pour dénoter l’égalité. Si “=” fait partie du vocabulaire du langage L , on dit que L est égalitaire .

Logique du premier ordre

Langages du premier ordre (V) : alphabet

Exemples de langages :

–    L 1 contient un prédicat unaire r et une constante c;

–    L 2 contient un prédicat binaire r, une fonction unaire f, deux symboles de fonctions binaires g et h, et deux constantes c et d.

Logique du premier ordre

Langages du premier ordre (VI) : construction des termes

L’ensemble des termes d’un langage L est le plus petit ensemble qui contient les symboles de constantes et de variables et qui est clos par application des fonctions.

L’ensemble des termes, noté T , est le plus petit ensemble satisfaisant :

1.    tout symbole de constante ou variable est un terme;

2.    si f est un symbole de fonction d’arité n et t1,t2, ,tn sont des termes alors f(t1,t2, ,tn) est un terme.

Remarque : les prédicats ne fournissent pas des termes; ils serviront pour construire les formules.

Logique du premier ordre

Langages du premier ordre (VII) : construction des termes

Exemples :

–    les seuls termes du langage L 1 sont la constante c et les variables; – les expressions suivantes sont des termes du langage L 2 :

–    f(c);

–    f(h(f(c),d));

–    f(y);

–    f(h(f(x),f(d))).

Un terme est clos s’il est sans variable. Par exemple f(c) est clos.

Logique du premier ordre

Langages du premier ordre (VIII) : construction des formules

L’ensemble des formules atomiques d’un langage L est l’ensemble des formules de la forme :

–    p(t1,t2, ,tn) ou p est un prédicat d’arité n et t1,t2, ,tn sont des termes du langage L ;

–    t1 = t2 si L est égalitaire et t1,t2 sont des termes du langage L .

Logique du premier ordre

Langages du premier ordre (IX) : construction des formules

L’ensemble des formules du langage L , que l’on désigne par F ( L ), est le plus petit ensemble qui satisfait :

1.    toute formule atomique est une formule;

2.    si ? est une formule alors ¬ ? est une formule;

3.    si ? et ? sont des formules alors ? ? ?, ? ? ?, ? ? ?, ? ? ? sont des formules;

4.    si ? est une formule et x une variable, alors ? x · ? et ? x · ? sont des formules.

Logique du premier ordre

Langages du premier ordre (X) : exemples de formules

La formule r(c) ?    ¬ ? x · r(x) est une formule du langage L 1.

Exemples de formules du langage L 2 :

–       ? x ·        ? y(g(x,y) = c ? g(y,x) = c)

–       ? x ·        ¬ (f(x) = c)

Logique du premier ordre

Langages du premier ordre (XI) : décomposition d’une formule

Toute formule d’un langage du premier ordre se décompose de manière unique sous l’une, et une seule, des formes suivantes : – une formule atomique,

–       ¬ ?, ou` ? est une formule,

–       ? ? ?, ? ? ?, ? ? ?, ? ? ? ou` ? et ? sont des formules,

–       ? x · ? ou ? x · ? ou` ? est une formule et x est une variable. Une formule ? est une sous-formule de ? si ? apparaˆ?t dans la décomposition de ?.

A nouveau, les parenthèses utilisées pour contrecarrer les règles de précédence ou rendre les formules plus lisibles seront omises dans les définitions (mais utilisées dans les exemples).

Logique du premier ordre

Langages du premier ordre (XII) : variables libres et liées

Une occurrence d’une variable dans une formule est un couple constitué de cette variable et d’une place effective, c’est-à-dire qui ne suit pas un quantificateur.

Par exemple, dans la formule

r(x,z) ?     ? z · (r(y,z) ? y = z)

la variable x possède une occurrence, la variable y deux et la variable z trois.

Logique du premier ordre

Langages du premier ordre (XIII) : variables libres et liées

Une occurrence d’une variable x dans une formule ? est une occurrence libre si elle ne se trouve dans aucune sous-formule de ?, qui commence par une quantification ? x ou ? x. Dans le cas contraire, l’occurrence est dite liée.

Une variable est libre dans une formule si elle a au moins une occurrence libre dans cette formule.

Une formule close est une formule sans variable libre.

Logique du premier ordre : Sémantique

Structures et langages (I)

Une structure M pour un langage L se compose d’un ensemble non vide M, appelé le domaine et :

–    d’un sous-ensemble de Mn, noté rM, pour chaque symbole de prédicat r d’arité n dans L ;

–    d’une fonction de Mm dans M, notée fM, pour chaque symbole de fonction f d’arité m dans L ;

–    d’un élément de M, noté cM, pour chaque symbole de constante c dans L .

Logique du premier ordre : Sémantique

Structures et langages (II)

Un ensemble D muni d’une relation unaire E et d’un élément distingué a est une structure pour le langage L 1 = {r,c }, notée (D,E,a).

On peut également donner un exemple plus concret d’interprétation pour le langage L 1 = {r,c } en prenant l’ensemble des nombres naturels comme domaine d’interprétation, l’ensemble des nombres premiers pour interpréter le prédicat r et le nombre 2 pour interpréter la constante c.

L’ensemble des réels RR permet de construire une structure pour L 2 = {r,f,g,h,c,d } de la fac¸on suivante :

–    on interprète le prédicat r comme l’ordre ? sur les réels;

–    on interprète f comme la fonction +1, g comme +, et h comme × ;

–    on interprète les constantes c et d comme 0 et 1.

On note cette structure

M 2 = (RR, ? ,+1,+, × ,0,1)

Logique du premier ordre : Sémantique

Structures et satisfaction des formules (I)

Etant donné un ensemble de variables V et un domaine M, une valuation pour les variables de V dans M est une fonction v : V ? M qui attribue à chaque variable x ? V , une valeur v(x) ? M.

Etant données une structure M et une valuation v pour V , on définit inductivement la valeur d’un terme t (dont les variables sont dans V ), que l’on note tM,v, de la fac¸on suivante : – si t est une constante c, alors tM,v est cM ;

–    si t est la variable x alors tM,v est v(x);

–    si t est de la forme f(t1,t2, ,tn) et si  est bi alors tM,v = fM(b1,b2, ,bn);

Logique du premier ordre : Sémantique

Structures et satisfaction des formules (II)

Soit le langage L 2 = {r,f,g,h,c,d } et M 3 la structure

(NN, ? ,+1,+, × ,0,1), ou` NN est l’ensemble des entiers positifs (nombres naturels). La valeur du terme t1 ? g(y,h(c,x)) pour une valuation v telle que v(x) = 3, v(y) = 4, v(z) = 6 est :

La valeur du terme t2 ? f(g(d,h(y,z))) est :

Logique du premier ordre : Sémantique

Structures et satisfaction des formules (III)

Une formule ? construite sur un langage L est satisfaite dans une structure M et pour une valuation v donnant une valeur aux variables de l’ensemble V , noté M ,v |=?, si et seulement si : – si L est égalitaire et ? ? t1 = t2 alors ? est vrai ssi ;

–    si  pour i = 1,2, ,n, alors ? est vraie ssi (b1,b2, ,bn) ? rM ;

Logique du premier ordre : Sémantique

Structures et satisfaction des formules (IV)

–    si ? ?       ¬ ?1, ? ? ?1 ? ?2, ? ? ?1 ? ?2, ? ? ?1 ? ?2,

? ? ?1 ? ?2 alors la valeur de ? est calculée à partir des valeurs de ?1 et ?2 comme dans le cas propositionnel;

–    si ? ?       ? x · ?, alors ? est vraie ssi il existe une valuation v? et une valeur u ? M telles que

                                                                                                                                                  )     si y 6? x

v?(y) = u      si y ? x ?

et ? est vraie dans ( M ,v?), c’est-à-dire M ,v? |=? ;

Logique du premier ordre : Sémantique

Structures et satisfaction des formules (V)

–    si ? ? ? x · ?, alors ? est vraie ssi pour toute valuation v? et valeur u ? M telles que

?? v?(y) = v(y) si y 6? x v?(y) = u   si y ? x ?

? est vraie dans ( M ,v?);

La valeur d’une formule ? dans une structure M est l’ensemble W des valuations telles que pour toute valuation v ? W , M ,v |=?.

Logique du premier ordre : Sémantique

Structures et satisfaction des formules (VI)

Notons que, si ? est une formule close, alors sa valeur de vérité dans un couple (M ,v), ne dépend pas de v.

Dans le cas ou` une formule close ? est vraie dans une structure M , ce que l’on note,

                                                                                                                               M |=?

On dit que M est un modèle pour ?.

Logique du premier ordre : Sémantique

Structures et satisfaction des formules (VII)

Quelques exemples :

–    La structure (D,R,a) du langage L 3 = {r,c } est un modèle de la formule

                                                                                        ? x ·    ? y · (r(x,y) ? r(y,x))

ssi la relation R est symétrique.

–    La formule close suivante

? x · r(x,x)

                                                            ? ? x ·    ? y · (r(x,y) ? r(y,x))

                                                            ? ? x · ? y ·     ? z · (r(x,y) ? r(y,z) ? r(x,z))

exprime que si une structure (D,R,a) est un modèle de la formule, alors R est une relation d’équivalence.

–    la formule ? y · r(x,y) est vraie dans la structure (NN, ? ,+1,+, × ,0,1) et la valuation v ssi v(x) = 0.

–    la formule ? x ·      ? y · r(x,y) est vraie dans la structure

(NN, ? ,+1,+, × ,0,1);

–    la formule close

                                                                 ? x · ? z ·    ? y · (x = c ? g(h(x,y),z) = c)

du langage L 2 est vraie dans la structure (RR, ? ,+1,+, × ,0,1) et fausse dans la structure (NN, ? ,+1,+, × ,0,1).

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes (I)

La relation d’équivalence sur les formules permet de les classifier et de regrouper celles qui possèdent la même signification. L’une de ces classes de formules est particulièrement intéressante : les formules vraies dans toute structure. On appellera ces formules, les formules valides.

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes (II)

Soit ?(x1,x2, ,xn) une formule du premier ordre avec les variables libres x1,x2, ,xn. On appelle cloˆture universelle de ? la

formule

                                                                  ? x1 ·        ? x2 · ? xn · ?(x1,x2, ,xn)

Soit L un langage du premier ordre, on définit les notions suivantes :

–    une structure M satisfait une formule

?(x1,x2, ,xn)

si elle satisfait la clôture universelle de ?;

–    une formule ? est valide si elle est satisfaite par toutes les structures du langage L ;

–    deux formules ? et ? sont équivalentes si, pour toute structure M et pour toute valuation v, on a (M ,v) |=? ssi ( M ,v) |=?.

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes (III)

Théorème : deux formules ? et ? sont equivalentes si et seulement si la formule ? ? ? est valide.

Théorème : si, dans une formule, on remplace une sous-formule par une formule équivalente, alors on obtient une formule équivalente à la formule de départ.

(Preuves à faire comme exercices).

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes (IV)

Exercices : démontrer que

–    si ? et ? ? ? sont des formules valides, alors ? est une formule valide;

–    la formule (? x ·    ? y · ?(x,y)) ? ( ? y · ? x · ?(x,y)) est valide;

–    la formule (? y ·    ? x?(x,y)) ? ( ? x ·    ? y · ?(x,y)) n’est pas valide.

Montrons que la formule

                                                                               ? x. ? y.?(x,y) ?  ? y. ? x.?(x,y)

est valide

Rappel : soient

?

?

?1 ? ?2

?1

?

? x. ? y.?(x,y)

?2

?

? y. ? x.?(x,y)

? valide ssi pour toute structure µ : µ |= ?

? valide ssi pour toute structure µ : si µ |= ?1 alors µ |= ?2

? valide ssi pour toute structure µ : soit µ 6|= ?1, ou µ |= ?1 et µ |= ?2

or si µ |= ?1 alors pour toute valuation v,

? u ? Dµ : µ,v[x7?u] |= ? y.?(x,y)

si µ |= ?1 alors pour toute valuation v,

? u ? Dµ ? w ? Dµ : µ,v[x7?µ,y7?w] |= ?(x,y)

On a donc que ? w ? Dµ : µ,v[x7?u,y7?w] |= ?(x,y). Donc on sait que ?(x,y) est vérifié pour n’importe quelle valeur attribuée à y si on attribue à x la valeur u. Il suffit donc de choisir cette valeur lors de l’évaluation de la quantification existentielle dans la formule

? y ? x · ?(x,y)

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes (V)

Notion de substitution : étant donné un terme t et une variable x apparaissant dans ce terme, on peut remplacer toutes les occurrences de x par un autre terme t?. Le nouveau terme est dit obtenu par substitution de t? à x et est noté t(t?/x).

Exemple :

–    le résultat de la substitution de f(y,z) à x dans le terme h(x,y) est le terme h(f(y,z),y);

–    le résultat de la substitution de g(y,z) à x dans le terme g(x,x) est g(g(y,z),g(y,z)).

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes (VI)

Substitution dans les formules : avant d’effectuer la substitution d’un terme à une variable libre dans une formule, il est nécessaire de prendre quelques précautions. Sinon, la signification de la formule peut être complètement modifiée par un phénomène appelé capture de variables .

Exemple : soit ?(x) la formule ? y · g(y,y) = x. Dans la structure M = (NN, ? ,+1,+, × ,0,1), ou` g est interprété par l’addition, la signification de ?(x) est claire : ( M ,v) |= ?(x) ssi v(x) est pair. Si l’on remplace la variable x par z, cette signification est conservée. Par contre si l’on remplace la variable x par y, on obtient : ? y · g(y,y) = y qui est une formule close qui est vraie dans M (en effet, il suffit de choisir la valeur 0 pour la variable y).

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes (VII)

La substition d’un terme t à une variable libre x dans une formule ? est obtenue en remplac¸ant toutes les occurrences libres de cette variable par le terme t, sous réserve que la condition suivante soit vérifiée : pour chaque variable y apparaissant dans t, x n’a pas d’occurrence libre qui se trouve dans une sous-formule de ? commenc¸ant par une quantification ? y ou ? y. Le résultat de cette substitution, si elle existe, est une formule notée ?(t/x).

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes (VIII)

Exemple : le résultat de la substitution du terme f(z) à la variable x dans la formule ?(x) suivante :

                                                                  ((r(c,x) ?     ¬ x = c) ? ( ? yg(y,y) = x))

est la formule

                                                 ((r(c,f(z)) ?       ¬ f(z) = c) ? ( ? yg(y,y) = f(z)))

Notons que la substitution de y à x n’est pas possible dans cette même formule.

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes (IX)

Théorème : si ? est une formule, x est une variable libre dans ? et t un terme tel que la substitution de t à x dans ? soit définie, alors les formules

( ? x · ?(x)) ? ?(t/x) et

?(t/x) ? ( ? x · ?(x))

sont valides.

Preuve. Etant donnée une structure µ, on montre par induction sur la formule ? que la satisfaction de la formule ?(t/x) dans (µ,v) est équivalente à celle de la formule ?(x) dans (µ,v1) ou` v1 est obtenu à partir de v en donnant à x la valeur tµ,v. Les seuls cas qui nécessitent une justification sont ceux ou` :

? ? ? y.?

D’après l’hypothèse de la substitution de t à x, la quantification porte sur une variable y distincte à la fois de x et de toutes variables de t.

Il suffit donc d’examiner la satisfaction de ?(t/x) pour une interprétation v? égale à v sauf sur y. Compte tenu de l’hypothèse d’induction sur ?, la formule ?(t/x) est satisfaite par v?ssi ? est satisfaite par  ou` ,, qui est égale à tµ,v vu que v et v?

sont égales pour toutes les variables qui apparaissent dans t (qui sont différentes de y).

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes(X)

Les couples de formules suivants sont des exemples de formules équivalentes :

–    ? et ? x · ? si x n’est pas libre dans ?;

–    ? et ? x · ? si x n’est pas libre dans ?;

–    ? x · (? ? ?) et ( ? x · ?) ? ( ? x · ?)

–    ? x · (? ? ?) et ( ? x · ?) ? ( ? x · ?)

–    ? x · (? ? ?) et ? x · ( ¬ ? ? ?)

–    ? x · ? et ? y · ?(y/x) si x est libre dans ? et y n’apparaˆ?t pas dans ?

–    ? x · ? et ? y · ?(y/x) si x est libre dans ? et y n’apparaˆ?t pas dans ?

Si x n’est pas libre dans ?, on obtient les équivalences suivantes : – ? x · (? ? ?) et ( ? x · ?) ? ?

–    ? x · (? ? ?) et ( ? x · ?) ? ?

Logique du premier ordre : Sémantique

Formules valides, formules équivalentes(X)

Les équivalences suivantes nous permettent de faire passer en tête de formule tous les quantificateurs. Soit ? une formule, x une variable et ? une formule dans laquelle x n’est pas libre :

–    ¬ ? x · ? et ? x ·      ¬ ?

–    ¬ ? x · ? et ? x ·      ¬ ?

–    ( ? x · ?) ? ? et ? x · (? ? ?)

–    ( ? x · ?) ? ? et ? x · (? ? ?)

–    (? ? ? x · ?) et ? x · (? ? ?)

–    (? ? ? x · ?) et ? x · (? ? ?) – ( ? x · ?) ? ? et ? x · (? ? ?)

–    ( ? x · ?) ? ? et ? x · (? ? ?)

Notons également que les formules suivantes sont équivalentes :

–    ? x ·   ? y · ? et ? y ·      ? x · ?

–    ? x ·   ? y · ? et ? y ·      ? x · ?

Logique du premier ordre : Sémantique

Formules prénexes , formes de Skolem (I)

Objectif : définir une forme standard pour les formules du premier ordre.

Une formule ? est prénexe si et seulement si elle est de la forme

Q1x1 · Q2x2 · Qn · xn · ?

ou` chaque Qi est un quantificateur (existentiel ou universel), tous les xi sont différents et ? est une formule sans quantificateur.

Rappel : Formules équivalentes

1.    ?x · ? et ?y · ?(y/x) (x libre dans ? et y n’apparaˆ?t pas dans ?)

2.    ?x · ? et ?y · ?(y/x) (idem)

3.    ?x · (? ? ?) et ?x · ? ? ? (x non libre dans ?)

4.    ?x · (? ? ?) et ?x · ? ? ? (idem)

5.    ¬?x · ? et ?x · ¬?

6.    ¬?x · ? et ?x · ¬?

7.    (?x · ?) ? ? et ?x · (? ? ?) (x non libre dans ?)

8.    (?x · ?) ? ? et ?x · (? ? ?) (x non libre dans ?)

Théorème Pour toute formule de la logique du premier ordre, il existe une formule prénexe équivalente.

Preuve. Par induction sur la structure des formules.

CB : Si ? est une formule atomique. Evident.

CI :

–    ? ?    ¬ ? et ? est supposée équivalente à une forme prénexe

Q1x1.Q2x2Qnxn.??. Après application de (5) ou (6) on obtient :

ou` ; cette formule est en forme prénexe.

–    Si ? ?       ? x · ? alors on sait qu’il existe ?? ? ? en forme prénexe et donc ? ?  ? x · ?? est en forme prénexe.

–    Si ? ?       ? x · ?, justification similaire.

–    ? ? ?1 ? ?2. On sait par hypothèse d’induction qu’il existe 2 formules prénexes ?1, et ?2, telles que ? et ?.

             Il y a plusieurs cas à considérer. Soit ?,1 ?  ? x · ?,,1 ou

. Si x n’est pas libre dans ?,2 on applique (3) ou (8)

pour sortir la quantification. Si x est libre dans ?,2 on applique d’abord les propriétés (2) ou (1) (renommage) et on applique (3) ou (8) comme au dessus.

Finalement ? est équivalente à ? x · ( ) ou ? x · ( ) avec 1 quantificateur en moins à l’intérieur. On itère ensuite cette transformation.

–    ? ? ?1 ? ?2, idem mais avec (1), (2), (4), (7).

–    ? ? ?1 ? ?2

on sait que ? et ?. On utilise les règles pour ¬ et ? .

–    ? ? ?1 ? ?2 est équivalent à ? ? (?1 ? ?2) ? (?1 ? ?2).

Logique du premier ordre : Sémantique

Formules prénexes, formes de Skolem (II)

Exercice : donner la formule prénexe équivalente à la formule

                                                                 ? x · ? y · (      (r(x,y) ?    ¬ x = y)

                                                                                                                 ?     ? z(y = g(x,h(z,z))))

Pour cela, on transforme successivement la formule de la fa¸con suivante :

                                                                 ? x · ? y · (      (r(x,y) ?    ¬ x = y)

                                                                                                                 ?     ? z(y = g(x,h(z,z))))

                                   ? x ·   ? y · ((¬ r(x,y) ? x = y) ?      ? z(y = g(x,h(z,z))))

                                ? x · ? y ·      ? z · (( ¬ r(x,y) ? x = y) ? (y = g(x,h(z,z))))

Logique du premier ordre : Sémantique

Formules prénexes, formes de Skolem (III)

Nous adaptons les notions de littéral, clause et forme normale conjonctive/disjonctive pour la logique du premier ordre :

–    un littéral est une formule atomique ou une négation d’une formule atomique;

–    une clause est une disjonction de littéraux;

–    une formule prénexe

Q1x1 · Q2x2 · Qnxn · ?

est sous forme normale conjonctive, respectivement forme normale disjonctive, si la formule sans quantificateur ? est une clause ou une conjonction de clauses, respectivement une disjonction de conjonctions de littéraux.

Logique du premier ordre : Sémantique

Formules prénexes, formes de Skolem (IV)

Par exemple, la formule

                                ? x · ? y ·      ? z · (( ¬ r(x,y) ? x = y) ? (y = g(x,h(z,z))))

est sous forme normale conjonctive.

Théorème : toute formule de la logique du premier ordre est équivalente à une formule prénexe sous forme normale conjonctive (respectivement disjonctive).

Logique du premier ordre : Sémantique

Formules prénexes, formes de Skolem (V)

Skolémisation : suppression des quantificateurs existentiels.

Note : cette suppression ne fournit pas une formule équivalente, mais préserve la satisfaisabilité.

Quelques définitions :

–    une formule ? est dite universelle si elle est prénexe et si tous les quantificateurs qui apparaissent dans ? sont universels;

–    soit L un langage du premier ordre, un langage L ? est une extension de Skolem de L si L ? est obtenu en ajoutant à L une infinité de symboles de fonctions de chaque arité et une infinité

de symboles de constantes.

Logique du premier ordre : Sémantique

Formules prénexes, formes de Skolem (VI)

Une formule prénexe close ? de L ? est soit universelle, soit de la forme ? x1 · ? xk · ? x · ? ou` ? est prénexe. Dans ce dernier cas, il se peut que k = 0 et ? est de la forme ? x · ?. La transformation que l’on applique à ? si elle contient au moins un quantificateur existentiel, consiste à lui associer une formule

? x1 · ? xk · ?(f(x1, ,xk)/x),

ou` f est un symbole de fonction n’apparaissant pas dans la formule

?. Dans le cas particulier ou` k = 0, c’est-à-dire ? ?     ? x · ?, on lui associe la formule ?(c/x) ou` c est une constante n’apparaissant pas dans ?. La formule ?1 ainsi obtenue possède un quantificateur existentiel en moins que ?. Cette transformation est appelée pas de

Skolémisation .

Logique du premier ordre : Sémantique

Formules prénexes, formes de Skolem (VII)

Quand on écrit

? ? ? x ·  ? y · p(x,y)

en rapport avec une structure M , on exprime que pour chaque valeur a donnée à x, on peut choisir une valeur b pour y telle que



(a,b) ? pM

Notons que l’on peut “approximer” cela en associant à chaque valeur pour x une valeur fixe f(x) pour y, ou` f est une nouvelle fonction. Si on interpréte f comme

fM?(a) = b alors on aura (a,fM?(a)) ? pM

ou` M ? est une inteprétation qui est “compatible” avec M et qui interpréte la nouvelle fonction f.

Logique du premier ordre : Sémantique

Formules prénexes, formes de Skolem (VIII)

Nous avons parlé d’approximation, pourquoi?

Considérons à nouveau la formule

? ? ? x ·  ? y · p(x,y)

et une interprétation M 1 telle que

MM1 = {1,2} et

pM1 = {(1,1),(1,2),(2,1),(2,2) }

Logique du premier ordre : Sémantique

Formules prénexes, formes de Skolem (IX)

et considérons

?? ?    ? x · p(x,f(x))

avec f un nouveau symbole de fonction, et nous étendons M 1 en  pour interpréter f :

alors on a . Mais on considère M 2 avec

pM2 = {(1,1),(2,2) }

et  l’extension de M 2 avec à nouveau :

alors on a

M 2 |=? mais

Logique du premier ordre : Sémantique

Formules prénexes, formes de Skolem (X)

Intuitivement, en remplac¸ant la quantification existentielle par une fonction, on se limite à une dépendance fonctionnelle entre les variables x et y alors qu’en général on a des dépendances relationnelles entre variables (donc on limite le choix possible des modèles d’une formule).

On va maintenant formaliser cette notion de suppression des quantificateurs existentiels, appelée Skolémisation , et montrer que cette transformation préserve la satisfaisabilité mais pas la validité des formules.

Logique du premier ordre : Sémantique

Formules prénexes, formes de Skolem (XI)

Soit ? une formule close en forme prénexe du langage L ?, possédant n quantificateurs existentiels :

–    une forme de Skolem de ? est une formule obtenue en appliquant n fois successivement le pas de skolémisation;

–    les nouvelles fonctions et constantes introduites au cours de ces transformations s’appellent les fonctions et constantes de Skolem

.

Théorème : le pas de skolémisation préserve la satisfaisabilité des formules : soit ? une formule prénexe et ?1 une formule obtenue de ? par un pas de Skolémisation, alors ? est satisfaisable ssi ?1 est satisfaisable.

Preuve. Supposons que µ est un modèle de ?1.

1.    Si ? ? ? x1 · · ? xk · ? x · ? et ?1 ? ? x1 · · ? xk · ?(f(x1, ,xk)/x) et le résultat provient de la validité de la formule

                                    ? x1 · ·      ? xk · ?(f(x1, ,xk)/x) ?       ? x1 · ·  ? xk ·                    ? x · ?

2.    et si ? ? ? x · ? et ?1 ? ?(c/x) et le résultat de la validité de la formule ?(c/x) ? ? x · ?.

Supposons que µ soit un modèle de ? on va enrichir µ pour interpréter les termes de Skolem et satisfaire ?1.

1.    Soit ? ?       ? x1 · · ? xk ·       ? x · ? et ?1 ?    ? x1 · · ? xk · ?(f(x1, ,xk)/x).

On sait que µ |= ? et donc, pour n’importe quel vecteur de valeurs a1, ,ak ? Mµ, il existe une valeur a

µ |= ?(a1/x1, ,ak/xk,a)

on construit µ? en attribuant l’interprétation fµ?(a1, ,ak) = a pour chaque vecteur a1, ,ak. Il est claire que µ? |= ?1

2.    ? ?        ? x · ? et ?1 ? ?(c/x)

On sait qu’il existe une valeur v pour x telle que µ,v |= ?.

Donc il suffit de prendre cµ? = v(x) et on a µ? |= ?(c/x)

Logique du premier ordre

Résolution (I)

La résolution est une méthode de démonstration automatique pour les formules du premier ordre sous forme de clauses.

Pour faire de la résolution dans le premier ordre on a besoin de la notion d’unification .

La méthode de résolution et l’unification sont utilisées dans les algorithmes sous-jacents à la programmation logique (par exemple Prolog).

Logique du premier ordre

Résolution (II)

Un préalable à l’application de la méthode de résolution est la mise

sous forme clausale .

Considérons un ensemble ? de formules closes et une formule close ?, la question“? est une conséquence logique de ??” est équivalente par réfutation à la question suivante : “l’ensemble de formules ? ?      {¬ ? } est-il non satisfaisable?”. Une manière de répondre à cette question consiste à transformer cet ensemble de formules en un ensemble S de clauses, puis appliquer les règles de résolution aux clauses de S.

Logique du premier ordre Résolution (III)

La suite de transformations qui permet de passer d’un ensemble de formules à un ensemble de clôtures universelles de clauses, est constitué par :

–    la mise sous forme prénexe et normale de chacune des formules de ?; notons que cette transformation préserve l’équivalence;

–    la mise sous forme de Skolem de chacune des formules obtenues; cette transformation préserve la satisfaisabilité mais pas l’équivalence;

–    la distribution des quantificateurs universels par rapport aux conjonctions dans chacune des formules; cette transformation préserve l’équivalence;

–    la décomposition des conjonctions en ensembles de clôtures universelles de clauses; cette dernière transformation préserve l’équivalence.

Logique du premier ordre

Résolution (V)

Un exemple de mise sous forme de clauses : soit L un langage comportant deux symboles de prédicats unaires p,q et

? = {( ? x · p(x)) ?  ? y · p(y), ? x · (p(x) ? q(x))} et ? ? ( ? x · ¬ q(x)) ?      ? y · p(y)

On applique la suite des transformations à l’ensemble ? ? {¬ ? } :

–    Formes prénexe :

                                                                                             ? x · ? y · ( ¬ p(x) ? p(y)),

? x · (p(x) ? q(x)),

                                                                                             ? x · ? y · ( ¬ q(x) ? ¬ p(y))

Logique du premier ordre Résolution (VI)

–    Skolémisation :

                                                                                               ? x · ? y · ( ¬ p(x) ? p(y)),

? x · (p(x) ? q(x)),

                                                                                               ¬ q(c) ? ¬ p(d)

ou` c et d sont de nouveaux symboles de constantes, – les formules restent les mêmes, – les clauses obtenues sont :

( ¬ p(x) ? p(y)),

(p(x) ? q(x)),

¬ q(c),

¬ p(d)

Logique du premier ordre

Résolution (VII)

Théorème : si S est l’ensemble des formules obtenues à partir de ? en appliquant la suite des transformations précédentes, alors S est satisfaisable si et seulement si ? est satisfaisable.

Preuve : les transformations 1,3 et 4 préservent l’équivalence des formules et la transformation 2 préserve le fait d’être satisfaisable.

Logique du premier ordre

Résolution (VIII) : unification

Pour pouvoir appliquer la règle de résolution aux clauses de S, il est nécessaire de savoir reconnaˆ?tre si deux, ou plusieurs, formules atomiques peuvent être unifiées, c’est-à-dire s’il existe une substitution des variables de ces formules par des termes du langage, qui permette de les rendre égales. L’algorithme utilisé pour résoudre ce problème s’appelle l’algorithme d’unification.

Logique du premier ordre

Résolution (IX) : unification

Définitions préalables à la présentation de l’algorithme d’unification :

–    une substitution ? est une fonction de l’ensemble des variables dans l’ensemble des termes;

–    dans la suite, le domaine d’une substitution, c’est-a`-dire {x | ?(x) 6= x}, est supposé fini. Si le domaine est {x1,x2, ,xn} et si pour i = 1,2, ,n, ti est le terme ?(xi), la substitution ? est notée :

(t1/x1,t2/x2, ,tn/xn)

–    la substitution ? appliquée a` une formule ?(x1,x2, ,xn), notée ?(?), est la formule obtenue en substituant le terme ?(xi) a` chaque occurrence de la variable xi dans ?, pour tout i = 1,2, ,n.

Notons que cette notion de substitution généralise la notion de substitution d’un terme à une variable que nous avons introduite précédement.

Logique du premier ordre

Résolution (XI) : unification

Exemple : dans la suite nous considérons un langage L comportant un symbole de prédicat binaire r, un symbole de fonction unaire f, deux symboles de fonctions binaires g,h, un symbole de fonction ternaire k et deux constante c,d. Soit la substitution

? : (g(d,z)/x,f(z)/y,d/z)

et la clause

C ? r(x,f(y)) ?      ¬ r(g(y,c),z)

la clause ?(C) est

r(g(d,z),f(f(z))) ?       ¬ r(g(f(z),c),d)

Logique du premier ordre

Résolution (XII) : unification

Un ensemble de formules atomiques

{A1,A2, ,An }

est unifiable s’il existe une substitution ? telle que ?(A1) = ?(A2) = = ?(An).

Ainsi, les formules atomiques

r(x,f(y)),r(g(y,c),z),r(g(d,v),f(d))

sont unifiables à l’aide de la substitution

(g(d,c)/x,d/y,f(d)/z,c/v)

ou` x,y,z,v sont des variables et c,d des constantes.

Logique du premier ordre

Résolution (XIII) : unification

Proposition : si ? est une substitution, alors il existe une fonction unique ¯? de l’ensemble des termes dans lui-même, qui prolonge ? et qui respecte la structure des termes.

En effet, la valeur de ¯?(t) est définie par induction sur le terme t :

–    si t est une constante c, on pose ¯?(c) = c;

–    si t est une variable x, on pose ¯?(x) = ?(x);

–    si t est de la forme f(t1,t2, ,tn) et si on suppose définis ¯?(t1), ?¯(t2), , ¯?(tn) on pose ¯?(t) = f?(t1),?¯(t2), ,?¯(tn)).

Logique du premier ordre

Résolution (XIV) : unification

Conséquences de la définition de ¯? :

–    pour calculer l’effet d’une substitution à un termet(x1,x2, ,xn), il suffit de substituer le terme ?(xi) à chaque occurrence de la variable xi dans le terme t;

–    si ? est une substitution et t un terme clos, c’est-à-dire sans variable, alors ¯?(t) = t.

Dans la suite, on notera ? au lieu de ¯?.

Logique du premier ordre

Résolution (XV) : unification

–    une substitution ? est un unificateur de deux termes t et t? si ?(t) = ?(t?);

–    soit un ensemble fini de couples de termes, noté

; une substitution ? est un

unificateur de S si, pour tout );

–    un unificateur ? de S est principal si pour tout unificateur ? de

S, il existe une substitution ? telle que ? = ? ? ? ;

–    une substitution ? est un unificateur principal d’un ensemble fini de formules atomiques {A1,A2, ,An } si ?(A1) = ?(A2) = = ?(An) et si pour tout unificateur ? de cet ensemble de formules, il existe une substitution ? telle que ? = ? ? ?.

Logique du premier ordre

Résolution (XVI) : unification

Les termes t = h(x,g(y,z)) et t? = h(f(z),v) sont-ils unifiables?

Si ? est un unificateur de t, t?, il doit satisfaire : ?(t) = ?(t?), c’est-à-dire

h(?(x),g(?(y),?(z))) = h(f(?(z)),?(v))

La substitution ? doit donc satisfaire :

?(x) = f(?(z)), ?(v) = g(?(y),?(z))

Il suffit donc de prendre deux termes arbitraire u,u? respectivement pour ?(y),?(z) et ? satisfaisant :

?(x) = f(u?) et ?(v) = g(u,u?)

pour obtenir un unificateur de t et t?.

Logique du premier ordre

Résolution (XVII) : unification

La hauteur i d’un terme d’un langage du premier ordre mesure la complexité de ce terme.

Formellement : soit L un langage du premier ordre. La suite des ensembles T n est définie par récurrence sur l’entier n :

–    T 0 est la réunion de l’ensemble des constantes et de celui des variables;

–    T n est supposé défini; on prend t ?     T n+1 si t ?     T n ou si t est de la forme f(t1,t2, ,tk) pour un symbole de fonction f d’arité k et chaque ti ?    T n.

La hauteur d’un terme t est le plus petit entier n tel que t ?  T n.

Notons la propriété suivante :

Théorème : si ? est une substitution, alors pour tout terme t, la hauteur de ?(t) est supérieure ou égale à la hauteur de t.

Logique du premier ordre

Résolution (XVIII) : unification

Théorème : Si ? et ?? sont des unificateurs principaux de deux termes t et t?, alors ils sont égaux à une permutation des variables près.

Preuve. Si ? et ?? sont des unificateurs principaux de t et t? alors il existe ? et ? tels que

? = ? ? ?? et ?? = ? ? ? et donc ? = ? ? ? ? ?

et donc ? ? ? est l’identité

Comme ? n’agit que sur les variables de ?(t), l’action de ? ? ? sur ces variables est l’identité.

Notons que ? transforme une variable x en une autre variable. En effet, comme nous venons de le montrer, une substitution ne peut associer un terme fonctionnel à une variable de ? sinon ? ne pourrait pas réattribuer une variable au terme ainsi créé. En effet cela contredirait le résultat qu’une substitution ne peut pas faire descendre la hauteur d’un terme. De même l’association d’une constante serait irréversible.

Le même raisonnement peut être fait sur ?.

Logique du premier ordre

Résolution (XIX) : unification

Quelques définitions supplémentaires :

–    la hauteur d’un couple de termes (t,t?) est le minimum des hauteurs des termes t,t? ;

–    la hauteur d’un ensemble fini S de couples de termes est le maximum des hauteurs des couples de S ;

–    un système est un ensemble fini de couples de termes.

Logique du premier ordre

Résolution (XX) : unification

Lemme : Etant donné un système S de couples de termes, il existe une suite finie de transformations qui préservent les unificateurs de S, s’il en existe, et le transforme en un système S1 de hauteur nulle, appelé système simplifié .

Preuve. Soit S un système de hauteur h > 0. La transformation que nous allons définir ci-dessous permet soit de montrer que S n’est pas unifiable, soit de déterminer un système S? qui est de hauteur h?< h et qui a les mêmes unificateurs que S.

La transformation peut-être définie de la fac¸on suivante :

–    remplacer si possible chaque couple (t,t?) de termes de hauteur h > 0 par un ensemble de couples de termes de hauteur h?< h – Soient deux termes t et t? tels que

t     =          f(t1,t2, ,tn)

alors soit :

–    f 6= f? et les termes t et t? ne sont pas unifiables et donc S n’a pas d’unificateur

–    f = f? et donc n = m et on remplace le couple (t,t?) par

l’ensemble des couples (ti,ti,) pour i = 1,2, ,n, qui sont de hauteurs h?< h et ont les mêmes unificateurs que (t,t?).

Après applications successives de ces transformations, on obtient, si S est unifiable, un ensemble S? de hauteur h = 0. On peut simplifier cet ensemble en appliquant les deux règles suivantes :

–    s’il existe plusieurs couples identiques dans S?, on n’en conserve qu’un;

–    on élimine les couples de la forme (t,t) ou` t est un terme.

Ces transformations préservent les unificateurs.

Logique du premier ordre

Résolution (XXI) : unification

Exemple : soit le système constitué par le seul couple (t,t?) avec

t = k(f(c,g(x4,x5)),f(c,g(x5,x4)),x2) et t? = k(x2,x2,x6)

le système simplifié est l’ensemble des couples :

–    (f(c,g(x4,x5)),x2)

–    (f(c,g(x5,x4)),x2)

–    (x2,x6)

Logique du premier ordre

Résolution (XXI) : unification

Définition : Soit S? un système simplifié. Un couple de termes dans S? est dit réductible s’il se compose d’une variable x et d’un terme t dans lequel x n’apparaˆ?t pas. Sinon il est dit irréductible .

Lemme : Si S? est un système simplifié qui possède un couple irréductible, alors S? n’est pas unifiable.

Preuve. Un couple irréductible peut être composé des trois manières suivantes

–    (c,d) deux constantes distinctes;

–    (f(t1, ,tn),c) un terme fonctionnel et une constante;

–    (x,f( ,x, )) par l’absurde, considérons ? qui unifie x et f( ,x, ) on a ?(x) = f( ,x, ) or la hauteur de ?(x) est strictement inférieure a` la hauteur de ?(f( ,x, )) et donc les deux termes ne peuvent pas être égaux.

Logique du premier ordre

Résolution (XXII) : unification

Algorithme d’unification :

? := {(x,x) | x ? Var}; Unifiable := true

Tant que S 6= ? et Unifiable = true

1.     la phase de simplification transforme S, si c’est possible, en un système simplifié S?, sinon elle s’arrête (et il n’existe pas d’unificateur) : Unifiable := false ;

2.     la phase de test permet d’arrêter l’algorithme en présence de termes irréductibles (et il n’existe pas d’unificateur) : Unifiable := false ;

3.     la phase de réduction consiste a` prendre un couple réductible (x,t), ou

(t,x), dans S?, a` considérer la ? := ?[x ? t] et

S1 := {(?(t),?(t?)) | ?(t) 6= ?(t?) ? (t,t?) ? S?}; a

4.     S := S1

Si Unifiable=true alors retourner ?. a La variable x n’apparaissant pas dans t, la substitution ? vérifie ?(x) = t.

Logique du premier ordre

Résolution (XXIII) : unification

Lemme : si S? est un système simplifié de couples réductibles, (x,t) l’un de ces couples de S? et ? la substitution définie par ?(x) = t : si ? est un unificateur du système S?, alors il existe une substitution ? telle que ? = ? ? ?.

Théorème : l’algorithme d’unification termine et produit, dans le cas ou le système S est unifiable, une suite de substitutions ?1,?2, ,?n dont la composée est un unificateur principal du système S.

Preuve. L’algorithme termine soit dans une phase de simplification ou de test par impossibilité de réaliser une unification, soit au après un nombre fini n d’étapes par un système vide. Dans ce dernier cas, il est facile de voir, par induction sur i ? n, que tout unificateur de S est de la

forme :

? ? ?i ? ?i?1 ? ? ?1 ou` ? est un unificateur de Si : en particulier, tout unificateur de S est de la forme ? ? ?n ? ?n?1 ? ? ?1 ou` ? est un unificateur de Sn.

Le système (Sn) étant vide, n’importe quelle substitution ? convient et ?n ? ? ?1 est alors un unificateur principal de S.

Logique du premier ordre

Résolution (XXIV) : unification

Dans l’exemple précédent, tous les couples de S? sont réductibles et l’on peut choisir le premier

(f(c,g(x4,x5)),x2)

La substitution ?1 de la phase de réduction est définie par :

?1(x2) = f(c,g(x4,x5))

et ?1 est l’identité sur les autres variables. Le système S1 = ?1(S?) est égal à :

–    (f(c,g(x5,x4)),f(c,g(x4,x5)))

–    (f(c,g(x4,x5)),x6)

Logique du premier ordre

Résolution (XXIV) : unification

On applique à nouveau une phase de simplification au système S1, et on obtient le système :

{(c,c),(x5,x4),(x4,x5), (f(c,g(x4,x5)),x6) }

que l’on peut simplifier en

–    (x4,x5)

–    (f(c,g(x4,x5)),x6)

Ces deux couples sont réductibles.

Logique du premier ordre

Résolution (XXV) : unification

En choisissant la substitution

?2(x4) = x5

le système réduit est S2 égal à :

(f(c,g(x5,x5)),x6)

Ce système étant de hauteur nulle et constitué d’un seul couple réductible, la réduction s’effectue à l’aide de la substitution

?3(x6) = f(c,g(x5,x5))

Le système réduit associé est vide et un unificateur principal du système S est

? = ?3 ? ?2 ? ?1

Logique du premier ordre

Résolution (XXVI) : règle

Etant donnée une clause C, les formules atomiques de C apparaissant sans négation sont dites positives et celles apparaissant précédées d’une négation sont dites négatives. La clause C peut être notée (?,?) ou` ?, respectivement ?, est l’ensemble des formules atomiques négatives, respectivement positives de C.

La règle de résolution permet de déduire une nouvelle clause à partir de deux clauses C1 et C2. Elle opère en deux temps : d’abord unification d’un ensemble de formules atomiques négatives de C1 et positives de C2, puis coupure sur la formule atomique obtenue.

Logique du premier ordre

Résolution (XXVII) : règle

Soit C1 = (?1,?1) et C2 = (?2,?2) deux clauses séparées , c’est-à-dire sans variables communes (il suffit de renommer des variables dans une des clauses si nécessaire).

S’il existe P1 ? ?1 et N2 ? ?2 tels que l’ensemble des formules atomiques P1 ? N2 soit unifiable et si ? est un unificateur principal, la nouvelle clause C, déduite des deux clauses C1,C2 par résolution, est définie par

? = ?(?1) ? ?(?2 \ N2) et

? = ?(?1 \ P1) ? ?(?2)

La clause C est dite déduite par résolution des clauses C1 et C2 relativement à l’unificateur ? (et P1, N2). On dit que la clause C est un résolvant de C1 et C2 relativement à ?.

Logique du premier ordre

Résolution (XXVII) : règle

Exemple : soit L un langage comportant les symboles de prédicats p,q,s unaires, r binaire, f un symbole de fonction unaire et les clauses :

–    C1 ?   ¬ s(z) ? p(z) ? q(z)

–    C2 ?   ¬ p(f(y)) ? r(x,y)

Logique du premier ordre

Résolution (XXVIII) : règle

La clause suivante est le résolvants de C1 et C2 :

P1 = {p(z) }, N2 = {¬ p(f(y))}

Donc, nous devons unifier {p(f(y)),p(z) }

On considère donc le système S = {(z,f(y))} de hauteur zéro qui est unifié par ?(z) = f(y).

Nous pouvons maintenant calculer C3 (la clause résolvante) comme

C3 ? (?(C1) \ ?(P1)) ? (?(C2) \ ?(N2)) et donc

C3 ?      ¬ s(f(y)) ? q(f(y)) ? r(x,y)

Logique du premier ordre

Résolution (XXIX) : règle

Soit S un ensemble de clauses et C une clause. Une preuve par résolution de C à partir de S est une suite finie de clauses

C1,C2, ,Cn telles que Cn = C et pour tout i = 1,2, ,n :

–       soit Ci est une clause de S ;

–       soit il existe 1 ? j,k < i tels que Ci soit un résolvant de Cj,Ck. L’existence d’une preuve C par résolution à partir de S est notée S ?R C. Une réfutation de S est une preuve de la clause vide à partir de S. La clause vide est notée × .

Logique du premier ordre Résolution (XXX) : règle

Exercice. Montrez que l’ensemble de clauses :

–       ¬ p(x) ? p(y)

–       p(z) ? q(z)

–       ¬ p(c) – ¬ q(d)

possède une réfutation.

Logique du premier ordre

Résolution (XXXI) : règle

La correction de la méthode de résolution est exprimée par la propriété suivante : l’existence d’une réfutation de S implique que S n’a pas de modèle. Pour établir ce résultat, nous prouvons d’abord l’adéquation d’un pas de coupure (formalisée dans le lemme suivant).

Lemme : si C est un résolvant de C1, C2 alors C¯ est une conséquence logique de C¯1 ? C¯2.

(la clôture universelle de C est notée C¯)

Preuve. On a besoin de la propriété suivante dans la démonstration du lemme.

Soit B(x1, ,xk) une clause et µ une structure pour le langage L .

Si ? est une substitution telle que pour i = 1,2, ,k :

?(xi) = ti(y1, ,yl)

et b1, ,bl ? Mµ, on pose :

La clause B satisfait alors : µ,[a1, ,ak] |= B ssi µ,[b1, ,bl] |= ?(B) .

Nous pouvons maintenant aborder la preuve du lemme. Les clauses C1,C2 et C, résolvant de C1,C2 relativement à l’unificateur ? (pour L1 et L2) peuvent être notées sous la forme suivante :

C1        ?        G1 ? (F1 ? L1)

C2        ?       (F2 ? L2) ? D2

et C ? (? (G1) ? ? (F2)) ? (? (F1) ? ? (D2))

ou` L1 est la disjonction des formules atomiques positives et L2 la conjonction des formules atomiques négatives qui sont unifiées par ?, donc :

?(L1) = ?(L2)

On va maintenant établir la contraposée du lemme. On suppose donc qu’il existe µ tel que µ 6|= C¯. En d’autres termes, nous supposons qu’il existe µ et b1,b2, ,bl ? Mµ tels que

µ,[b1, ,bl] |= ¬ C

On va maintenant établir que µ 6|= C¯1 ou µ 6|= C¯2.

Par hypothèse, µ,[b1, ,bl] |= ¬ C, donc on a que µ et [b1, ,bl] sont tels que :

µ,[b1, ,bl] |= (? (G1) ? ? (F2))

et µ,[b1, ,bl] |= ¬ (? (F1) ? ? (D2))

Soient x1,x2, ,xk les variables apparaissant dans C1,C2 et ti les termes définis par

? (xi) = ti (y1, ,yl) pour i = 1,2, ,k.

La suite des ai est définie par

Vu qu’on a ?(L1) = ?(L2), deux cas sont possibles :

1.    Soit µ,[b1, ,bl] |= ?(L2) et donc µ,[a1, ,ak] |= L2 d’après la propriété rappelée précédemment.

De la même manière on sait que µ,[a1, ,ak] |= F2 et également µ,[a1, ,ak] |= ¬D2.

Donc µ,[a1, ,ak] satisfait la négation de C2.

2.    Soit µ,[b1, ,bl] |= ¬?(L1) et donc µ,[a1, ,ak] |= ¬L1. De même µ,[a1, ,ak] |= G1 et µ,[a1, ,ak] |= ¬F1. et donc µ,(a1,a2, ,ak) satisfait la négation de la clause C1.

Dans les deux cas, l’une des formules de  est fausse dans µ.

Corollaire : Si S ?R C, alors C¯ est une conséquence logique de S. En particulier, s’il existe une réfutation de S, alors S n’a pas de modèle.

Logique du premier ordre

Résolution (XXXIV) : Modèle de Herbrand

Soit T l’ensemble des termes du langage L .

Le domaine de Herbrand H est l’ensemble des termes clos, c’est-à-dire sans variables, de L . Donc H est le plus petit sous-ensemble de T contenant les constantes et clos par application des fonctions. Si L ne contient pas de constante, on lui en ajoute une.

La base de Herbrand B est l’ensemble des formules atomiques closes de L .

Logique du premier ordre

Résolution (XXXIV) : Modèle de Herbrand

Le domaine et la base de Herbrand vérifient les conditions suivantes :

1.    si L a un nombre fini de prédicats et de constantes, mais sans fonctions, alors H et B sont finis;

2.    si l’ensemble des fonctions de L est non vide, alors H et B sont infinis dénombrables.

Logique du premier ordre

Résolution (XXXIV) : Modèle de Herbrand

Exemples de domaines et de bases de Herbrand :

–                                                          si L comporte deux prédicats unaires p,q et deux constantes c,d, alors

–                                                          H = {c,d } ;

–                                                          B = {p(c),p(d),q(c),q(d) }.

–                                                          si L comporte deux prédicats unaires p,q, une fonction unaire f et une constante c, – H = {c } ? {fn(c) | n ? 1} ;

                          B =      {p(c),q(c) }? ,

–                                                          .

{p(fn(c)),q(fn(c)) | n ? 1}

Logique du premier ordre

Résolution (XXXV) : Modèle de Herbrand

Une structure de Herbrand H pour le langage L est une structure telle que :

–                                                          l’ensemble de base est le domaine de Herbrand;

–                                                          pour tout symbole de fonction f d’arité m, l’interprétation de f est la fonction qui à (t1,t2, ,tm) ? Hm associe le terme f(t1,t2, ,tm) (chaque terme est interprété par lui-même).

Pour compléter l’interprétation, il suffit pour chaque formule atomique close r(t1,t2, ,tn) de préciser quelle est la valeur de vérité de cette formule dans H : il faut définir une fonction V : B ? {0,1}. Une telle fonction définie sur un sous-ensemble de la base de Herbrand est appelée une structure partielle.

Soit ? une formule close . Un modèle de Herbrand de ? est une structure de Herbrand qui satisfait ?.

Implication : vu que B est fini ou dénombrable, on peut énumérer les structures partielles de Herbrand.

Logique du premier ordre

Résolution (XXXVI) : Modèle de Herbrand

Lemme : Soit ? une formule universelle close , ? possède un modèle si et seulement si elle possède un modèle de Herbrand.

Preuve. Montrons tout d’abord que si ? possède un modèle µ alors on peut construire un modèle de Herbrand H pour cette formule. Rappelons que, pour définir un modèle de Herbrand, il suffit de définir quelles sont les formules de la base de Herbrand qui sont vraies ou celles qui sont fausses. On sait que

? ? ?x1 ?xk · ?

ou` ? est une formule sans quantificateur. On définit la structure de Herbrand H de la fac¸on suivante : pour toute formule atomique close p(t1, ,tn), on pose

V (p(t1, ,tn)) = 1 ssi µ |= p(t1, ,tn).

Il est alors facile de montrer que µ |= ? ssi H |= ?, par induction sur la structure des formules.

L’autre direction est triviale car un modèle de Herbrand est un modèle particulier.

Implication de ce théorème : pour tester si une formule universelle close est satisfaisable ou non, on peut se restreindre a` lui chercher un modèle de Herbrand.

Logique du premier ordre

Résolution (XXXVII) : Modèle de Herbrand

Etant donnée une formule close universelle ? de la forme ? x1 · ? x2 · ? xn · ?, une formule ? est appelée instance de ? si elle est obtenue en substituant dans ? des termes clos t1,t2, ,tn respectivement aux variables x1,x2, ,xn.

Lemme : Soit ? un ensemble de fomules universelles closes. Si ? n’a pas de modèle de Herbrand, alors il existe un nombre fini d’instances de formules de ? qui n’ont pas de modèle.

(preuve omise)

Logique du premier ordre

Résolution (XXXVII) : Modèle de Herbrand

Représentation de la classe des modèles de Herbrand par des arbres sémantiques :

Un arbre sémantique est associé à une énumération {An } des formules atomiques closes ( B est fini ou dénombrable).

On va utiliser les arbres sémantiques pour énumérer les structures partielles de Herbrand pour une base B donnée (rappel : il suffit de déterminer la valeur de vérité de chaque formule atomique close de B ).

Logique du premier ordre

Résolution (XXXVII) : Modèle de Herbrand

Un arbre sémantique pour B est un arbre binaire dont les arêtes sont étiquetées par des formules atomiques closes de telle sorte que : – il existe un seul noeud de niveau 0, appelé racine;

– pour chaque noeud u de niveau n ? 1, une arrête partant de ce noeud est étiqueté par la formule An et l’autre arête par la formule ¬ An.

Une feuille est un noeud terminal de l’arbre. Une branche est un chemin constitué de noeuds, qui conduit de la racine à une feuille de l’arbre.

Logique du premier ordre

Résolution (XXXVIII) : Modèle de Herbrand

A     chaque noeud u d’un arbre sémantique est associée une valuation partielle V u sur B , et donc une structure de Herbrand partielle, notée M u : si u est un noeud de niveau n, c’est la valuation partielle définie en prenant la valeur 1 sur les formules atomiques étiquetant les arêtes menant de la racine au noeud u.

D’autre part, il existe un ordre partiel sur l’ensemble des noeuds de l’arbre : u < u? si et seulement si la valuation V u? prolonge strictement la valuation V u.

Logique du premier ordre

Résolution (XXXIX) : Modèle de Herbrand

Exemple d’arbre sémantique, pour la base de Herbrand

B     = {p(a),p(b) } (arbre donné au cours)

Notons que, si la base de Herbrand considérée est infinie, alors l’arbre sémantique est infini également.

Logique du premier ordre

Résolution (XL) : Modèle de Herbrand

Soit A un arbre sémantique et S un ensemble (fini) de clauses.

–    un noeud u de l’arbre A réfute une clause C de S s’il existe une substitution ? qui associe à chaque variable de la clause C un terme clos telle que la structure partielle M u rend fausse la clause ?(C);

–    un noeud u est un noeud d’échec pour S si

–    il existe une clause de S qui est réfutée par u;

–    pour tout noeud u?< u, il n’existe pas de clause dans S qui soit réfutée par u?.

–    un arbre sémantique A est fermé pour l’ensemble des clauses de S si sur toute branche de l’arbre, il existe un noeud d’échec pour S.

Logique du premier ordre

Résolution (XLI) : Modèle de Herbrand

Exemple d’arbre sémantique fermé. Considérons la base de Herbrand suivante :

B = {p(c),q(c),p(f(c)),q(f(c)), ,p(fn(c)),q(fn(c)), } et considérons les trois clauses suivantes :

–    C1 ?   ¬ p(x) ? q(x)

–    C2 ? p(f(y))

–    C3 ?   ¬ q(f(c))

Nous allons construire une partie suffisante de l’arbre sémantique (infini) associé à B pour montrer que la conjonction des clauses C1, C2 et C3 est non satisfaisable.

Logique du premier ordre

Résolution (XLI) : Modèle de Herbrand

(arbre donné au cours)

Logique du premier ordre

Résolution (XLIII) : Modèle de Herbrand

Théorème : un ensemble S de clauses est non satisfaisable si et seulement si il existe un arbre sémantique fermé pour S.

Preuve. D’après la définition des arbres sémantiques, toute structure de Herbrand correspond à une branche de l’arbre. On a également vu qu’un ensemble de clauses S est satisfaisable ssi S a un modèle de Herbrand.

S’il existe un arbre sémantique fermé pour S cela veut dire que chaque branche contient un noeud d’échec et toute structure de Herbrand réfute au moins une clause de S. Aucune structure de Herbrand n’est un modèle de S. Dans le cas contraire, au moins une branche de l’arbre semantique ne contient pas de réfutation (ne contient pas de noeud d’échec) et donc cette branche constitue un modèle de Herbrand pour l’ensemble de clauses de l’ensemble S.

Remarque : contrairement au cas propositionnel, la propriété, pour un ensemble de clauses du premier ordre, d’être satisfaisable n’est pas décidable en général : en effet le problème revient à vérifier si un arbre sémantique, qui peut être infini, est fermé ou non. Notons tout de même que, si l’on se restreint aux langages ne possédant qu’un nombre fini de symboles de relations et de constantes et pas de symboles fonctionnels, alors H et B sont finis et donc le problème devient décidable et se ramène au cas propositionnel.

Logique du premier ordre

Résolution (XLIV) : Modèle de Herbrand

Théorème : Un ensemble de clauses S est non satisfaisable si et seulement si il existe une réfutation de S par résolution.

Programmation Logique

Résolution et dérivations SLD (I)

La programmation logique repose sur une stratégie spécifique de la résolution, appelée Sélection Linéaire Définie . La stratégie SLD est une stratégie basée sur la résolution linéaire ou`, à chaque étape, une clause de l’ensemble de départ est utilisée.

Notons que la méthode n’est pas complète en général, mais elle est complète lorsqu’elle est appliquée à une classe particulière de clauses, appelées clauses définies .

Soit S un ensemble de clauses et C une clause. Une preuve de C par résolution linéaire est dite par entrée, si à chaque étape, le résolvant est obtenu en utilisant une clause de S.

Programmation Logique

Résolution et dérivations SLD (II)

Quelques notions nécessaires :

–    une clause définie (aussi appelée clause de Horn ) est une clause de la forme :

?1 ? ?2 ? ? ?n ? ?

ou` ?1,?2, ,?n avec n ? 0, et ? sont des formules atomiques. La formule ? s’appelle la tête de la clause et la conjonction ?1 ? ?2 ? ? ?n le corps.

–    Un programme logique est un ensemble fini de clauses définies.

Programmation Logique

Résolution et dérivations SLD (III)

–    Soit P un programme logique, G une clause négative, nommée but , et une clause C. Une preuve de C par résolution à partir de P ?        {G} est dite L       D si elle est linéaire par entrée et si la première étape de résolution utilise le but G. L’existence d’une telle preuve est notée

P ?   {G}    ?LDC

–    Une réfutation L  D de P ?        {G} est une preuve L D de la clause vide à partir de P ?       {G}.

Programmation Logique

Résolution et dérivations SLD (IV)

Exemple : soit L un langage comportant deux symboles de relations binaires q,r et deux symboles de constantes a,b, P le programme logique constitué des clauses {C1,C2,C3 } et G le but ¬ q(x,b). – C1 ? (r(x,y) ? q(y,z)) ? q(x,z)

–    C2 ? q(x,x)

–    C3 ? r(a,b)

Programmation Logique

Résolution et dérivations SLD (V)

L’ensemble P ? {G} possède deux réfutations L D : – la première :

–    la seconde :

Programmation Logique

Résolution et dérivations SLD (VI)

Le théorème suivant rend valide l’utilisation de la résolution L       D dans le cadre de la programmation logique (clauses définies) :

Théorème : tout programme logique P possède un modèle de Herbrand. De plus, si G est une clause négative telle que P ? {G} ne possède pas de modèle, alors il existe une réfutation L D de P ? {G}.

Montrons d’abord qu’un programme logique a toujours un modèle, et en particulier un modèle de Herbrand. En effet, le résolvant de deux clauses définies est une clause définie :

?11 ? ? ?n11 ? ?1?21 ? ? ?2n2 ? ?2

?(?11 ? ? ?1n1 ? ?21 ? ? ?2i?1 ? ?i2+1 ? ? ?2n2) ?? ?(?2)

En particulier, on ne pourra jamais déduire la clause vide. La résolution étant complète, on sait qu’un programme logique est toujours satisfaisable.

La résolution L D est complète. Si P ? G n’a pas de modèle alors P ? G possède une réfutation linéaire (par complétude de cette méthode). Une étape de résolution ne peut utiliser deux clauses négatives et le résolvant de l’application d’une clause définie avec une clause négative est une clause négative. Un résolvant négatif ne peut provenir que d’une clause négative et d’une clause définie. C’est le cas de la clause vide dans une réfutation. Dans un arbre de réfutation linéaire de P ? G par réfutation linéaire, il existe donc une branche dont toutes les étiquettes sont des clauses négatives : cette branche commence par G, qui est la seule clause négative de P ? G. Et donc on doit utiliser à chaque étape une clause de P vu qu’on a que des clauses négatives.

Programmation Logique

Résolution et dérivations SLD (VII)

Une dérivation SLD de P ?            {G} est une suite (Gi,Ci,?i)i?1

éventuellement infinie, telle que :

–    G0 = G et (Gi)i?1 est une suite de buts,

–    (Ci)i?1 est une suite de clauses de P,

–    (?i)i?1 est une suite d’unificateurs principaux telle que pour chaque i ? 1, Gi+1 est un résolvant de Gi,Ci+1 relativement à l’unificateur ?i.

Programmation Logique

Résolution et dérivations SLD (VIII)

Une dérivation SLD finie de P ?       {G} peut :

–    soit réussir si c’est une réfutation de P ?   {G},

–    soit échouer si elle se termine par un but, qui n’est pas la clause vide, tel que l’atome sélectionné dans le but ne s’unifie avec la tête d’aucune clause de P.

Programmation Logique

Prolog (I)

Nous allons nous intéresser à une implémentation particulière de la résolution SLD. Cette implémentation de la programmation logique est appelée Prolog et est très répandue.

Prolog voit la résolution SLD comme un processus opérationnel de calcul appliqué à un programme logique P et à un but G, dont le résultat, appelé aussi réponse, est :

–    soit une réponse, positive ou négative, si le but G est sans variable, suivant que G est une conséquence logique ou non du programme P ;

–    soit une substitution obtenue par composition des unificateurs principaux d’une réfutation de P ?       {G}, puis par restriction aux variables de G;

–    soit une absence de réponse dans le cas d’une dérivation infinie.

Programmation Logique

Prolog (III) : syntaxe

La clause (p(x,y) ? q(z,w)) ? r(x,w) est exprimé en Prolog avec la syntaxe suivante :

r(X,W) : ? p(X,Y ),q(Z,W).

La clause positive p(a,x) est notée

p(a,X).

Programmation Logique Prolog (IV) : un programme

1.    equivalent(X,X).

2.    equivalent(X,Y ) : ? equivalent(Y,X).

equivalent(X,Y ),

3.    equivalent(X,Z) : ? equivalent(Y,Z).

4.    equivalent(a,b)

5.    equivalent(b,c)

Programmation Logique

Prolog (V) : implémentation de SLD

Prolog implémente une stratégie particulière de recherche qui peut être spécifiée à l’aide :

–    d’une règle de calcul;– d’une stratégie de recherche.

Dans les interpréteurs Prolog standards, la règle de calcul consiste à sélectionner l’atome le plus a` gauche dans un but et la recherche s’effectue en profondeur d’abord, en examinant les clauses du programme dans l’ordre d’écriture.

Programmation Logique

Prolog (VI) : implémentation de SLD

L’implémentation utilise une pile des buts. Un état courant de la pile représente la dérivation examinée actuellement :

–    lorsque l’atome sélectionné dans le but est au sommet de la pile et s’unifie avec la tête d’une clause, le résolvant est empilé et devient le nouveau but courant;

–    lorsqu’il existe pas de clause dont la tête puisse s’unifier avec l’atome sélectionné dans le but courant, ce but est dépilé et il y a alors backtracking pour examiner à nouveau le but précédent avec les clauses suivantes, dans l’ordre d’écriture.

Programmation Logique

Prolog (VII) : implémentation de SLD

Illustrons cette stratégie de recherche sur un exemple. Considérons le programme P suivant :

1.    p(X,X) : ? q(X,Y ),r(X,Z).

2.    p(X,X) : ? s(X).

3.    q(b,a).

4.    q(a,a).

5.    q(X,Y ) : ? r(a,Y ).

6.    r(b,Z).

7.    s(X) : ? q(X,a).

(traité au cours)

Programmation Logique

Prolog (VIII) : implémentation de SLD

Considérons le but G = {¬ p(X,X) }. Rappelons-nous que, si nous arrivons à dériver la clause vide de P ?       {¬ p(X,X) }, alors on sait que p(X,X) est une conséquence logique de P.

Une dérivation est représentée à l’aide d’un arbre, appelé arbre

SLD. Le long des branches de l’arbre, nous noterons les clauses de P qui sont utilisées pour obtenir le résolvant. On respectera également la convention suivante : les successeurs sont listés de gauche à droite dans l’ordre de leur apparition dans le programme. Un chemin est un succès s’il se termine par une réponse positive, que l’on notera × . Un chemin est un échec s’il se termine avec une clause G? telle qu’il n’existe aucune clause du programme avec laquelle on peut résoudre sur l’atome le plus à gauche de G?.

Programmation Logique

Prolog (IX) : implémentation de SLD

Nous avons vu dans l’exemple précédent que, parmi les six chemins possibles, trois terminent en échec, deux terminent avec un succès et la substitution {X/b }, et un autre succès avec la substitution {X/a}.

Notons encore que le prouveur de théorèmes au coeur de Prolog cherche dans l’arbre SLD après une branche à succès en essayant d’abord le chemin le plus à gauche. C’est-a`-dire que Prolog tente de résoudre le but courant avec la première clause de P qui permet l’application d’un pas de résolution. Dans notre exemple, Prolog utilisera donc les clauses 1,3,6 du programme pour obtenir la réponse correcte : la substitution {X/b }.

Programmation Logique

Prolog (X) : implémentation de SLD

Si le prouveur de théorèmes atteint un noeud d’échec (failure) alors il backtrack. C’est-a`-dire qu’il remonte le chemin qu’il vient de parcourir jusqu’au moment ou` il trouve une branche à droite qui doit encore être parcourue. S’il y a plus d’une de ces branches, alors le prouveur de théorèmes prend celle qui est la plus à gauche. Le prouveur de théorèmes répète l’opération jusqu’au moment ou` il trouve un chemin à succès. (il se peut qu’il ne s’arrête jamais) Programmation Logique

Prolog (XI) : implémentation de SLD

Considérons P sans la clause 3 :

1.    p(X,X) : ? q(X,Y ),r(X,Z).

2.    p(X,X) : ? s(X).

3.

4.    q(a,a).

5.    q(X,Y ) : ? r(a,Y ).

6.    r(b,Z).

7.    s(X) : ? q(X,a).

(traité au cours)

Programmation Logique

Prolog (XII) : implémentation de SLD

La procédure de backtracking est également utilisée lorsque nous demandons à Prolog une seconde réponse.

Par exemple, avec le programme original P, si nous posons la question

? ? p(X,X).

On obtient la réponse X = b ?. Si nous demandons une deuxième réponse (en entrant “;”), le prouveur de théorèmes backtrack du noeud à succès jusqu’au moment ou` il rencontre un noeud avec un chemin alternatif. Quand il trouve un tel noeud il recommence la recheche à partir de ce noeud sur la branche la plus à gauche non encore empruntée.

Programmation Logique

Prolog (XIII) : implémentation de SLD

Complétude de la résolution SLD et Prolog.

Si le prouveur de théorèmes répond “non”. Nous savons que P ?  {G} est satisfaisable et donc il n’existe pas de substitution pour laquelle le but est une conséquence logique de P.

Malheureusement, du point de vue de la complétude, Prolog est implémenté suivant une procédure de recherche en profondeur d’abord. En effet, le prouveur de théorèmes tente d’aller le plus profond possible dans un chemin avant d’essayer un autre chemin. Une alternative à la recherche en profondeur d’abord serait la recherche en largeur d’abord. En général, la recherche en profondeur d’abord est plus efficace. Malheureusement, elle entraˆ?ne l’incomplétude de l’implémentation de Prolog.

Programmation Logique

Prolog (XIV) : implémentation de SLD

Le théorème général de complétude garantit que si P ?        {G} est insatisfaisable, alors il existe une réfutation-SLD (nécessairement finie) qui commence avec G. Notons que s’il y a une réfutation de longueur n alors on peut toujours la découvrir avec une recherche en largeur d’abord qui parcourt tous les chemins de longueur n. Malheureusement, on n’a pas une telle garantie avec une recherche en profondeur d’abord. Le problème est que certains chemins peuvent être infinis. Ce phénomène est illustré sur l’exemple suivant.

Programmation Logique

Prolog (XV) : implémentation de SLD

Considérons le programme P?? (seul la clause 6 diffère) :

1.    p(X,X) : ? q(X,Y ),r(X,Z).

2.    p(X,X) : ? s(X).

3.    q(b,a).

4.    q(a,a).



5.    q(X,Y ) : ? r(a,Y ).

6.    r(W,Z) : ? r(b,Z).

7.    s(X) : ? q(X,a).

Programmation Logique

Prolog (XVI) : implémentation de SLD

Nous pouvons constater en analysant l’exemple précédent que l’ordre des clauses a de l’importance. En effet, si on réordonne le programme P?? en intervertissant les clauses 1 et 2, le prouveur de théorèmes trouvera la réponse {X/b } et ensuite {X/a} et ce n’est que si on demande une troisième réponse que le prouveur de théorèmes entrera sur un chemin infini.

Malheureusement, un réordonnancement des clauses ne suffit pas toujours. La recherche en profondeur d’abord est intrinsèquement incomplète.

Programmation Logique

Prolog (XVII) : implémentation de SLD

En effet, reconsidérons l’exemple suivant :

1.    equivalent(X,X).

2.    equivalent(X,Y ) : ? equivalent(Y,X).

equivalent(X,Y ),

3.    equivalent(X,Z) : ? equivalent(Y,Z).

4.    equivalent(a,b)

5.    equivalent(b,c) et le but G ? ¬ equivalent(c,a).

Programmation Logique

Prolog (XVIII) : implémentation de SLD

Notons d’abord que equivalent(c,a) est clairement une conséquence logique du programme. Le problème est que, peu importe dans quel ordre apparaissent les clauses 1 et 2 dans le programme ci-dessus, une recherche en profondeur d’abord ne pourra utiliser qu’une seule des deux clauses. Il est également facile de voir que si on supprime une des deux clauses, equivalent(c,a) n’est plus une conséquence logique du programme.

Programmation Logique

Prolog : exemples de programmes (I)

Considérons le programme Prolog suivant : parent(luc,anne). parent(marie,anne). parent(henry,marie). parent(henry,thierry). parent(thierry,noel). parent(julie,helene). ancetre(X,X). ancetre(X,Y ) : ? parent(X,Y ). ancetre(X,Y ) : ? parent(X,Z),ancetre(Z,Y ). ancetre(X,Y ) : ? parent(Z,Y ),ancetre(X,Z). apparente(X,Y ) : ? ancetre(Z,X),ancetre(Z,Y ).

Programmation Logique

Prolog : exemples de programmes (II)

Que donnent les questions suivantes :

–    ?apparente(anne,noel).

–    ?apparente(anne,X).

Calculez l’arbre de dérivation.

Programmation Logique

Prolog : exemples de programmes (III)

Que se passe-t-il si on rend le programme plus “déclaratif”? Par exemple si on prend le programme suivant?

parent(luc,anne). parent(marie,anne). parent(henry,marie). parent(henry,thierry). parent(thierry,noel). parent(julie,helene).

ancetre(X,X).

ancetre(X,Y ) : ? parent(X,Y ). ancetre(X,Y ) : ? ancetre(X,Z),ancetre(Z,Y ). apparente(X,Y ) : ? ancetre(Z,X),ancetre(Z,Y ).

Que se passe-t-il si on pose les mêmes questions sur ce nouveau programme?

Programmation Logique

Prolog : exemples de programmes (IV)

Dans la deuxième formulation, on a exprimé plus “déclarativement” que la relation ancêtre est transitive.

Même si la sémantique “déclarative” est identique (c’est-a`-dire que l’ensemble des valuations qui rendent la formule vraie sont les mêmes), la sémantique opérationnelle est différente.

Quand on écrit un programme Prolog, on est malheureusement obligé de tenir compte de la fac¸on dont le programme va être exécuté.

Programmation Logique

Prolog : exemples de programmes (V)

Quelques règles générales quand on écrit un programme Prolog :

–    quand on utilise des définitions récursives (cfr ancetre), le cas de base doit précéder le cas inductif.

–    les faits connus pour un prédicat précèdent généralement les règles définies sur ce prédicat.

Attention ce ne sont que des heuristiques

Programmation Logique

Prolog : exemples de programmes (V)

Une structure de donnée de Prolog : la liste.

–    cas de base : [] empty list.

–    constructeur : .(b,T), on construit une nouvelle liste par concaténation de la constante b à la liste T.

Les programmes qui manipulent les listes seront naturellement récursifs.

Programmation Logique

Prolog : exemples de programmes (V)

Exemples de listes :

–    .(b,[]) liste d’un seul élément b

–    [a,b,c,d], abbréviation pour .(a,.(b,.(c,.(d,[]))))

–    on peut également écrire [a| [b,c,d]]

–    [b | X] définit l’ensemble des listes qui commencent avec l’élément b

–    [a,[a,b],b], une liste avec trois éléments dont le deuxième est lui-même une liste.

Programmation Logique

Prolog : exemples de programmes (V)

Exemple de programme qui manipule des listes : le programme append.

Le but du programme est de calculer la concaténation de deux listes. Voici le programme :

append([],X,X). append([X | Y ],Z,[X | W]) : ? append(Y,Z,W).

Le prédicat append est défini par induction. Le cas de base dit que la concaténation de la liste vide avec une liste X est cette même liste X. Le cas inductif exprime que si la concaténation de Y et Z est W, alors la concaténation de la liste Y augmentée de l’élément X avec la liste Z est la liste W augmentée de l’élément X.

Programmation Logique

Prolog : exemples de programmes (V)

Comment la recherche Prolog répond-t-elle aux questions suivantes :

–    ?append([a],[b],[a,b]).

–    ?append([a,b],[c],[a,b,c]).

–    ?append([a,b],[c],[a,b,b,c]).

–    ?append([a],X,[Y | Z]). – ?append(X,Y,[a,b,c]).

Programmation Logique

Prolog : exemples de programmes (V)

Dans un langage de programmation impératif comme Pascal, les arguments d’une procédure peuvent toujours être classifiés comme input ou ouput. Ce n’est pas le cas en Prolog. Il y a dans un programme Prolog une symétrie inhabituelle entre input et output.

Considérons à nouveau le programme “append”. append([],X,X). append([X | Y ],Z,[X | W]) : ? append(Y,Z,W).

Le prédicat append(X,Y,Z) exprime que la concaténation des listes X et Y est égale à la liste Z.

Programmation Logique

Prolog : exemples de programmes (V)

Si on pose la question ?append([a,b],[c,d],Z)., les deux premiers arguments sont des inputs à la procédure, qui calcule la concaténation des listes [a,b] et [c,d].

Par contre, si on pose la question ?append(X,Y,[a,b,c,d]), le dernier argument devient input et les deux premiers outputs. Quand on pose cette question, la procédure calcule quelles sont les listes qui, quand elles sont concaténées, donnent la liste [a,b,c,d].

Cette caractéristique de Prolog est appelée la multi-directionnalité. Cette multi-directionnalité donne une grande souplesse et expressivité au langage. Cela a parfois un prix au niveau de l’efficacité.

Programmation Logique

Prolog : exemples de programmes (V)

Un autre programme qui manipule des listes : member.

member(X,[X | Y ]).

member(X,[Y | T]) : ? member(X,T).

A nouveau la définition est récursive. Calculez les réponses aux questions suivantes :

–    ?member(a,[a,b]).

–    ?member(X,[a,b,c]).

–    ?member(a,[X | Y ]).

–    ?member(X,Y ).

A nouveau, ces questions illustrent la puissance de la multi-directionnalité de Prolog.

Programmation Logique

Prolog : exemples de programmes (V)

Parcours d’un graphe :

a(namur,bruxelles). a(bruxelles,ostende). a(ostende,courtrai). a(courtrai,mons). a(mons,charleroi). a(charleroi,namur). a(mons,nivelles). a(nivelles,bruxelles). a(X,Y ) : ? a(Y,X).

go(From,To) : ? a(From,To). go(From,To) : ? a(From,In),go(In,To).

Programmation Logique

Prolog : exemples de programmes (V)

Comment retenir par ou` l’itinéraire passe? On mémorise le chemin dans une liste. a(namur,bruxelles).

a(nivelles,bruxelles). go(From,To,[]) : ? a(From,To).

go(From,To,[In| T]) : ? a(From,In),go(In,To,T).

On peut poser les questions suivantes :

–    ?go(namur,ostende,T).

–    ?go(namur,X,[bruxelles]).

Programmation Logique

Prolog : exemples de programmes (V)

La résolution n’est pas efficace lorsqu’il s’agit d’évaluer des opérations arithmétiques. On peut coder les entiers, les opérations (comme l’addition) et certaines de leur propriétés. Et ce, en utilisant des clauses comme :

add(s(X),Y,s(Z)) : ? add(X,Y,Z).

Pour évaluer directement des expressions arithmétiques, Prolog offre un prédicat infixe is :

Result is Expression

Programmation Logique

Prolog : exemples de programmes (V)

Par exemple la clause suivante retrouve le prix catalogue d’un article à partir d’une base de faits ainsi qu’un pourcentage de remise et établit le prix de vente :

sellingprice         (Item,Price) : ?

listeprice(Item,List), discountpercent(Item,Discount),

Price is List ? List ? Discount/100

Attention, les prédicats arithmétiques diffèrent des autres prédicats. Un prédicat arithmétique est unidirectionnel! Par exemple, si “10 is X + Y ”était un prédicat logique, alors X et Y pourraient être unifiées a` 1 et 9 par exemple, ou encore a` 2 et 8, via un backtracking. Néanmoins, ceci est illégal. Dans le prédicat Result is Expression, les variables de “Expression” doivent être instanciées a` des valeurs numériques lorsque le prédicat est évalué.

Programmation Logique

Prolog : exemples de programmes (V)

Pour terminer, nous abordons un moyen (pas très élégant mais souvent efficace) pour contrôler l’exécution d’un programme logique, via le prédicat“!” appelé“cut ”.

Syntaxiquement“!” peut apparaˆ?tre comme n’importe quel autre prédicat.

p : ? q1,q2,!,q3,q4

Cut n’a aucune sémantique (déclarative), mais il altère la recheche SLD de la fac¸on suivante : quand la clause ci-dessus est appelée dans une recherche, le sous-but q1,q2,!,q3,q4 est inséré au début du but courant. La recherche tente de satisfaire q1, puis q2 comme d’habitude. Si ca réussit, on passe outre le cut et on continue avec q3 et q4. Si on réussit, on continue en ignorant le cut. Sinon, si q3 puis q4 échouent, on doit backtracker. Et en remontant sur le “cut”, on fait comme si p avait échoué (donc on ne remonte pas sur q2). La recherche repart alors du but parent qui a appelé p et on cherche la branche suivante à droite de ce noeud.

Programmation Logique

Prolog : exemples de programmes (V)

Illustration : considérons le programme Prolog suivant. t : ? p,r. t : ? s. p : ? q1,q2,!,q3,q4. q1. q2. s.

u.

Et le but ¬ t. Calculons l’arbre de dérivation.

Programmation Logique

Prolog : exemples de programmes (V)

Une application du cut : le calcul de la factorielle. factorial(0,1).

factorial(N,F) : ?                  N1 is N ? 1,

factorial(N1,F1),

F is N ? F1.

Maintenant faisons l’hypothèse que l’on appelle factorielle dans d’une autre procedure.

check(N) : ? factorial(N,F),property(F).

Si check est appelé avec la valeur N = 0, il y a un appel de factorial(0,F) qui va renvoyer F = 1 et appeler property(1). Supposons que cet appel échoue. Alors il y a backtracking, et on

“défait” la substitution F = 1. On essaye à nouveau un appel à factorielle. On n’utilise plus le cas de base mais le cas inductif avec F = 0. Cela à pour effet de générer l’appel : factorial(0,F) : ? N1 is 0 ? 1,

factorial( ? 1,F1),

F is 0 ? F1.

et cela entraine un boucle infinie. Pour éviter cela, on peut utiliser le cut de la fac¸on suivante : factorial(0,1) : ? !.

factorial(N,F) : ?                  N1 is N ? 1,

factorial(N1,F1),

F is N ? F1.

Le cut évite ainsi de backtracker sur la procédure factorial lorsque celle-ci a été appelée avec 0.

Logique du premier ordre déduction naturelle (I)

Pour raisonner dans le logique du premier ordre, on utilise les règles de déduction naturelle de la logique propositionnelle et on y ajoute des règles pour (i) l’égalité, (ii) la quantification existentielle, et (iii) la quantification universelle. Règles de preuves pour l’égalité

t=t =i

t1=t2 ?[t1/x] ?[t2/x] =e


Logique du premier ordre déduction naturelle

Exemples

t1 = t2 ? t2 = t1

1

t1 = t2        prémisse

2

t1 = t1              =i, rem : ? ? x = t1

3

t2 = t1            =e,1,2

Logique du premier ordre déduction naturelle

Exemples

t1 = t2,t2 = t3 ? t1 = t3

                                                        1      t2 = t3

prémisse

                                                        2      t1 = t2

prémisse , rem : ? ? t1 = x

                                                        3      t1 = t3

=e,1,2

Logique du premier ordre déduction naturelle (I) Règles de preuves pour la quantification universelle

avec t libre pour x

                                                                                                                          ?x?                                     ? i

x0 doit être une variable fraˆ?che, c’est-à-dire que x0 n’apparaˆ?t nulle part en dehors de la boˆ?te. En effet, on ne peut faire aucune hypothèse sur x0 (on veut faire une preuve quel que soit x0).

Logique du premier ordre déduction naturelle Exemples

? x · (p(x) ? q(x)), ? x · p(x) ?   ? x · q(x)

1     ? x · (p(x) ? q(x))       prémisse

2     ? x · p(x)        prémisse

3     x0       x0 fresh

4     p(x0) ? q(x0)        ? e,1

5     p(x0)       ? e,2

6     q(x0)       ?e,4,5

7     end hypothesis on x0

8     ? x · q(x)        ? xi

Logique du premier ordre déduction naturelle (I)

x0?[x0/x]

?

? x · ?

                       ? xe ?

ou` x0 n’apparaˆ?t pas dans ? et n’est pas utilisé ailleurs.


Logique du premier ordre déduction naturelle

Exemples

         ? x · ? ? ? x · ?

                  1    ? x · ?

prémisse

                  2     ?[x/x]

? e,1

                  3    ? x · ?      ? xi

Logique du premier ordre déduction naturelle Exemples

? x · (p(x) ? q(x)), ? x · p(x) ?    ? x · q(x)

1    ? x · (p(x) ? q(x))       prémisse

2    ? x · p(x)        prémisse

3    x0

4    p(x0)       ? e,2

5    p(x0) ? q(x0)        ? e,1

6    q(x0)       ?e,4,5

7    ? x · q(x)        ? i,5

8    end hypothesis on x0

9    ? x · q(x)        ? xe

Logique du premier ordre

Théorème de complétude (Go¨edel)

Complétude du système de preuves de la logique du premier ordre :

? |= ? implique ? ? ?

Note : l’adéquation, i.e. ? ? ? implique ? |= ? est établie de manière classique.

Théorème de complétude

Définition d’un ensemble de formules consistantes

? est consistant s’il n’existe pas de ? tel que :

? ? ?

                                                                                                                           ? ? ¬ ?

Donc, la notion de consistance est une notion syntaxique. Voici deux exemples d’ensembles non consistants :

ex :

–    ? = {?, ¬ ? } : ? est non consistant.

–    ? = {?,? ? ?, ¬ ? } est également non consistant.

Théorème de complétude

Définition de la cohérence

Une formule ? est cohérente avec ? si

                                                                                                                ? ? {? } 6? ?

Cela revient à dire que ? ?    {? } est consistant.

Or nous voulons montrer que :

? |= ? implique ? ? ?

ce qui est équivalent, par contraposée, à :

? ? 6? ? implique ? 6|= ?

                                                                                     ? ? ?  {¬ ? } est consistant

implique

                                                                                           ? ?  {¬ ? } a un modèle.

Théorème de complétude

Pour passer de la deuxième formulation à la troisième, on utilise le fait que :

                                                                     ? 6? ? ssi ? ?  {¬ ? } est consistant

Prouvons cette équivalence :

–    ? 6? ? implique que ? ?   {¬ ? } est consistant

On prouve la contraposée. Si ? ? {¬ ? } est inconsistant, ? ? {¬ ? } ? ? , et donc ? ? {¬ ? } ? ?, par la règle de raisonnement sous hypothèses, on obtient ? ? ¬ ? ? ?, ce qui est

équivalent à ? ? ¬ ¬ ? ? ?, par raisonnement propositionnel, cela donne ? ? ?.

–    ? ?    {¬ ? } est consistant implique que ? 6? ?

On établit la contraposée. Si ? ? ?, alors ? ? {¬ ? } ? ? ? ¬ ?, donc ? ? {¬ ? } est inconsistant.

Théorème de complétude

Prouver la complétude revient donc à montrer que tout ensemble consistant de formules ? possède un modèle.

La solution est simple et ingénieuse : le modèle va être un modèle syntaxique (rappelez-vous les modèles de Herbrand).

Le domaine d’interprétation sera le domaine des termes sur L et l’interprétation des fonctions et prédicats sera définie au regard de ?.

Il y a deux difficultés majeures :

1.    Le domaine des termes peut ne pas être assez riche pourconstruire un modèle. Par exemple :

                                                    ? = {? x · p(x) }   ?   {¬ p(t) : t est un terme de L }

Bien que ? soit satisfaisable, on ne peut pas construire un modèle pour ? à partir des termes.

2.    De plus, ? peut ne pas nous donner assez d’information pournous guider dans la construction du modèle. Par exemple, pour un terme t et un prédicat p, ? peut ne pas contenir de manière explicite l’information pour décider si p(t) doit être vrai ou faux.

Théorème de complétude

Solutions à ces deux problèmes (Léon Henkin).

Pour 1.

On va ajouter au langage L un nombre infini dénombrable de constantes

                                                                               L ? = L    ?          {c1,c2, ,cn, }.

Maintenant, il faut montrer que cette modification n’altère pas la consistance de ?. En effet, on a ajouté des constantes à L . Donc il y a des nouvelles formules que l’on peut déduire de ?. Peut-être peut-on déduire ? de ??

On va voir que c’est faux, ? est toujours consistant.

Théorème de complétude

Lemme : Si ? est consistant en considérant L alors ? le reste pour L ? = L       ?     {c1,c2, ,cn, }.

Proof. Si ? n’est pas consistant pour L ? alors on a une preuve

S = (?1, ,?n)                  ?n ? ? ?  ¬ ?

On peut faire l’hypothèse qu’il y a un nombre infini dénombrable de variables qu’on n’utilise pas dans la preuve (en effet la preuve est finie).

Dans la preuve S qui aboutit à une contradiction, on a utilisé des constantes de {c0,c1, ,cn, } (sinon on aurait déjà pu faire la preuve avec L et ? serait non consistant pour L ).

Comme ces nouvelles constantes n’apparaissent pas dans ?, on peut donc refaire la preuve S avec des variables qui n’apparaissent pas dans ? on a suffisamment de variables (en effet dans L , et comme dans tout langage du premier ordre, on a une infinité dénombrable de variables et vu que les nouvelles constantes n’apparaissent pas dans ? on peut remplacer ces constantes par des variables) donc S? est une nouvelle preuve de la contradiction. Mais c’est également une preuve qu’on pouvait faire avec L . Donc ? est inconsistant pour L . Ce qui est absurde.

Théorème de complétude

Solution pour le problème 2

Pour résoudre le problème du manque d’information, nous allons ajouter des formules à ? pour qu’il contienne l’information nécessaire.

On va énumérer les formules ?1,?2, ,?n, du langage L ? et construire des ensembles successifs ?0,?1, ,?n, .

Pour construire les ?i, on procède par induction :

Cas de base : ?0 = ?

Cas d’induction : Supposons que ?1, ,?i?1 soient construits.

1.    si ?i?1 ? {?i } est consistant et ?i n’est pas de la forme ? x · ? alors ?i = ?i?1 ? {?i }.

2.    si ?i?1 ? {?i } est consistant et ?i est de la forme ? x · ? alors ?i = ?i?1 ?   {? x · ?,?[c/x] }, avec c qui n’apparaˆ?t pas dans

?0, ,?i?1

Intuitivement, c est un témoin pour x qui montre que ? x · ? est vrai.

3.    si ?i?1 ? {?i } est inconsistante et ?i n’est pas de la forme ? x · ? alors ?i = ?i?1 ? {¬ ?i }.

4.    ?i?1 ?     {?i } est inconsistant et ?i est de la forme ? x · ? alors ?i = ?i?1 ?   {¬ ?i, ¬ ?[c/x] } avec c une constante qui n’apparaˆ?t pas dans ?0,?1, ,?i?1.

Théorème de complétude

On va maintenant montrer que les ensembles de formules ?i que l’on vient de construire sont tous consistants.

Lemme. ? i ? 0 : ?i est consistant.

Preuve. A nouveau, la preuve est par induction.

C.B. : i = 0 on sait ?0 = ? et donc ?0 est consistant.

C.I. : Supposons que ?i?1 est consistant et montrons que ?i l’est

également.

1.    Si ?i est obtenu par le cas 1. Alors trivialement ?i est consistant.

2.    Même preuve que pour le cas 4 ci-dessous..

3.    Si ?i est obtenu par le cas 3 alors on sait que ?i?1 ? {?i } est inconsistant (?i?1 ? {?i } ? ? ) .

Par la règle ¬ i on sait donc que ?i?1 ?      ¬ ?i. Par l’adéquation du système de preuve, on sait que ?i?1 ?        {¬ ?i } = ?i est consistant.

4.    Considérons le cas 4, par définition on a que?i = ?i?1 ? {¬ ? x · ? } ? {¬ ?[c/x] } .

Faisons l’hypothèse (raisonnement par l’absurde) que ?i est inconsistant. On sait également que ?i?1 ?   {¬    ? x · ? } est consistant car on sait que ?i?1 ?        {? x · ? }        ?     ? et donc la règle ¬ i nous permet de d’affirmer ?i?1 ?     ¬      ? x · ?.

L’ inconsistance ne peut donc venir que de l’ajout de ¬ ?[c/x]!

Donc faisons l’hypothèse que ?i?1 ? {¬ ?[c/x] } est inconsistant. A nouveau par ¬ i, nous obtenons :

?i?1 ? ?[c/x]

Donc on a une preuve de ? ou` on a remplacé x par c, car lors de la construction de ?i on a utilisé un c qui n’apparaissait pas dans ?0, ,?i?1.

On peut donc remplacer la constante c dans cette preuve par une nouvelle variable y.

?i?1 ? ?[y/x]

ou` y est une nouvelle variable En utilisant, ? xi On obtient :

                                                                                                                        ?i?1 ?   ? y · ?

y étant quantifiée, elle peut être renommée, ce qui donne :

                                                                                                                        ?i?1 ?   ? x · ?

Or, on avait montré précédemment que :

                                                                                                                     ?i?1 ?   ¬ ? x · ?

On obtient donc une contradiction. Et donc l’hypothèse ?i non consistant est fausse. C.Q.F.D.

Théorème de complétude

Nous sommes maitenant en mesure de définir l’ensemble de formules ??.

?? = Si?0 ?i

Quelles sont les propriétés de ?? ?

1.    Pour toute formule ? sur L ? on a

–    soit ? ? ??

–    soit ¬ ? ? ??

On dit que ?? est complet. En effet, par construction, pour chaque formule ?i de l’énumération, on a toujours ajouté soit ?i, soit ¬ ?i.

2.    Pour toute formule de la forme ? x · ? ? ??, on a une formule ?[c/x] ? ?? : on dit que ?? est clos.

3.    De plus, ?? est consistant. En effet, faisons l’hypothèse que ?? est non consistant.

                                                                                                                                     ?? ?   ?

Il existe donc une preuve S = (?1, ,?n) telle que ?n ?        ?     ? ? ?    ¬ ?. La preuve a une longueur finie : on sait donc que pour chaque ?i il existe un j tel que ?i ? ?j, ce qui voudrait dire que ?j ?        ? , ce qui est absurde puisque nous avons montré que la séquence des ?i est consistante.

Théorème de complétude

Nous sommes maintenant en position pour définir le modèle ?. Définissons tout d’abord le domaine d’interprétation M?.

M? va être défini à partir des termes de L ?. On a besoin d’une relation d’équivalence sur les termes de L ? :

t ? t? ssi t = t? ? ??

? est bien une relation d’équivalence.

En effet, nous avons déjà montré que les propriétés de l’égalité peuvent être établies dans le système de preuves : – réflexive (? t1 = t1)

–    transitive (t1 = t2 ? t2 = t3 ? t1 = t3)

–    symétrique (t1 = t2 ? t2 = t1)

On prend un représentant par classe d’ équivalence :

t ? [t]

[t] est le représentant de sa classe d’équivalence.

Le domaine d’interprétation est constitué des seuls représentants des classes d’équivalence :

M? = Term( L ?) mod ?

Théorème de complétude

Nous allons maintenant fournir l’interprétation µ? des fonctions et prédicats.

1.    Si f est une fonction d’arité k

fµ?([t1], ,[tk]) = [f(t1, ,tk)]

2.    Si R est un prédicat d’arité k alors

Rµ?([t1], ,[tk]) ssi R(t1, ,tk) ? ??

On a choisi de ne garder dans le domaine de M? qu’un seul représentant par classe d’ équivalence. On va montrer que la définition de fµ? et Rµ? est indépendante du choix d’un représentant particulier :

Formellement, cela revient à montrer que :

t1 ? t?1

... alors si

tk ? t?kf(t1, ,tk) ? f(t?1, ,t?k)

En effet, on sait par définition que

 ssi

On veut montrer que

On peut obtenir cette preuve de la fac¸on suivante :

                                                            =i           ??                       ? f(t1, ,tk) = f(t1, ,tk)

                                                           =e           ??                     ? f(t1, ,tk) = f(t?1, ,t?k)

et

Ici on a traité le cas de base. Pour les termes de hauteur > 1, on utilise un raisonnement par induction et le même schéma de preuve.

On peut faire le même raisonnement pour les prédicats.

On a donc : si  alors

R(t1, ,tk) ? ?? ssi

Théorème de complétude

Nous avons défini l’interprétation µ??. On va maintenant prouver que :

µ? |= ??

On va montrer que l’interprétation µ? est un modèle pour toute formule ? ? ??, i.e.

µ? |= ?.

On va raisonner par induction sur la structure de ? pour montrer que µ? |= ?.

C.B. : ? ? R(t1, ,tn)

Par définition de Rµ? on a que

([t1], ,[tn]) ? Rµ? ssi R(t1, ,tn) ? ??.

On a donc µ? |= R(t1, ,tn). C.I :

–    ? ?    ¬ ?, par hypothèse d’induction on a que ? 6? ?? ssi µ? |6 = ?, or on sait que ¬ ? ? ?? et donc ? 6? ?? par construction de ?? et donc µ?? 6|= ?. On a donc établi :

µ? |= ¬ ?

–    ? ? ?1 ? ?2 par hypothèse d’induction on a :

?1 ? ?? ssi µ? |= ?1

?2 ? ?? ssi µ? |= ?2

Or par définition de la sémantique de l’opérateur ? , on a

également :

µ? |= ? ssi   µ? |= ?1 ou    µ? |= ?2

Vu que ?1 ? ?2 ? ? et que l’on peut montrer que

?1 ? ?2, ¬ ?1 ? ?2et   ?1 ? ?2, ¬ ?2 ? ?1

On a donc soit ?1 ? ?? ou ?2 ? ??. (on se sert donc des règles syntaxiques pour établir cela). Et donc, on a :

µ? |= ?1

, ou

µ? |= ?2

et donc, par sémantique de ? ,

µ? |= ?1 ? ?2

? = ? x · ?

Montrons que ? ? ?? ssi ?[t/x] ? ?? pour tout terme t. Par hypothèse d’induction on a :

?[t/x] ? ??

ssi

µ? |= ?[t/x]

Donc si on prouve ce résultat, alors on obtient bien ? x · ? ? ?? ssi µ? |= ? x? (sémantique du ? ). En effet, le domaine M? ne contient que les termes du langage L ? (plus exactement, les classes d’équivalence de cet ensemble de termes).

1.    supposons que ? x · ? ? ?? alors en utilisant la règle de preuve (syntaxique) ? e :

? x · ?

?[t/x]

?? ? ?[t/x] et ?? est consistant

Donc ¬ ?[t/x] ?6    ??. Par complétude de ??, ?[t/x] ? ?? pour tout terme t. Par hypothèse d’induction :

?? |= ?[t/x] pour tout terme t

et donc par sémantique du ? :

µ? |= ? x · ?

2.    supposons ? x · ? ?6 ?? par complétude on sait que

                                                                                                                          ¬ ? x · ? ? ??

par construction de ?? on a ¬ ?[c/x] ? ?? (témoin) et donc ?[c/x] 6? ??. Par hypothèse d’induction on a

µ? 6|= ?[c/x]

et donc par la sémantique du ? on a

µ? 6|= ? x · ?

et donc µ? |= ¬ ? x · ?

Théorème de complétude

Donc, pour toute formule ? ? ??, on a montré que

µ? |= ?

et donc, vu que ? ? ??, on a que pour toute formule ? ? ?

µ? |= ?

et ? a donc un modèle! C.Q.F.D.

Théorème d’incomplétude (Go¨edel)

En général lorsque l’on fait des preuves en mathématique, on fait des raisonnements informels.

Hilbert : Peut-on formaliser les mathématiques, c’est-à-dire prouver formellement tous les théorèmes des mathématiques?

Go¨edel va établir que c’est impossible!

Théorème d’incomplétude (Go¨edel)

Soit µ un modèle mathématique (les graphes, l’arithmétique, ) au sujet duquel on veut faire des raisonnements, par exemple démontrer un théorème formalisé par une formule ?. On veut donc

établir :

µ |= ?

Remarque : vu que l’on fixe l’interprétation µ, chaque formule ? est soit vraie soit fausse.

Théorème d’incomplétude (Go¨edel)

Pour faire des raisonnements formels sur µ, on utilise la méthode axiomatique . On parlera d’axiomatisation d’une théorie mathématique.

µ est complètement axiomatisé (“décrit”) par ? (un ensemble de formules) si :

1.    pour tout ? ? ?, on a µ |= ? ;

2.    si µ |= ? alors |= ? ? ?, et donc (par le théorème de complétude, si ? et ? sont des formules du premier ordre) ? ? ? ?, ce qui est équivalent à ? ? ?.

Théorème d’incomplétude (Go¨edel)

Est-ce que la méthode axiomatique est complète? C’est-a`-dire applicable à tout modèle mathématique µ?

Malheureusement, la réponse est négative. C’est ce que nous apprend le théorème d’incomplétude de Go¨edel.

Plus précisement, Go¨edel montre qu’il ne peut pas exister d’axiomatisation complète (dans le sens précis que l’on vient de définir) de l’arithmétique (théorie mathématique somme toute assez simple).

Théorème d’incomplétude (Go¨edel)

Pour formaliser l’arithmétique, nous utilisons le language

L N = (0N,s,+N, × N,<N)

Voici quelques exemples de formules dans ce langage :

–    ? x ·   ? y ·        ¬ (x > y)

–    ? x,y ·        ? d,x·

x × d + r = y ? r < d ? x × (d + 1) > y

Théorème d’incomplétude (Go¨edel)

On obtient l’interprétation standard, en interprétant les symboles de L N de la fac¸on suivante :

–    la constante 0N est interprétée par 0 ? N ;

–    la fonction s (pour successeur) est interprétée par la fonction

+1 ? N ? N ;

–    la fonction +N est interprétée par la fonction d’addition sur les nombres naturels;

–    la fonction × N est interprétée par la fonction de multiplication sur les nombres naturels;

–    la relation <N est interprétée par l’ordre “plus petit que” sur les nombres naturels.

Notons que, puisque nous avons fixé le modèle d’interprétation µ, on aura donc µ |= ? ou µ |= ¬ ? pour toute formule close ?.

Théorème d’incomplétude (Go¨edel)

Des ensembles d’axiomes ont été proposés pour formaliser l’arithmétique. Il y a par exemple les axiomes de l’arithmétique de Peano :

–    ?x · (s(x) 6= 0N)

–    ?x · ?y · (s(x) = s(y) ? x = y)

–    ?x · (x = 0 ? ?y · x = s(y))

–   

Plus un schéma d’axiomes pour l’induction :

(?[0/x]

??x · ?(x) ? ?[s(x)/x])

? ?y · ?[y/x]

Ces axiomes et ce schéma d’axiomes nous permettent de déduire certains théorèmes de l’arithmétique, mais pas tous.

Théorème d’incomplétude (Go¨edel)

Enoncé du théorème de Go¨edel :

Tout ensemble fini ou énumérable d’axiomes ? pour l’arithmétique est tel que :

Si ? est consistant

Alors ? est incomplet.

Théorème d’incomplétude (Go¨edel)

Comment Go¨edel établit-il ce résultat?

La preuve de ce théorème est très ardue mais l’idée principale est simple et élégante. C’est une application ingénieuse du procédé de la diagonale de Kantor.

L’idée principale est de créer une correspondance, appelée numéro de Go¨edel, entre les nombres naturels et les objets logiques comme les formules et les preuves. A chaque formule et à chaque preuve (séquence finie de formules) est attribué un numéro, le numéro de Go¨edel.

Cette numérotation peut à son tour être définie par des formules du langage L N quand celui-ci est interprété dans le modèle standard. Ces formules, avec les axiomes de Peano, sont suffissantes pour définir cette numérotation.

Théorème d’incomplétude (Go¨edel)

En particulier, on peut montrer qu’il existe une formule

?(i,j)

dont l’interprétation est la suivante.

Pour tout i,j, on a que :

?(i,j) est vrai ssi

–    i est le numéro de Go¨edel d’une formule ?(x) avec une variable libre x;

–    j est le numéro de Go¨edel de la preuve de ?[i/x].

Théorème d’incomplétude (Go¨edel)

Lemme de complétude partielle pour les formules sans variable :

Lemme : si ? est une formule valide de l’arithmétique sans variable, alors ? peut-être dérivée grâce aux axiomes de Peano.

En particulier, si ?(n,m) est vraie, alors

?Peano ?(n,m).

Théorème d’incomplétude (Go¨edel)

Considérons maintenant la formule ? suivante :

? ? ? y ·  ¬ ?(x,y)

Cette formule a une variable libre x et nous noterons son numéro de Go¨edel m.

Maintenant, considérons la formule ? définie comme suit :

? ? ?[m/x] ?  ? y · ¬ (?(m,y))

? exprime donc “Il n’y a pas de preuve de ?”.

Théorème d’incomplétude (Go¨edel) On établit maitenant le théorème suivant :

Théroème : Si ? est consistant, alors :

? 6? ?et

                                                                                                                        ? 6? ¬ ?

(et donc ? est incomplet).

La preuve est établie par contradiction.

Supposons que ? ? ? . Notons par n le numéro de Go¨edel de cette preuve. Par définition on a que ?(m,n) est vraie. Vu que ?(m,n) est sans variable, par le théorème de complétude partielle on a :

? ? ?(m,n)

or ? ? ? y · ¬ ?(m,y); en utilisant la règle ? e, et l’hypothèse ? ? ?, je peux déduire :

                                                                                                           ?,? ?   ¬ ?(m,n)

et donc

                                                                                                              ? ?  ¬ ?(m,n)

Ce qui contredit la consistance de ?.

Théorème d’incomplétude (Go¨edel)

Supposons maintenant que ? ?       ¬ ? . On a donc

? |= ? y · ?(m,y)

Notons n le nombre qui rend ?(m,y) vrai. Donc ?(m,n) est vrai. Cette formule signifie que la formule ? a une preuve de numéro n et donc ? ? ?. Ce qui contredit l’hypothèse de consistance de ? si l’on suppose ? ? ¬ ?.

[

Index

]

?-règles, 50 ?-règles, 51

égalitaire, 139

Algorithme d’unification, 213 arbres sémantiques, 237 arité, 139 axiomatisation, 337

backtracking, 260

base de Herbrand, 230

but, 249

capture de variables, 168 clôture universelle, 161 clause, 110 clause dans le premier ordre, 180 clause de Horn, 248

clause négative, 113

clause positive, 113

clause tautologique, 113

clause vide, 113, 223

clauses définies, 247

clauses séparées, 220 conclusion, 71 connecteurs logiques, 21 conséquence logique, 40, 71 constantes de Skolem, 188

contradictions, 91

couples de termes irréductibles, 212

couples de termes réductibles, 212 coupure, 117

cut, 292

déduction naturelle, 70 déduction naturelle dans le premier ordre, 297

domaine de Herbrand, 230 domaine, domaine d’interprétation, 149

ensembles de clauses, 115 equivalentes, 40 extension de Skolem, 182

fonction d’interprétation, 32 forme clausale, 192

forme de Skolem, 188 forme normale conjonctive, 101 forme normale conjonctive dans le premier ordre, 180

forme normale disjonctive, 101

forme normale disjonctive dans le premier ordre, 180

formes de Skolem, 175

formule close, 148, 233

formule universelle, 182

formule universelle close, 234

formules équivalentes dans le premier ordre, 161 formules atomiques, 143 formules cohérentes, 307 formules complémentaires, 42 formules consistantes, 306

formules de la logique propositionnelle, 22

formules du langage L , 144

Formules prénexes, 175

formules valides dans le premier ordre, 160

Goedel, théorème d’incomplétude, 335

hauteur d’un couple de termes, 208 hauteur d’un ensemble fini S de couples, 208

hauteur d’un terme, 205

induction mathématique, 29

langage L , 139

littéral, 42, 110 littéral dans le premier ordre, 180

littéraux complémentaires, 45

méthode axiomatique, 337

modèle de Herbrand, 233 Modus Ponens, 75 Modus Tollens, 77

notation infixe, 24

occurrence d’une variable, 147 occurrence libre, 148

pas de Skolémisation, 183

prédicats, 139 prémisses, 71 preuve par résolution, 223

profondeur d’une formule, 28 Prolog, 256

propositions, 21

propriété de Hintikka, 64

quantificateur existentiel ? , 138

quantificateurs universel ? , 138

réfutation, 122, 223

résolution dans le premier ordre, 191

résolution linéaire, 247

résolution, règle, 219 résolvant, 220

règle de résolution, 219

Sélection Linéaire Définie, 247

séquent, 71

satisfaction dans le premier ordre, 161

satisfaisable, 38 Skolémisation, 187

sous-formule, 146 structure d’interprétation, 149 structure de Herbrand, 233

substitution, 167, 198 symboles de constantes, 139 symboles de fonctions, 139 symboles de relations, 139 système simplifié, 209

systèmes (unification), 208

tableau complet, 54 tableau fermé, 54 tableau ouvert, 54

tableau sémantique, 52 tables de vérité, 36 termes d’un langage L , 141 Théorème d’incomplétude de Goedel, 335

unificateur, 203 unificateur principal, 203

unification, 191

valeur de vérité, 33 valide, 38 validité dans le premier ordre, 161

valuation, 32

valuation dans le premier ordre, 152

variable libre, 148 vocabulaire du langage de la logique propositionnelle, 21



296