Langage de la logique des prédicats : annexes

Introduction et motivation

En logique propositionnelle on se limite à des connecteurs propositionnels (connecteurs associant des propositions, et non des variables et des propositions). Ceci ne permet pas de rendre compte de raisonnements comme le suivant. Ce raisonnement repose sur une analyse plus fine des énoncés en termes d'énoncés génériques (`tout être humain est...') et énoncés singuliers (`Socrate est...'). Il utilise les notions d'objet et de propriété des objets.
On écrit les propriétés d'objets sous la forme être-humain(Socrate).
Socrate est l'objet, et être-humain est la propriété.
C'est un énoncé singulier. Les énoncés génériques nécessitent l'emploi du quantificateur universel . Ainsi, `` TOUT être humain est mortel '' peut être traduit comme (∀x) (être-humain(x) -> mortel(x)) .

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).

Retour


Remarque sur la notation

Remarque.

et sont parfois notés /\ et \/, ce qui rappelle la similarité avec la conjonction et la disjonction : Si on se limite à un ensemble fini d'objets o1,...,on alors :
(/\x) p(x) correspond à la conjonction p(o1) ∧ ... ∧ p(on) et
(\/x) p(x) correspond à la disjonction p(o1) ∨ ... ∨ p(on) .

Retour


Remarque sur les connecteurs primitifs

Remarque. Notre présentation avec les connecteurs primitifs et peut être remplacée par une présentation avec seulement l'un des deux primitif :

En ce qui concerne les connecteurs propositionnels, nous avons la même remarque sur les jeux de connecteurs primitifs qu'en logique propositionnelle.

Retour


Définition plus explicite des formules

Définition. L'ensemble FOR des formules (ou formules bien formées) de la logique des prédicats est le plus petit ensemble de mots construits sur l'alphabet tel que

Retour


Remarque sur une définition plus explicite de la substitution

Remarque. Une définition plus explicite est la suivante : une substitution de variables est un ensemble fini de couples associant à une variable un terme, notée s = {x1\t1 , ... , xn\tn} tel que xi = xj implique i = j.

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).

Retour

































                                                      

Langage de la logique des prédicats : exemples de traduction d'énoncés en formules

Retour


Exemples de variables libres et liées

Dans ∀y ((p(x) ∨ ∃x p(x)) ∧ q(y)) la première occurrence de x est libre, tandis que la deuxième occurrence est liée. L'occurrence de y est liée.

Retour


Exemples de formules fermées et ouvertes

La formule A = ∀y ((p(x) ∨ ∃x p(x)) ∧ q(y)) est ouverte, car il y a une occurrence de variable libre.

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).

Retour


Exemples de substitutions

(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 :

Ces deux cas de figure seront exclus dans la définition des unifieurs.

Retour



























                                                      


Théorie des modèles de la logique des prédicats : annexes

Introduction et motivation

Comme en logique propositionnelle, on fixe d'abord un ensemble de modèles (aussi appellés valuations ou interpretations). Ensuite, pour un modèle donné, on stipule des conditions de vérité permettant d'établir pour n'importe quelle formule A du langage si A est vraie ou fausse dans ce modèle.

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'.

Retour


Remarque sur validité et satisfiabilité

Remarque.

A est insatisfiable si I(A) = 0 pour toute interpretation I, et A est invalide si il existe une interpretation I t.q. I(A) = 0.
Les formules valides sont forcément satisfiables, et les formules insatisfiables sont forcément falsifiables.

Retour





























                                                      

Théorie des modèles de la logique des prédicats : exemples

Exemple d'interpretation

Soit le domaine d'individus D = {Alice, Bernard, Christian}. Soit l'interprétation de variables telle que IV(x) = Alice, I(y) = Bernard, I(z) = Christian. Soit l'interprétation des prédicats telle que IP(aime) (Alice,Bernard) = IP(aime) (Bernard,Alice) = IP(aime) (Christian,Alice) = 1, et 0 sinon.
Le même domaine D avec l'interprétation de variables IV' telle que IV'(x) = Alice, IV'(y) = Bernard = IV(z) et la même interprétation des prédicats est une variante de I en z.
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)

Un autre exemple d'interpretation

Soit la formule A = (∀x ∃y R(x,y)) & (∀x ~R(x,x)) & (∀x ∀y ∀z ((R(x,y)&R(y,z)) -> R(x,z)) ).
Un modèle pour A est l'interprétation I suivante :
Soit D l'ensemble des entiers naturels. Soit l'interprétation du Si le prédicat R est interprété par la relation `strictement plus plus petit que' sur les entiers naturels, alors I est un modèle de A, pour n'importe quelle interprétation des variables.

N.B. : nous aurions également pu choisir comme domaine les nombres entiers, réels ou rationels.

Retour


Exemples de formules valides et satisfiables

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)))

