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

LOGIQUE DES PRÉDICATS


Logique des prédicats : langage

Introduction

Définition (alphabet). L'alphabet de la logique des prédicats est constitué de

Notation. Q dénote un quantificateur quelconque, c-à-d /\ ou \/.
Les fonctions à 0 arguments sont appellées constantes (souvent notées a, b, ..., Socrate, ...). Les prédicats à 0 arguments ne sont rien d'autre que des variables propositionnelles.

Définition (terme). L'ensemble des termes est le plus petit ensemble de mots construits sur l'alphabet de la logique des prédicats tel que

Définition (formule). Si p est un prédicat à n arguments et t1,...,tn sont des termes alors p(t1,...,tn) est une formule atomique.
L'ensemble FOR des formules (ou formules bien formées) de la logique des prédicats est alors défini de la même manière qu'en logique propositionnelle, en rajoutant une clause pour les quantificateurs :

Une expression est un terme ou une formule.
(Annexe : une définition plus explicite des formules)

Exemples de traduction d'énoncés en formules

Remarque sur les jeux de connecteurs primitifs

On reprend de la logique propositionnelle les notations pour les formules, la notion de sous-formule (en tenant compte des quantificateurs dans la définition) et les conventions pour économiser les parenthèses.


suite : variables libres, substitution de variables















                                                      


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

Logique des prédicats : langage (suite)

Définition (portée d'un quantificateur, variable libre). Dans les formules (/\ x A) et (\/ x A) , la formule A est appellé la portée du quantificateur.
Une occurrence d'une variable est libre si elle n'est dans la portée d'aucun quantificateur. Sinon elle est liée.

Exemples

Définition (formule fermée, formule ouverte). Une formule est fermée (ou close) si elle ne contient pas de variables libres. Sinon elle est ouverte.
Exemples

Définition (substitution de variables). Une substitution de variables est une application des variables dans les termes qui est l'identité presque partout.
L'application d'une substitution à une expression E est le résultat du remplacement simultanée de toutes les occurrences libres des variables dans E par leur terme associé.
Si E est une expression alors (E)s est appelé une instance de E.
La composition de substitutions est la composition de fonctions.

Notation. Soit {x1 , ... , xn} l'ensemble des variables tel que s(x) est différent de x . La substitution s est alors notée s = {x1\t1 , ... , xn\tn}.
Exemples de substitutions


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
































                                                      


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

Logique des prédicats : théorie des modèles

Introduction

Définition (interprétation). Une interprétation I est constituée de

Par abus de notation, les fonctions d'interprétation IV , IF , IP sont souvent notées I.

Définition (interprétation des termes et formules). Une interprétation donnée I peut être étendue aux termes par


Une interprétation I' est une variante en x de I si I' est identique à I sauf en x (la seule différence entre I et I' est la valeur qu'elles donnent à x).
N.B. : I et I' peuvent être identiques : I est une variante de I en x .

Une interprétation donnée I peut être étendue aux formules par :

Exemples

Comme en logique propositionnelle, I(A) = 1 est parfois noté |=I A , et nous dirons alors que I est un modèle de A.

Validité et satisfiabilité sont alors défini comme en logique propositionnelle, ainsi que la conséquence logique (Exemples).


suite : section sur la théorie de la preuve

















                                                      


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

Logique des prédicats : théorie de la preuve

Introduction

Définition (axiomatique à la Hilbert). Les schémas d'axiome de la logique des prédicats sont ceux de la logique propositionnelle, plus

/\ x A -> ((A){x\t})

(A){x\t} -> \/ x A


(où {x\t} est une substitution quelconque), et les règles d'inférence sont le Modus Ponens :

A    A -> B
_____________
B


plus les deux règles pour les quantificateurs

A -> B
______________
A -> (/\ x B)
s'il n'y a pas d'occurrence libre de x dans A

et

A -> B
______________
(\/ x A) -> B
s'il n'y a pas d'occurrence libre de x dans B

Même définition de preuve, de prouvabilité et de consistance qu'en logique propositionnelle (Exemples)

Remarque. Il est possible de définir également la déduction. Nous l'omettons ici, car elle est plus complexe que celle de la logique propositionnelle (les deux règles d'inférence pour les quantificateurs peuvent seulement être appliquées à des axiomes logiques, et non à des axiomes non-logiques et des formules déduites à partir de ceux-ci). De plus, cette notion peut être réduite à la validité, par un théorème de la déduction similaire à celui de la logique propositionnelle.


