[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

un ensemble dénombrable de symboles de prédicats à 0, 1, ou plusieurs arguments,
notés p, q, r, ..., homme, mortel, père, ...
un ensemble dénombrable de variables d'objets (ou variables d'individu),
notées x, y, z, x₁, x₂, ...
un ensemble dénombrable de fonctions à 0, 1, ou plusieurs arguments,
notées f, g, ... , père-de, ...
les quantificateurs ∀, ∃ (notations alternatives)
les connecteurs FALSE, ~, ∧, ∨, -> ainsi que les parenthèses de la logique propositionnelle

Notation. Q dénote un quantificateur quelconque, c-à-d ∀ ou ∃.
Les fonctions à 0 arguments sont appellées constantes et sont notés sans parenthèses ( a, b, ..., Socrate, ...). Même chose pour les prédicats à 0 arguments, qui 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

toute variable est un terme
f(t₁,...,t_n) est un terme si f est une fonction à n arguments et t₁,...,t_n sont des termes

Définition (formule). Si p est un prédicat à n arguments et t₁,...,t_n sont des termes alors p(t₁,...,t_n) 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 :

(Q x A) est une formule si Q est un quantificateur, x une variable et A une formule

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

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 {x₁ , ... , x_n} l'ensemble des variables tel que s(x) est différent de x . La substitution s est alors notée s = {x₁\t₁ , ... , x_n\t_n}.
Exemples de substitutions

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

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

Introduction

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

un ensemble non-vide D appelé domaine d'individus
une fonction IV de l'ensemble des variables dans D
une fonction IP associant à chaque prédicat à n arguments une application de Dⁿ dans {0,1}
une fonction IF associant à chaque fonction à n arguments une application de Dⁿ dans D

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

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

I(f(t₁,...,t_n)) = (IF(f))(I(t₁),...,I(t_n))

Définition (interprétation des formules). 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 :

I(p(t₁,...,t_n)) = 1 ssi IP(p)( I(t₁,...,I(t_n) ) = 1
I(∀x A) = 1 ssi I'(A) = 1 pour toute variante I' de I en x
I(∃x A) = 1 ssi il existe une variante I' de I en x telle que I'(A) = 1
ainsi que les conditions de vérité des connecteurs propositionnels

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

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

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

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,

si A est valide alors la procédure s'arrête et retourne `oui'
sinon ou bien la procédure s'arrête et retourne `non', ou bien elle ne s'arrête pas.

suite : quelques équivalences utiles

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 :: |- (Q₁ x Q₂ x A) <-> Q₂ 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) ∨ (∃x B) <-> ∃x (A ∨ 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) ∨ B <-> Q x (A ∨ 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

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 Qx₁ ... Qx_n 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) : ~~A <-> A ~(A ∨ B) <-> ~A ∧ ~B ~(A ∧ B) <-> ~A ∨ ~B ~(∀x A) <-> ∃x ~A ~(∃x A) <-> ∀x ~A
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) : (Q x A) ∧ B <-> Q x (A ∧ B) (Q x A) ∨ B <-> Q x (A ∨ B) A ∧ (Q x B) <-> Q x (A ∧ B) A ∨ (Q x B) <-> Q x (A ∨ B)
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

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(x₁,...,x_n)} à la matrice de A , où

x₁,...,x_n sont les quantificateurs universels précédant ∃x dans le préfixe de A
f est une nouvelle fonction qui n'a pas encore été utilisée ;

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

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

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 = {t₁=t'₁ , ... , t_n=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

toutes les parties gauches des équations sont des variables

chaque variable apparaît au plus une fois dans E

Soit E = {x₁=t₁ , ... , x_n=t_n} un ensemble d'équations résolu. La substitution associé à E est s_E = {x₁\t₁ , ... , x_n\t_n}
Annexe : remarque sur les propriétés de s_E

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 :

si elle est de la forme t = t alors la supprimer
si elle est de la forme f(t₁,...,t_n) = g(t'₁,...,t'_m) et f et g sont différentes alors échec
si elle est de la forme f(t₁,...,t_n) = f(t'₁,...,t'_n) alors la remplacer par n équations t₁ = t'₁, ... ,t_n = t'_n
si elle est de la forme t = x et t n'est pas une variable alors la remplacer par x = t
si elle est de la forme x = t et x apparaît dans t alors échec
si elle est de la forme x = t et x n'apparaît pas dans t alors remplacer x par t partout ailleurs dans E

fin tant que ;

rendre la substitution s_E 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

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

C = {p(t₁,...,t_n)}UD
C' = {~p(t'₁,...,t'_n)}UD'
il existe un unifieur le plus général s de {t₁=t'₁ , ... t_n=t'_n} (après avoir éventuellement renommé les variables d'une des deux clauses)

Alors (DUD')s est une résolvante de C et C'.
Exemples

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

ou bien C = {p(t₁,...,t_n),p(t'₁,...,t'_n)}UD,
ou bien C = {~p(t₁,...,t_n),~p(t'₁,...,t'_n)}UD, et

il existe un unifieur le plus général s de {t₁=t'₁ , ... t_n=t'_n}.

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

Définition (réfutation). Une réfutation des clauses C₁,...,C_m est une liste finie de clauses (D₁, ... ,D_n) telle que

D_n est la clause vide {}
pour i = 1, ...,n, la clause D_i est
- soit égale à une des clauses C_j
- soit elle est résolvante de deux clauses D_j, D_k précédant D_i dans la liste
- soit elle est facteur d'une clause D_j précédant D_i dans la liste

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 x₁,...,x_m les variables libres de A. Alors ∀x₁ ... ∀x_n 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

nier A : A' = ~A
mettre A' en forme normale clausale ;
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
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

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

chaque facteur est obtenu à partir de la clause immédiatement précédente
chaque résolvante est obtenue à partir de deux clauses dont exactement une la précède immédiatement

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

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

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, ~p₁, ..., ~p_n}, 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 PU{(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, ~p₁, ..., ~p_n} sont notées ``p :- p₁, ..., p_n''.
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 :

BinProlog
Rentrer le programme dans le champ ``Quick Online Editor'', et la question dans le champ ``Query Interpreter''.
Une extension de BinProlog est le Multi-Engine Horn Clause Prolog de Paul Tarau.

Plus sur PROLOG

Il existe un livre Logic, Programming and Prolog accessible via www.

suite : chapitre sur les logiques non-classiques

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