Exemples de conséquences logiques

N.B. : ni p(y) ni ∀x p(x) sont conséquences logiques de {p(x)}.

Retour






















                                                      


Théorie de la preuve de la logique des prédicats : annexes

Introduction et motivation

Tout comme en logique propositionnelle, l'objectif de la théorie de la preuve est de donner une caractérisation finie des formules valides, en se basant sur un (petit) ensemble de `vérités premières' : les axiomes, et un (petit) ensemble de règles permettant de produire toutes les vérités : les règles d'inférence.

Retour





























                                                      

Théorie de la preuve de la logique des prédicats : exemples

Exemples de preuve

Preuve de (∀x p(x)) -> (∃x p(x)) :

  1. (∀x p(x)) -> p(x)
    instance de (∀x A) -> (A){x\t}
  2. ( (∀x p(x)) -> p(x) ) -> ( ((∀x p(x)) -> (p(x) -> (∃x p(x)))) -> ((∀x p(x)) -> (∃x p(x))) )
    instance de (A -> B) -> ((A -> (B -> C)) -> (A -> C))
  3. ((∀x p(x)) -> (p(x) -> (∃x p(x)))) -> ((∀x p(x)) -> (∃x p(x)))
    obtenue par Modus Ponens à partir de 1. et 2.
  4. p(x) -> (∃x p(x))
    instance de (A){x\t} -> (∃x A)
  5. (p(x) -> (∃x p(x))) -> ((∀x p(x)) -> (p(x) -> (∃x p(x))))
    instance de A -> (B -> A)
  6. (∀x p(x)) -> (p(x) -> (∃x p(x)))
    obtenue par Modus Ponens à partir de 4. et 5.
  7. (∀x p(x)) -> (∃x p(x))
    obtenue par Modus Ponens à partir de 3. et 6.

Retour


Exemples de formules prouvables et consistantes

Se référer aux formules valides et satisfiables (ce seront l'adéquation et complétude qui garantiront que l'ensemble des formules prouvables est indentique à l'ensemble des formules valides, et que l'ensemble des formules consistantes est indentique à l'ensemble des formules satisfiables)

Retour




































                                                      


Propriétés importantes de la logique des prédicats : annexes

Introduction et motivation

Même qu'en logique propositionnelle

Retour




























                                                      


Propriétés importantes de la logique des prédicats : exemples

Exemples d'application des équivalences

Exemple.

|- (∀x ∀y (p(x) ∧ q(y))) <-> ∀x (p(x) ∧ q(x))

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))
On utilise donc successivement

  1. l'élargissement de la portée de ∀y (car il n'y a pas d'occurrence libre de y dans p(x))
  2. l'élargissement de la portée de ∀x, (car il n'y a pas d'occurrence libre de x dans ∀y q(y))
  3. le renommage de y
  4. la distributivité de ∀x sur la conjonction.
ainsi que le fait que le remplacement des équivalences est valide (v. aussi son corollaire).