suite : section sur les propriétés importantes

















                                                      


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

Logique des prédicats : propriétés importantes

Même introduction et motivation qu'en logique propositionnelle

Adéquation et de complétude

Théorème d'adéquation. Si |- A alors |= A.
(même type de démonstration qu'en logique propositionnelle)

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

Semi-décidabilité

Théorème (semi-décidabilité). La logique des prédicats est semi-décidable : il existe une procédure effective telle que pour toute formule A en entrée,


suite : quelques équivalences utiles









































                                                      


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

Logique des prédicats : propriétés importantes (suite)

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

Équivalences propositionnelles

Ces principes peuvent être `importées' de la logique propositionnelle.

théorème de remplacement des équivalences

équivalences permettant d'éliminer les connecteurs

propriétés algébriques

Équivalences relatives aux quantificateurs

Ce sont les principes de base pour pouvoir mettre en forme normale.

Fermeture universelle :
soit A sans occurrence libre de x. Alors
|- A ssi |- /\ x A .

Fermeture existentielle :
soit A sans occurrence libre de x. Alors
A est satisfiable ssi \/ x A est satisfiable.

Quantification répetée :
|- (Q1 x Q2 x A) <-> Q2 x A

Quantification sans variable libre :
soit A sans occurrence libre de x. Alors
|- (Q x A) <-> A
|- (A){x\t} <-> A

Renommage :
|- (Q x A) <-> Q y (A){x\y}

Les deux cas où la distribution est possible :
|- (/\ x A) & (/\ x B) <-> /\ x (A & B)
|- (\/ x A) v (\/ x B) <-> \/ x (A v B)

Elargissement de la portée des quantificateurs :
soit B sans occurrence libre de x. Alors
|- (Q x A) & B <-> Q x (A & B)
|- (Q x A) v B <-> Q x (A v B)
N.B. : Ces équivalences ne sont pas prouvables si x a des occurrences libres dans B :
p.ex. (\/ x p(x)) & ~p(x) n'est pas équivalent à \/ x (p(x) & ~p(x)) .

Exemples d'application
suite : section sur les formes normales
























                                                      


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

Logique des prédicats : formes normales

Introduction et motivation

Forme normale prénexe

Définition (forme normale prénexe).
Une formule A est en forme normale prénexe si elle est de la forme Qx1 ... Qxn B , où B est une formule sans quantificateurs.
La suite des quantificateurs est appellée préfixe, et B est appellée matrice.

Exemples

Algorithme de mise en forme normale prénexe
entrée : une formule A
sortie : une formule en forme normale prénexe
début
éliminer -> , <-> , FALSE ;
appliquer autant que possible les équivalences suivantes, dans n'importe quel ordre (en remplaçant le membre gauche par le membre droit) :
tant que il existe une sous-formule Q x B telle que x apparaît en dehors de B dans A faire
remplacer Q x B par Q y (B){x\y} , où y est une nouvelle variable (n'apparaissant pas dans A) ;
fin tant que;
appliquer autant que possible les équivalences suivantes, dans n'importe quel ordre (en remplaçant le membre gauche par le membre droit) :
fin

Exemples d'application

Théorème. Pour toute entrée A, l'algorithme de mise en forme normale prénexe s'arrête. Il retourne une formule en forme normale prénexe équivalente à l'entrée.
(la démonstration utilise que les équivalences sont valides - en particulier ceux de la dernière étape reposent sur le fait que grâce au renommage de l'étape précédente toutes les occurrences de x sont dans la portée de Q x - , ainsi que le théorème de la substitution des équivalents : les remplacements effectués par l'algorithme correspondent à des équivalences prouvables).


suite : forme normale de Skolem

















                                                      


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

Logique des prédicats : formes normales (suite)

Forme normale de Skolem

Définition (forme normale de Skolem).
Une formule est en forme normale de Skolem si elle est en forme normale prénexe et ne contient pas de quantificateur existentiel.

Algorithme de mise en forme normale de Skolem
entrée : une formule A
sortie : une formule en forme normale de Skolem
début
mettre A en forme normale prénexe ;
pour tout quantificateur existentiel \/ x apparaissant dans A faire
appliquer la substitution {x\f(x1,...,xn)} à la matrice de A , où
supprimer \/ x du préfixe de A
fin pour tout
fin

Remarque. Si n = 0 on substitue par une constante.

Exemples d'application

Théorème. Pour toute formule d'entrée A, l'algorithme de mise en forme normale de Skolem s'arrête. Il retourne une formule A' en forme normale de Skolem telle que A est satisfiable ssi A' est satisfiable.
(la démonstration utilise que toutes les étapes préservent la satisfiabilité ; notons que la mise en forme normale prénexe préserve même l'équivalence logique)

Remarque. Dualement, on obtient l'équivalence de validité si on remplace les variables quantifiées universellement par une fonction des variables quantifiées existentiellement.


suite : forme normale clausale


















                                                      


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

Logique des prédicats : formes normales (suite)

Forme normale clausale

Définition (forme normale clausale).
Une formule est en forme normale clausale si elle est en forme normale de Skolem, fermée et sa matrice est en forme normale conjonctive propositionnelle.
Exemples

Notation. Comme toute variable est quantifiée universellement, nous pouvons éliminer le préfixe.
Avec les mêmes définitions de littéral et clause qu'en logique propositionnelle nous pouvons appliquer la même convention notationnelle : une formule est représentée par un ensemble d'ensembles de littéraux.

Algorithme de mise en forme normale clausale
entrée : une formule A
sortie : une formule en forme normale clausale
début
pour tout variable x apparaissant libre dans A faire
fermer A existentiellement : remplacer A par \/ x A
fin pour tout;
mettre A en forme normale de Skolem ;
mettre la matrice de A en forme normale conjonctive
fin

Exemples d'application

Théorème. Pour toute entrée A, l'algorithme de mise en forme normale clausale s'arrête. Il retourne une formule A' en forme normale clausale telle que A est satisfiable ssi A' est satisfiable.
(la démonstration est un corollaire du théorème pour la forme normale de Skolem et du théorème pour la forme normale conjonctive de la logique propositionnelle)


suite : section sur la démonstration automatique























                                                      


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

Logique des prédicats : démonstration automatique

Introduction

L'unification

Définition (unifieur). Une substitution s unifie deux termes si elle les rend identiques : s unifie t et t' si (t)s = (t')s.
Un unifieur d'un ensemble fini d'équations entre termes E = {t1=t'1 , ... , tn=t'n} est une substitution qui unifie les deux termes de chaque équation.

Exemples

Définition (unifieur le plus général).
Soient t et t' deux termes, et s un unifieur de t et t'. s est un unifieur le plus général (upg) si pour tout unifieur s' de t et t' il existe une substitution s'' telle que s' = s'' o s.
Exemples

Théorème. Si un ensemble d'équations entre termes est unifiable alors il existe un unique upg s (à un renommage de variables près).

Définition (équations résolues). Un ensemble d'équations E est résolu si

  1. toutes les parties gauches des équations sont des variables
  2. chaque variable apparaît au plus une fois dans E
Soit
E = {x1=t1 , ... , xn=tn}
un ensemble d'équations résolu. La substitution associé à E est
sE = {x1\t1 , ... , xn\tn}

Annexe : remarque sur les propriétés de sE

Algorithme d'unification
entrée : un ensemble fini E d'équations entre termes
sortie : ou bien échec, ou bien un upg de E
début
tant que E n'est pas résolu faire
choisir une équation de E ;
appliquer une des règles suivantes à cette équation :
fin tant que ;
rendre la substitution sE associé à E
fin
Exemples

Théorème. Si un ensemble de termes est unifiable alors l'algorithme calcule leur upg, sinon il s'arrête sur échec.


suite : résolvantes et réfutations

















                                                      


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

Logique des prédicats : démonstration automatique (suite)

La méthode de résolution

Définition (résolvante). Soient C et C' deux clauses telles que Alors (D U D')s est une résolvante de C et C'.
Exemples

Définition (facteur). Soit C une clause telle que

Alors (C)s est un facteur de C.
Exemples

Définition (réfutation). Une réfutation des clauses C1,...,Cm est une liste finie de clauses (D1, ... ,Dn) telle que

Exemples
Annexe : remarque sur la réfutation en tant que déduction

Théorème. Soit A une formule en forme normale clausale, et soient x1,...,xm les variables libres de A. Alors /\ x1 ... /\ xn A est insatisfiable ssi il existe une réfutation de l'ensemble de clauses associé à A.

Corollaire. Pour savoir si une formule donnée A est valide en logique des prédicats, il suffit de

  1. nier A : A' = ~A
  2. mettre A' en forme normale clausale ;
  3. répéter la production de résolvantes et facteurs jusqu'à ce que
    • ou bien la clause vide est produite
    • ou bien il n'est plus possible de produire des clausess nouvelles
  4. si la clause vide est produite alors A est valide ;
    si il n'est plus possible de produire des clausess nouvelles alors A n'est pas valide

N.B. : Il est possible qu'aucun des deux conditions d'arrêt soit atteinte (voir p.ex. le dernier des exemples). La résolution est donc un exemple de procédure de semi-décision pour la logique des prédicats.


suite : stratégie linéaire, programmation logique





















                                                      


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

Logique des prédicats : démonstration automatique (suite)

La stratégie linéaire

Lors de la recherche d'une réfutation d'un ensemble de clauses il faut explorer toutes les possibilités possibles de production de résovante entre deux clauses, et ceci itérativement. Une stratégie linéaire restreint cette combinatoire et diminue ainsi l'espace de recherche.

Définition (réfutation linéaire). Une réfutation est linéaire si


Exemples

Théorème. Soit E un ensemble de clauses. Si il existe une réfutation de E alors il existe une réfutation linéaire de E.


suite : PROLOG































                                                      

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











                                                      


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

PROLOG et la programmation logique

Clauses de Horn

Définition (clause de Horn). Une clause de Horn est une clause avec au plus un littéral positif.

Théorème. Soit E un ensemble de clauses de Horn. Si il existe une réfutation de E alors il existe une réfutation linéaire de E où la règle de factorisation n'est pas utilisée.

De la résolution à la programmation logique

En programmation logique, on sépare les clauses de Horn en faits, règles et questions. Un programme logique est constitué de faits et de règles. C'est une séquence plutôt qu'un ensemble, car cette structure est pertinente pour la stratégie appliquée. Un programme logique est interrogé par des questions.

Définition (fait, règle, programme logique, question).
Un fait est un littéral positif.
Une règle est une clause avec un littéral positif et au moins un littéral négatif (elle est donc de la forme {p, ~p1, ..., ~pn}, avec n > 0)
Un programme logique est une liste de faits et règles.
Une question est une clause sans littéral positif.
Exemples

Définition (réponse). Soit P un programme logique, et soit C une question. Alors une substitution s est une réponse ssi P U {(C)s} est insatisfiable.
Exemples

Notation de PROLOG

Par convention, les expressions représentant des constantes et noms de prédicat ont comme première lettre une minuscule. Les expressions représentant des variables ont comme première lettre ou bien une majuscule, ou bien l'underscore ``_''.
Les faits p sont notés ``p.''.
Les règles {p, ~p1, ..., ~pn} sont notées ``p :- p1, ..., pn''.
Les questions ~P sont parfois notées ``? p.'', mais en sont la plupart du temps représentées dans un champ a part, et notées``p.'' (ou ``p'') comme les faits.

Les implantations de PROLOG

Il existe des implantations de PROLOG qui sont online :

Plus sur PROLOG

Il existe un livre Logic, Programming and Prolog accessible via www.
suite : chapitre sur les logiques non-classiques































                                                      

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