Une notion plus générale que celle de propriété est celle de prédicat, qui permet d'exprimer une relation entre plusieurs objets, comme père(Jean,Pierre) ou plus_petit_que(3,7). Un prédicat a zéro, un, ou plusieurs arguments. Les variables propositionnelles peuvent être vus comme des prédicats à zéro arguments.
La logique des prédicats est aussi appellée logique des prédicats du premier ordre, par oposition à la logique des prédicats de second ordre qui admettent la quantification non seulement sur des objets mais aussi sur des prédicats, ce qui leur permet de représenter la théorie des ensembles (la logique propositionnelle peut être vue comme logique des prédicats d'ordre zéro).
En ce qui concerne les connecteurs propositionnels, nous avons la même remarque sur les jeux de connecteurs primitifs qu'en logique propositionnelle.
L'application de s à une formule A (notée (A)s) est le résultat du remplacement simultané dans A de toutes les occurrences libres de chaque xi par ti.
Soient s1 et s2 deux substitutions, et soit s1 = {x1\t1 , ... , xn\tn}. Alors la composition de s1 et s2 est s1 o s2 = {x1\(t1)s , ... , xn\(tn)s} U s2 (où U denote l'union ensembliste).
La formule ∀x ∀y ((p(x) ∨ ∃x p(x)) ∧ q(y)) est fermée (c'est la fermeture universelle de A). La formule ∃x ∀y ((p(x) ∨ ∃x p(x)) ∧ q(y)) est également fermée (c'est la fermeture existentielle de A).
(p(x) ∨ q(x,y)){x\z} | = p(z) ∨ q(z,y) |
(p(x) ∨ q(x,y)){x\y} | = p(y) ∨ q(y,y) |
(∀x q(x,y)){x\z} | = ∀x q(x,y) |
(p(x) ∨ q(x,y)){x\z,y\z} | = p(z) ∨ q(z,z) |
(p(x) ∨ q(x,y)){x\f(x)} | = p(f(x)) ∨ q(f(x),y) |
(p(x) ∨ q(x,y)){x\y,y\a} | = p(y) ∨ q(y,a) |
(p(x) ∨ q(x,y)){x\y,y\x} | = p(y) ∨ q(y,x) |
N.B. : les trois dernières substitutions sont particulières :
Pour donner un `sens' aux variables, constantes et fonctions du langage, il faut un domaine d'objets (ou domaine d'individu, ou univers de discours). À chaque variable et constante sera associé un élément du domaine. À chaque fonction sera associé une application dans le domaine.
Ensuite, pour pouvoir donner un `sens' aux formules, il faut une fonction associant à chaque symbole de prédicat à n places l'ensemble des n-uplets d'éléments du domaine qui le rendent vrai.
Finalement, l'interprétation d'une formule A se fait comme en logique propositionnelle : I(A) prend une valeur dans l'ensemble {0,1} (`vrai'/`faux'), où la quantification universelle ∀x A est interprétée comme `pour toute interprétation de x, A est vrai', et la quantification existentielle ∃x A est interprétée comme `il existe une interprétation de x telle que A est vrai'.
I est un modèle de | I n'est pas un modèle de |
---|---|
aime(z,x) | aime(x,z) |
∃z aime(x,z) | ∀z aime(z,x) |
∀x ~aime(x,x) | ∃x aime(x,x) |
∃x ∃y aime(x,y) | ∀y ∃x aime(x,y) |
∀x ∃y aime(x,y) | ∃x ∀y aime(x,y) |
∃u ∃v (aime(u,v) ∧ aime(v,u)) | ∃y ∀x aime(x,y) |
N.B. : nous aurions également pu choisir comme domaine les nombres entiers, réels ou rationels.
formules valides | formules satisfiables et invalides | formules insatisfiables |
---|---|---|
(∀x p(x)) -> p(y) | p(x) | ∀x (p(x) ∧ ~p(x)) |
(∀x p(x)) -> (∃x p(x)) | ∀x p(x) | (∀x p(x)) ∧ (∀z ~p(z)) |
p(x) -> (∃x p(x)) | (∃x p(x)) ∧ (∃x ~p(y)) | (∀x p(x)) ∧ (∃x ~p(x)) |
∃x (p(x) -> (∀x p(x))) | ∀x (p(x) -> (∀x p(x)) | ∀x (p(x) ∧ (∃x ~p(x))) |
(∃x ∀y p(x,y)) -> (∀y ∃x p(x,y))) | (∀x ∃y p(x,y)) ∧ (∀x ∃y ~p(x,y))) | (∀x ∃y p(x,y)) ∧ (∃x ∀y ~p(x,y))) |
N.B. : ni p(y) ni ∀x p(x) sont conséquences logiques de {p(x)}.
Preuve de (∀x p(x)) -> (∃x p(x)) :
Même qu'en logique propositionnelle
On utilise les équivalences suivantes.
∀x ∀y (p(x) ∧ q(y)) | <-> | ∀x (p(x) ∧ ∀y q(y)) | |
<-> | (∀x p(x)) ∧ ∀y q(y) | ||
<-> | (∀x p(x)) ∧ ∀x q(x) | ||
<-> | ∀x (p(x) ∧ q(x)) |
Problème :
pour une formule Il sera cependant possible d'obtenir une formule La formule p(x) ∧ ~p(y) est en forme normale prénexe.
La formule
∀x ∃y ( (p(x) ∧ q(x,y)) ∨ r(z))
est en forme normale prénexe.
∀x ∃y est le préfixe, et
(p(x) ∧ q(x,y)) ∨ r(z) est la matrice.
N.B. : dans une formules en forme normale prénexe
il peut y avoir des variables libres
(comme z dans notre exemple).
La formule
∃x ( (p(x) -> ∀x p(x) )
n'est pas en forme normale prénexe.
La formule ∃x (p(x) ∧ ~p(y)) est en forme normale de Skolem.
La formule
∀x ∃y ( (p(x) ∧ q(x,y)) ∨ r(z))
n'est pas en forme normale de Skolem, à cause de l'occurrence
du quantificateur existentiel ∃y.
N.B. : dans une formules en forme normale de Skolem
il peut y avoir des variables libres
(comme z dans notre exemple).
La formule ∃x ∃y (p(x) ∧ ~p(y))
est en forme normale clausale.
La formule
∀x ∃y ( (p(x) ∧ q(x,y)) ∨ r(z))
n'est pas en forme normale clausale pour deux raisons :
d'une part, la matrice n'est pas en forme normale conjonctive ;
d'autre part, elle n'est pas fermée car la variable z
a une occurrence libre.
même motivation de la nécessité d'une procédure de décision
qu'en logique propositionnelle
De plus, une conséquence de la
semi-décidabilité
de la logique des prédicats
est qu'il n'existe aucune procédure de décision pour
la logique des prédicats :
pour chaque procédure il y aura des formules en entrée
sur lesquelles la procédure ne s'arrête pas
(pas forcement les mêmes).
Comme E est résolu, il n'y a pas de variable x
qui apparaît comme substituée et substituant, c-à-d
que pour tout x\t dans sE :
Alors on a en particulier que
sE est l'upg de E.
De plus,
comme chaque xi apparaît exactement une fois dans E
on a que sE est idempotent :
Soit E = {x=f(y) , y=z}.
Soit E = {x=f(y) , y=z}.
D = {~p(y,u) , ~p1(y) , p2(h(u,y))}
D = {~p(y) , ~p(y')}
N.B. :
la clause résolvante est tautologique.
Elle `ne sert donc à rien' et pourra être éliminé.
N.B. :
comme les clauses sont des ensembles (et non des listes),
les `doublons' engendrés par l'application de l'upg en 2. sont éliminés.
On applique l'algorithme d'unification à {y=f(y)} :
l'algorithme échoue.
Il n'existe donc pas de facteur de C.
N.B. :
contrairement à la production d'une résolvante, la production d'un facteur
ne comporte pas de renommage.
N.B. : remarquer qu'ici une réfutation est impossible sans
utiliser la factorisation
N.B. : cet exemple illustre qu'il ne suffit pas qu'au départ
les variables dans des clauses différentes soient différentes,
et qu'il faut parfois renommer `en cours de route'.
Alors les substitutions
{z\b} et {z\c}
sont des réponses.
Formes normales de la logique des prédicats : exemples
Exemples de formules en forme normale prénexe
Exemple.
Exemple.
Exemple.
Exemples de mise en forme normale prénexe
Exemple.
Soit la formule ∃x ( p(x) -> ∀x p(x) ) :
N.B. : le renommage est essentiel ici ; p.ex.
∃x ( ~p(x) ∨ ∀x p(x) )
n'est pas équivalent à
∃x ∀x ( ~p(x) ∨ p(x) )
Exemple.
Soit la formule
~( p(x) -> ((∃y q(x,y)) ∧ ∃y r(y)) ) :
Remarque.
Il est parfois possible d'être plus économique :
La formule ∀x ∃x (p(x) ∨ q(x))
peut alors être simplifiée en :
∃x (p(x) ∨ q(x)) .
La formule ∀x ( p(x) ∧ ∀y p(y) )
est alors d'abord renommée en
∀x ( p(x) ∧ ∀x p(x) )
et ensuite mis en forme normale prénexe :
∀x ( p(x) ∧ ∀x p(x) ) .
Exemples de formules en forme normale de Skolem
Exemples de mise en forme normale de Skolem
Exemple.
Soit la formule
∃x ∀y p(x,y) :
Exemple.
Soit la formule
∀x ∃y p(x,y) :
Exemple.
Soit la formule
∃u ∀x ∃y ∀z ∃t ( p(x) ∧ q(y) ∧ r(x,z,t) ∧ s(y) ∧ k(u) ) :
Exemples de formules en forme normale clausale
Exemples de mise en forme normale clausale
Exemple.
Soit la formule ∃x ( p(x) -> ∀x p(x) ) :
Exemple.
Soit la formule
∀x ∃y ( (p(x) ∧ q(x,y)) ∨ r(z) ) :
Déduction automatique pour la logique des prédicats : annexes
Introduction et motivation
Remarque sur les substitutions associées à des ensembles d'équations résolus
Remarque.
Soit
Remarque sur la réfutation en tant que déduction
Remarque.
Une réfutation des clauses C1,...,Cm
n'est donc rien d'autre qu'une
déduction
de FALSE à partir de C1,...,Cm ,
dans un système logique ayant aucun axiome et
deux règles d'inférence :
Ce système déductif permet de trouver non pas les formules valides, mais plutôt
les formules insatisfiables.
Déduction automatique pour la logique des prédicats : exemples pour l'unification
Exemple d'unifieur
Un unifieur de E est
s = {x\f(a) , y\a , z\a}.
Un autre unifieur de E est
s = {x\f(z) , y\z}.
Exemples d'unifieur le plus général (upg)
Un upg de E est
s = {x\f(z) , y\z}.
Un autre upg de E est
s = {x\f(u) , y \u , z\u}.
Exemples d'unification
Exemple.
Soit {x=y' , f(y)=u}.
{x=y' , u=f(y)}
{ x\y' , u\f(y) }
Exemple.
Soit {g(y)=g(z) , x=f(y)}.
{y=z , x=f(y)}
{y=z , x=f(z)}
{y\z , x\f(z)}
Exemple.
Soit {x=y , x=f(y)}.
{x=y , x=f(x)}
Exemple.
Soit {x=g(y) , f(x)=z , y=a}.
{x=g(a) , f(x)=z , y=a}
{x=g(a) , f(g(a))=z , y=a}
{x=g(a) , z=f(g(a)) , y=a}
{x\g(a) , z\f(g(a)) , y\a}
Déduction automatique pour la logique des prédicats : exemples pour la résolution
Exemples de résolvantes
Exemple.
Soient les deux clauses
Ensuite on
applique l'algorithme d'unification à E, qui rend
un unifieur le plus général s = {x\y' , u\f(y)}.
La résolvante de C et D ainsi calculée est donc :
Exemple.
Soient les deux clauses
Exemples de facteurs
Exemple.
Soit la clause
Exemple.
Soit la clause
Exemple de réfutation
Notation.
Dans une réfutation, on utilise une ligne numérotée par clause.
On commence par écrire les clauses de départ.
Ensuite on associe un commentaire à chaque ligne spécifiant comment elle a été obtenue.
`` résolvante de 3,1 et 4,1 '' signifie que la clause présente a été obtenue
à partir de la 3ème et 4ème clause, par unification des premiers littéraux de chauque clause.
Exemple.
Soient les clauses
{p(x) , p(x')} et {~p(y) , ~p(y')}.
Une réfutation est :
1 {p(x) , p(x')} clause 1
2 {~p(y) , ~p(y')} clause 2
3 {p(x)} facteur de 1,1 et 1,2 avec {x'\x}
4 {~p(y)} facteur de 2,1 et 2,2 avec {y'\y}
5 {} résolvante de 3,1 et 4,1 avec {x\y}
Exemple.
Soient les clauses
{p(x)} ,
{~p(y) , p(f(y))} et
{~p(f(f(z)))}.
Une réfutation est :
1 {p(x)} clause 1
2 {~p(y) , p(f(y))} clause 2
3 {~p(f(f(z)))} clause 3
4 {p(f(y))} résolvante de 1,1 et 2,1 avec {x\y}
5 {p(f(f(y')))} résolvante de 4,1 et 2,1 avec {y\f(y')}, après avoir renommé {y\y'} en clause 4
6 {} résolvante de 5,1 et 3,1 avec {z\y'}
Exemple.
Soient les clauses
{p(x)} et
{~p(y) , p(f(y))}.
Alors la procédure de résolution ne s'arrête pas :
1 {p(x)} clause 1
2 {~p(y) , p(f(y))} clause 2
3 {p(f(y))} résolvante de 1,1 et 2,1 avec {x\y}
4 {p(f(f(y)))} résolvante de 3,1 et 2,1 avec {y'\f(y)}, après avoir renommé {y\y'} en clause 2
5 {p(f(f(f(y))))} résolvante de 4,1 et 2,1 avec {y'\f(y)}, après avoir renommé {y\y'} en clause 2
6 {p(f(f(f(f(y)))))} résolvante de 5,1 et 2,1 avec {y'\f(y)}, après avoir renommé {y\y'} en clause 2
7 .... ...
Exemple de réfutation linéaire
Exemple.
Parmi les
exemples de réfutation,
la première n'est pas linéaire, tandis que les deux autres le sont.
Une réfutation linéaire du premier ensemble de clauses suit.
Exemple.
Soient les clauses
{p(x) , p(x')} et {~p(y) , ~p(y')}.
Une réfutation linéaire est :
1 {p(x) , p(x')} clause 1
2 {~p(y) , ~p(y')} clause 2
3 {p(x)} factorisation de 1,1 et 1,2 avec {x'\x}
4 {~p(y')} résolvante de 3,1 et 2,1 avec {x\y}
5 {} résolvante de 4,1 et 3,1 avec {x\y'}
Exemples de clauses de Horn
faits règles questions
{p(x)}
{p(x) , ~q(x)}
{~q(x)}
{père(a,b)}
{père(x,y) , ~fils(y,x)}
{~fils(b,a)}
Exemples de réponses
Soit le programme logique
Soit la question {~fils(z,a)}.
P = {
{père(a,b)},
{père(a,c)},
{père(d,a)},
{fils(x,y) , ~père(y,x)} }
https://www.irit.fr/~Andreas.Herzig