Exemple.

p(x) ∧ ~p(y) est satisfiable ssi (∃x p(x)) ∧ ∃y ~p(y) est satisfiable.
  1. Fermeture universelle :
    soit A sans occurrence libre de x. Alors
    |- A ssi |- ∀x A .
  2. Fermeture existentielle :
    soit A sans occurrence libre de x. Alors
    A est satisfiable ssi ∃x A est satisfiable.
  3. Quantification répetée :
    |- (Q1 x Q2 x A) <-> Q2 x A
  4. Quantification sans variable libre :
    soit A sans occurrence libre de x. Alors
    |- (Q x A) <-> A
    |- (A){x\t} <-> A
  5. Renommage :
    |- (Q x A) <-> Q y (A){x\y}
  6. Les deux cas où la distribution est possible :
    |- (∀x A) ∧ (∀x B) <-> ∀x (A ∧ B)
    |- (∃x A) ∨ (∀x B) <-> ∃x (A ∨ B)
  7. 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)

Retour






























                                                      

Formes normales de la logique propositionnelle : annexes

Introduction et motivation

Problème : pour une formule A de la logique des prédicats il n'existe pas toujours une formule en forme normale conjonctive équivalente (comme c'est le cas en logique propositionnelle).

Il sera cependant possible d'obtenir une formule A' telle que A est satisfiable ssi A' est satisfiable. On procède en trois étapes :

  1. mise en forme normale prénexe : séparation en une suite de quantificateurs et une formule sans quantificateurs (la matrice)
  2. mise en forme normale de Skolem : élimination des quantificateurs existentiels
  3. mise en forme normale conjonctive de la matrice, en utilisant le même algorithme qu'en logique propositionnelle

Retour














                                                      

Formes normales de la logique des prédicats : exemples

Exemples de formules en forme normale prénexe

Exemple.

La formule p(x) ∧ ~p(y) est en forme normale prénexe.

Exemple.

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).

Exemple.

La formule ∃x ( (p(x) -> ∀x p(x) ) n'est pas en forme normale prénexe.

Retour


Exemples de mise en forme normale prénexe

Exemple.

Soit la formule ∃x ( p(x) -> ∀x p(x) ) :

Éliminer -> :
∃x ( ~p(x) ∨ ∀x p(x) )

Renommer ∀x p(x) en ∀y p(y) :
∃x ( ~p(x) ∨ ∀y p(y) )

Sortir ∀y :
∃x ∀y ( ~p(x) ∨ p(y) )
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)) ) :

Éliminer -> :
~( ~p(x) ∨ ((∃y q(x,y)) ∧ ∃y r(y)) )

Rentrer ~ :
~~p(x) ∧ ~((∃y q(x,y)) ∧ ∃y r(y))
p(x) ∧ ~((∃y q(x,y)) ∧ ∃y r(y))
p(x) ∧ (~(∃y q(x,y)) ∨ ~∃y r(y))
p(x) ∧ ((∀y ~q(x,y)) ∨ ~∃y r(y))
p(x) ∧ ((∀y ~q(x,y)) ∨ ∀y ~r(y))

Renommer ∀y ~r(y) en ∀z ~r(z) :
p(x) ∧ ((∀y ~q(x,y)) ∨ ∀z ~r(z))

Sortir ∀y et ∀z :
p(x) ∧ ∀y ( ~q(x,y) ∨ ∀z ~r(z))
∀y ( p(x) ∧ ( ~q(x,y) ∨ ∀z ~r(z)) )
∀y ( p(x) ∧ ∀z ( ~q(x,y) ∨ ~r(z)) )
∀y ∀z ( p(x) ∧ ( ~q(x,y) ∨ ~r(z)) )

Remarque.

Il est parfois possible d'être plus économique :
  1. On peut économiser des quantificateurs en utilisant qu'on peut éliminer les quantificateurs qui `ne servent à rien' :
    La formule ∀x ∃x (p(x) ∨ q(x))
    peut alors être simplifiée en : ∃x (p(x) ∨ q(x)) .
  2. On peut économiser des variables (c-à-d éviter l'introduction de nouvelles variables) en utilisant la distribution de ∀x sur et de ∃x sur , (après avoir utilisé le renommage pour engendrer le même x partout) :
    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) ) .

Retour


Exemples de formules en forme normale de Skolem

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).

Retour


Exemples de mise en forme normale de Skolem

Exemple.

Soit la formule ∃x ∀y p(x,y) :

remplacer x par la constante a :
∀y p(a,y)

Exemple.

Soit la formule ∀x ∃y p(x,y) :

remplacer y par la fonction f(x) :
∀x p(x,f(x))

Exemple.

Soit la formule ∃u ∀x ∃y ∀z ∃t ( p(x) ∧ q(y) ∧ r(x,z,t) ∧ s(y) ∧ k(u) ) :

remplacer u par la constante a :
∀x ∃y ∀z ∃t ( p(x) ∧ q(y) ∧ r(x,z,t) ∧ s(y) ∧ k(a) )

remplacer y par la fonction f(x) :
∀x ∀z ∃t ( p(f(x)) ∧ q(f(x)) ∧ r(f(x),z,t) ∧ s(y) ∧ k(a) )

remplacer t par la fonction g(x,z) :
∀x ∀z ( p(f(x)) ∧ q(f(x)) ∧ r(f(x),z,g(x,z)) ∧ s(y) ∧ k(a) )

Retour


Exemples de formules en forme normale clausale

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.

Retour


Exemples de mise en forme normale clausale

Exemple.

Soit la formule ∃x ( p(x) -> ∀x p(x) ) :

mise en forme normale prénexe :
∃x ∀y ( ~p(x) ∨ p(y) )

mise en forme normale de Skolem :
∀y ( ~p(a) ∨ p(y) )

... qui est aussi sa forme normale clausale ; l'ensemble de clauses associé est :
{ {~p(a)} , {p(y)} }

Exemple.

Soit la formule ∀x ∃y ( (p(x) ∧ q(x,y)) ∨ r(z) ) :

fermer existentiellement :
∃z ∀x ∃y ( (p(x) ∧ q(x,y)) ∨ r(z) )

mettre en forme normale prénexe : la formule l'est déjà

mettre en forme normale de Skolem :
∀x ( (p(x) ∧ q(x,f(x))) ∨ r(a) )

mettre la matrice en forme normale conjonctive :
∀x (p(x) ∨ r(a)) ∧ (q(x,f(x)) ∨ r(a))

L'ensemble de clauses associé est
{ {p(x) , r(a)}, {q(x,f(x)) , r(a)} }

Retour




















                                                      


Déduction automatique pour la logique des prédicats : annexes

Introduction et motivation

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).

Retour


Remarque sur les substitutions associées à des ensembles d'équations résolus

Remarque.

Soit
E = {x1=t1 , ... , xn=tn}
un ensemble d'équations résolu, et soit sE la substitution associée à E.

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 :

sE o sE = sE

Retour


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.

Retour




























                                                      


Déduction automatique pour la logique des prédicats : exemples pour l'unification

Exemple d'unifieur

Soit E = {x=f(y) , y=z}.
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}.

Retour


Exemples d'unifieur le plus général (upg)

Soit E = {x=f(y) , y=z}.
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}.

Retour


Exemples d'unification

Exemple.

Soit {x=y' , f(y)=u}.
  1. inversion de f(y)=u :
    {x=y' , u=f(y)}
  2. L'upg associé est donc :
    { x\y' , u\f(y) }

Exemple.

Soit {g(y)=g(z) , x=f(y)}.
  1. décomposition de g(y) = g(z) :
    {y=z , x=f(y)}
  2. remplacement y\z :
    {y=z , x=f(z)}
  3. L'upg associé est donc :
    {y\z , x\f(z)}

Exemple.

Soit {x=y , x=f(y)}.
  1. remplacement x\y :
    {x=y , x=f(x)}
  2. échec par `occur check' (car x apparaît dans t(x))

Exemple.

Soit {x=g(y) , f(x)=z , y=a}.
  1. remplacement y\a :
    {x=g(a) , f(x)=z , y=a}
  2. remplacement x\g(a) :
    {x=g(a) , f(g(a))=z , y=a}
  3. inversion de f(g(a))=z :
    {x=g(a) , z=f(g(a)) , y=a}
  4. L'upg associé est donc :
    {x\g(a) , z\f(g(a)) , y\a}

Retour




















                                                      


Déduction automatique pour la logique des prédicats : exemples pour la résolution

Exemples de résolvantes

Exemple.

Soient les deux clauses
C = {p(x,f(y)) , q(x,y,z)}

D = {~p(y,u) , ~p1(y) , p2(h(u,y))}

  1. Il faut d'abord renommer une des clauses pour que les ensembles de variables des deux clauses soient disjoints. Disons la deuxième, qui en substituant y' à y devient :
    D' = (D){y\y'} = {~p(y',u) , ~p1(y') , p2(h(u,y'))}
  2. Les littéraux p(x,f(y)) et ~p(y,u) sont des `candidats' pour être complémentaires. On forme alors l'ensemble d'équations E = {x=y' , f(y)=u} entre les arguments des deux prédicats.
    Ensuite on applique l'algorithme d'unification à E, qui rend un unifieur le plus général s = {x\y' , u\f(y)}.
  3. Alors
    1. on supprime p(x,f(y)) de C et ~p(y,u) de D',
    2. on applique s à ce qui reste dans les deux clauses
    3. et on `met les deux restes ensemble' :
      (C - {p(x,f(y))})s U (D' - {~p(y,u)})s
    La résolvante de C et D ainsi calculée est donc :
    {q(y',y,z) , ~p1(y') , p2(h(f(y),y'))}

Exemple.

Soient les deux clauses
C = {p(x) , p(x')}

D = {~p(y) , ~p(y')}

  1. Comme il n'y a pas de variable commune, un renommage n'est pas nécessaire.
  2. Les littéraux p(x) et ~p(y) sont des `candidats' pour être complémentaires. L'ensemble d'équations E = {x=y} admet comme upg s = {x\y}.
  3. Alors
    1. on supprime p(x) de C et ~p(y) de D,
    2. on applique s à ce qui reste dans les deux clauses
    3. et on `met les deux restes ensemble' :
      (C - {p(x)})s U (D - {~p(y)})s = {p(x') , ~p(y')}

N.B. : la clause résolvante est tautologique. Elle `ne sert donc à rien' et pourra être éliminé.

Retour


Exemples de facteurs

Exemple.

Soit la clause
C = {~p(x,a) , ~p(f(y),y) , q(y,z)}.
  1. On applique l'algorithme d'unification à {x=f(y) , a=y}, qui rend un unifieur le plus général s = {x\f(a) , y\a}.
  2. Alors on applique s à C : Un facteur de C est donc :
    (C)s = {p(f(a),a) , q(a,z)}

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.

Exemple.

Soit la clause
C = {~p(y) , ~p(f(y))}.

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.

Retour


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}

N.B. : remarquer qu'ici une réfutation est impossible sans utiliser la factorisation

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'}

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'.

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 .... ...

Retour


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'}

Retour


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)}

Retour


Exemples de réponses

Soit le programme logique
P = { {père(a,b)},
{père(a,c)},
{père(d,a)},
{fils(x,y) , ~père(y,x)} }
Soit la question {~fils(z,a)}.

Alors les substitutions {z\b} et {z\c} sont des réponses.

Retour


















































                                                      

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