Université de M'sila

Département Informatique
3eme Licence -SI -

Programmation logique

Rappel de logique pour prolog

1
2018 / 2019
 Rappel de logique pour prolog

Introduction

Logique des propositions

Logique des prédicats

2
 INTRODUCTION
VÉRITÉ ET VALIDITÉ (1)

Logique :
“Etudes des raisonnements valides”
- Philosophie : raisonnement humain
- Mathématiques : validité des démonstrations
- Informatique : traitement automatique de l’information

Raisonnement logique:
Articulation de plusieurs jugements, c’est-à-dire de propositions
auxquelles on peut associer une valeur de vérité
- Hypothèses ou prémisses : propositions supposées ou jugées
vraies au départ du raisonnement
- Conclusion : nouvelle proposition déduite des hypothèses
3
 INTRODUCTION
VÉRITÉ ET VALIDITÉ (2)

Raisonnement 1 Valide • Raisonnement 2 Valide

Tous les chevaux ont une crinière Tous les oiseaux volent
Les poneys sont des chevaux L ’autruche est un oiseau
Donc les poneys ont une crinière Donc l’autruche vole

• Raisonnement 3 Invalide • Raisonnement 4 Valide

Tout nombre pair est divisible par 2 Tout nombre pair est divisible par 2
Tout nombre divisible par 2 est pair 6 est nombre pair
6 est divisible par 2

Validité ≠ Vérité

4
 INTRODUCTION
LOGIQUE

Deux approches ...

Approche syntaxique Approche sémantique

(formelle) Étude du point de vue de la
Étude du point de vue de la propagation de la vérité entre
forme des énoncés logiques prémisses et conclusions

5
 INTRODUCTION
LOGIQUE: APPROCHE FORMELLE
• Axiome:
Proposition primitive considérée comme non démontrable et admise a priori
Exemple : axiomes de la géométrie euclidienne
• Théorème
Proposition pouvant être démontrée à partir d’axiomes ou d’autres théorèmes à
l’aide de raisonnement formels valides. Les axiomes sont considérés comme des
théorèmes particuliers.
Notation :
T
• Règle d’inférence
Schéma minimal de raisonnement valide qui permet de produire de nouvelles
propositions à partir de prémisses qui sont soient des théorèmes, soit des
hypothèses.
Exemple : modus ponens Notation

(P1) Si A alors B
(P2) A P1, P2
T
(T) Donc B
6
 INTRODUCTION
LOGIQUE: APPROCHE SEMANTIQUE (1)
• Sens Sens d’un énoncé logique = valeur de vérité {V,F}
• Interprétation Toute application I attribuant une valeur de vérité aux propositions
P d’un système logique : I(P) ∈ {V,F }
• Modèle Une interprétation I est un modèle d’une proposition logique P ssi
I(P)=V. On dit que P est satisfaisable.
• Tautologie Une proposition logique P est dite tautologique ssi elle est vraie
pour toute interprétation I. Exemple: P ∨ ¬P
Notation ╞ T
• Contradiction Une proposition logique est dite contradictoire, ou insatisfaisable,
si elle n’admet aucun modèle. Exemple: P ∧ ¬P
• Equivalence Deux propositions logiques A et B sont équivalentes logiquement
ssi elles ont la même valeur de vérité pour toute interprétation
Exemple: P⇒Q ≡ ¬P ∨ Q
Notation A≡B
7
 INTRODUCTION
LOGIQUE: APPROCHE SEMANTIQUE (2)
• Conséquence logique Une proposition logique B est la conséquence logique
d’une proposition logique A ssi tout modèle de A est un
modèle de B
Notation A╞B
Exemple : {P , P⇒Q} ╞ Q

• Raisonnement valide Un raisonnement est dit valide ssi sa conclusion est la

conséquence logique de ses prémisses.
Notation
P1, …, Pn ╞ B

8
 INTRODUCTION
EQUIVALENCE ENTRE APPROCHES

• Consistance Un système logique est sain (ou consistant) si tout

théorème obtenu par démonstration formelle est une
conséquence logique des axiomes

• Complétude Un système logique est dit complet si, pour tout

ensemble de formules du système logique, les
conséquences logiques de ces formules peuvent être
démontrées comme des théorèmes de ces dernières
(i.e. en sont des conséquences formelles).

• Système sain et complet Dans un système logique sain et complet, tout

théorème est une tautologie et réciproquement

Exemple LP et LP1

9
 Logique des propositions

10
 LOGIQUE DES PROPOSITIONS

Exemple
Si le drapeau est vert et si je suis raisonnable alors je ne me baigne pas
Je peux me noyer ssi je ne suis pas raisonnable ou je ne sais pas nager
Le drapeau est rouge et je me baigne
Je risque la noyade

• Atome Jugement de base irréductible : drapeau_vert

Connecteurs logiques
Désignation Symbole signification
Négation ¬ Ne … pas
Conjonction ∧ Et
Disjonction ∨ Ou
Implication ⇒ Alors

Équivalence ⇔ ssi

11
 LOGIQUE DES PROPOSITIONS
SYNTAXE
• Vocabulaire

Symboles représentant les atomes : chaînes de caractères

Symboles des connecteurs logique : { ¬ , ∧ , ∨, ⇒ , ⇔, ..}

Symboles de parenthésage : { ( , ) }
• Règles de construction des formules bien formées (fbf)

Tout atome P est une fbf de la LP

Si F est une fbf, alors ( F ) est une fbf

Si F est une fbf alors ¬ F est une fbf

Si A et B sont deux fbf, alors les formules suivantes sont des fbf :
A ∧ B, A ∨ B, A ⇔ B, A ⇒B
Exemples : P⟹Q ⋁ R est bien formée.
P⟹ ⋁ Q ne l’est pas.

Priorités : 1) ¬ 2) ∧ 3) ∨ 4) ⇒ 5) ⇔

Associativité à gauche
l’écriture : P CL Q CL R est écrite avec les parenthèse comme :
(P CL Q) CL R ; où P, Q et R sont des fbf et CL est un connecteur logique
Exemple: A ⇒ B ⇒ F (A⇒B)⇒F
12
 LOGIQUE DES PROPOSITIONS
CALCUL DES PROPOSITIONS

• Compositionnalité de la LP (Calcul Booléen)

La valeur de vérité d’une fbf de la LP dépend uniquement :
- de l’interprétation des atomes qui la composent
-de l’emploi des connecteurs logiques entre ces atomes
• Tables de vérité

13
 LOGIQUE DES PROPOSITIONS
FORMULES D’EQUIVALENCE DE LA LP
P⇒Q≡¬P∨Q
Equiv. connecteurs
P ⇔ Q ≡ (P ⇒ Q ) ∧ (Q ⇒ P ) ≡ (P ∧ Q ) ∨ (¬P ∧ ¬Q )
Double négation ¬¬P≡P
¬ (P ∧ Q ) ≡ ¬P ∨ ¬Q
Lois de Morgan
¬ (P ∨ Q ) ≡ ¬P ∧ ¬Q
Idempotence P∧P≡P∨P≡P
P∧Q≡Q∧P
Commutativité
P∨Q≡Q∨P
(P ∧ Q) ∧ R ≡ P ∧ (Q ∧ R) ≡ P ∧ Q ∧ R
Associativité
(P ∨ Q) ∨ R ≡ P ∨ (Q ∨ R) ≡ P ∨ Q ∨ R
Contradiction P ∧ ¬P ≡ Faux
Tiers-exclus P ∨ ¬P ≡ Vrai
P ∨ ( Q ∧ R ) ≡ (P ∨ Q) ∧ (P ∨ R)
Distributivité
P ∧ ( Q ∨ R ) ≡ (P ∧ Q) ∨ (P ∧ R)
P∨(P∧Q)≡ P
Absorption
P∧(P∨Q)≡ P
14
 LOGIQUE DES PROPOSITIONS
FORMES NORMALES (1)
Système complet de connecteur { ¬ , ∧ , ∨ }
Littéral On appelle littéral tout atome ou sa négation
Exemples : Q ou ¬ R
Forme normale conjonctive
Une fbf de LP est dite sous forme normale conjonctive (fnc) ssi elle
se compose d'une conjonction de disjonctions de littéraux
Exemple : (P ∨ Q) ∧ (Q ∨ ¬ R) ∧ ¬ P mais aussi …. P ∨ Q
Forme normale disjonctive
Une fbf de LP est dite sous forme normale disjonctive (fnd) ssi elle
se compose d'une disjonction de conjonctions de littéraux
Exemple : (P ∧ Q) ∨ (Q ∧ ¬R) ∨ ¬P mais aussi …. P ∧ Q

15
 LOGIQUE DES PROPOSITIONS
FORMES NORMALES (2)

Toute fbf de LP admet une fnc et une fnd (minimales) uniques (à

une commutation prête) qui lui sont logiquement équivalentes.

Algorithme de mise sous forme normale

1) Passage dans le système complet {¬
¬,∧,∨}
Remplacement des ⇒ et ∨ par équivalence
2) Réduction des négations
Lois de De Morgan + double négation
3) Distributivité + commutativité + absorption
P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R) pour la fnc
P ∧ (Q ∨ R) ≡ (P ∧ Q) ∨ (P ∧ R) pour la fnd.

16
 LOGIQUE DES PROPOSITIONS
DEDUCTION EN LOGIQUE DES PROPOSITIONS
Rappel
Un raisonnement logique est valide ssi sa conclusion est la
conséquence logique de ses prémisses. On note alors : P1, ..., Pn ╞ C
Méthode des tables de vérité
Application directe de la définition de la conséquence logique : il suffit
d’évaluer à l’aide d’une table de vérité l’ensemble des modèles de
P1∧ ... ∧ Pn constituent des modèles de C
Principe de déduction par réfutation (théorème)
Pour montrer que P1, ..., Pn ╞ C (raisonnement valide) il faut et il suffit
de montrer que la formule de réfutation Fr ≡ P1 ∧ ... ∧ Pn ∧ ¬C est
contradictoire.
On dit alors qu'on a montré la validité par réfutation de la conclusion

17
 LOGIQUE DES PROPOSITIONS
RESOLUTION EN LOGIQUE DES PROPOSITIONS (1)
Clause On appelle clause toute disjonction d'atome ou de littéraux
d'atome. Exemples : P ∨ Q ou P ∨ ¬ Q
Forme clausale Une formule est dite sous forme clausale si elle se
présente comme une conjonction de clauses
Notation : Si P un littéral d’une clause C, on notera C\P la clause dont
tous les littéraux sont ceux de C sauf P.
Exemple: (P ∨ Q ∨ R) \ Q ≡ P ∨ R
Règle de résolution
Soient (S1) et (S2) deux clauses appartenant à une formule (S) mise
sous forme clausale. S'il existe un atome L tq L ∈ (S1) et ¬L ∈ (S2)
alors la clause : (R) ≡ (S1 \ {L} ) ∪ (S2 \ {¬L} ) dite résolvante de (S1)
et (S2) est une conséquence logique de (S1) et (S2)
Corollaire : (S) et (S) ∪ (R) sont logiquement équivalentes
(Herbrand, Robinson)
Exemple (S1) = P ∨ Q, (S2) = R ∨ ¬Q alors res(S1,S2) = P ∨ R
18
 LOGIQUE DES PROPOSITIONS
RESOLUTION EN LOGIQUE DES PROPOSITIONS (2)
Méthode de résolution de Robinson
Pour montrer qu'une formule (S) est contradictoire, il faut et il suffit de
produire la clause vide (notée ) par résolution de l'ensemble des clauses
issues de (S) mise sous forme clausale
Soit un raisonnement dont on cherche à montrer la validité
1 — Construction de la formule de réfutation associée
2 — Mise sous forme clausale de la formule de réfutation (Fr)
3 — tant que la clause vide n'appartient pas à (Fr) ou bouclage
3.1. appliquer la résolution sur 2 clauses de (Fr)
3.2. ajouter la résolvante à (Fr)
4 — Si clause vide : raisonnement valide. Sinon, non valide.

19
 LOGIQUE DES PROPOSITIONS
RESOLUTION EN LOGIQUE DES PROPOSITIONS (3)

Deux règles d'inférence :

Résolution. Soient C1 et C2 deux clauses, soit p un litteral.

C1 ∨ p C2 ∨ ¬p
R = C1 ∨ C2

On appelle R la résolvante de C1 ∨ p et C2 ∨ ¬p

Factorisation. Soient C une clause et p une litteral

C∨p∨p
C∨p

20
 LOGIQUE DES PROPOSITIONS
RESOLUTION EN LOGIQUE DES PROPOSITIONS (3)
Méthode de résolution de Robinson: exemple
Modus ponens A, A ⇒ B a-t-il pour conséquence logique B ?
Formule de réfutation Fr ≡ A ∧ (A ⇒ B) ∧ ¬ B
Formule clausale Fr ≡ A ∧ (¬ A ∨ B) ∧ ¬ B trois clauses
Résolution A ¬ A∨ B ¬B

B
¬A

2 démonstrations Fr contradictoire donc Raisonnement valide

21
 Logique des prédicats
du 1er ordre

22
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE

Avec la logique des propositions, on peut :

•Représenter l’information,
•déduire / inférer de nouvelles connaissances.

Mais on ne peut pas
•Généraliser
•Utiliser des relations

La logique des propositions

suppose que le monde contient des faits
La logique des prédicats

Suppose que le monde contient :
•Des objets : Gens, maisons, nombres, …
•Des relations : Frères, plus grand que, …
•Des fonctions : Le père de, le meilleur ami de, …
23
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
Exemple de raisonnement en LP1
Tout être humain a un père
Le grand-père de quelqu'un est le père du père de ce dernier
Khaled est un être humain
Donc, Khaled a un grand-père
prédicat : jugement élémentaire dont la valeur de vérité dépend de ses
arguments. Tout prédicat a un nombre fixe d’arguments : arité.
Syntaxe LP1 : vocabulaire

connecteurs logiques ¬, ∨, ∧, ⇒, ⇔, etc..

symboles de quantification ∀ : tout ; ∃ : il existe

constantes symboles commençant par majuscule Khaled, V, F

variables symboles commençant par une minuscule x

fonctions ident. commençant par un minuscule pere(x)

prédicats ident. commençant par une majuscule Humain(x)

Égalité ( entre termes) =

24
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
SYNTAXE (1)

Termes représentation des éléments du problème :
• constantes
• variables
• fonctions nom_fonction(terme1, ..., terme n)

Formules atomiques représentation des jugements de base
• prédicats Nom_predicat(term1, ... , terme n)
Exp: Frères(Salah,Rachid)

Formules complexe: elles sont construites à partir des formules
atomiques en ajoutant des connecteurs.
Exp:
Frères(Salah,Rachid) ⇒ Frères(Rachid,Salah)

Un littéral est une formule atomique (Littéral positif ) ou la négation d'une
formule atomique (Littéral négatif).

Exemples

Frères(Salah,Rachid) (littéral positif )

¬ Frères(Salah,Rachid) (littéral négatif).
25
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
SYNTAXE (2)

Formules bien formées (fbf)
Toute formule atomique P est une fbf

Si P est une fbf (P) et ¬ P sont des fbf

Si P et Q sont des fbf P ∧ Q , P ∨ Q , P ⇒ Q et P ⇔ Q sont des fbf

Si P est une fbf et x variable
•∀x (P) est une fbf
•∃x (P) est une fbf

Priorités Exemple
1) ¬ 2) ∧ ∀x A(x) ∨ ∃B(x,y) ⇒ A(x) ⇒ B(x,y)
3) ∨ 4) ∀ , ∃
5) ⇒ 6) ⇔ ( ( ∀x( A(x) ∨ ∃B(x,y) )⇒
⇒ A(x) ) ⇒ B(x,y) )

Associativité à gauche
l’écriture : P CL Q CL R est écrite avec les parenthèse comme :
(P CL Q) CL R ; où P, Q et R sont des fbf et CL est un connecteur logique
Exemple: A(x) ⇒ B(y) ⇒ F(z) ( A(x) ⇒ B(y) ) ⇒ F(z)
26
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
QUANTIFICATION UNIVERSELLE

∀<variables><enonce>

Tous les étudiants sont intelligents :

∀x Etudiant(x)⇒ Intelligent(x)

∀x P est vrai dans un modèle si et seulement si P est vrai pour tous les
objets x

∀x P est équivalent à la conjonction de toutes les instanciations de P :
Etudiant(Fateh)⇒Intelligent(Fateh) ∧
Etudiant(Tarek)⇒Intelligent(Tarek) ∧
Etudiant(Salima)⇒Intelligent(Salima) ∧
Etudiant(Fatma)⇒Intelligent(Fatma) ∧ …

27
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
QUANTIFICATION UNIVERSELLE

Erreur fréquente à éviter

•Le connecteur principal à utiliser avec ∀ est l’implication ⇒

•Erreur fréquente : utiliser la conjonction ∧ comme connecteur
principal avec ∀
•∀x Etudiant(x) ∧ Intelligent(x) signifie “tout le monde est étudiant et
tout le monde est intelligent”

28
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
QUANTIFICATION EXISTENTIELLE

∃<variables><enonce>

Un étudiant est intelligent :

∃x Etudiant(x)∧ Intelligent(x)

∃x P est vrai dans un modèle si et seulement si P est vrai pour un
objet x

∃x P est équivalent à la disjonction de toutes les instanciations de P
:
Etudiant(Fateh)∧Intelligent(Fateh) ∨
Etudiant(Tarek)∧Intelligent(Tarek) ∨
Etudiant(Salima)∧Intelligent(Salima) ∨
Etudiant(Fatma)∧Intelligent(Fatma) ∨ …

29
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
QUANTIFICATION EXISTENTIELLE

Erreur fréquente à éviter

Le connecteur principal à utiliser avec ∃ est la conjonction ∧

Erreur fréquente : utiliser l’implication ⇒ comme connecteur principal
avec ∃

∃x Etudiant(x)⇒ Intelligent(x) est vrai s’il existe quelqu’un qui n’est pas
étudiant!

30
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
PROPRIÉTÉS DES QUANTIFICATEURS

∀x∀y est équivalent à ∀y∀x

∃x∃y est équivalent à ∃y∃x

Attention : ∃x∀y n’est pas équivalent à ∀y∃x

∃y∀x Mange(x,y) “Il existe une chose mangé par tout le monde”

∀x∃y Mange(x,y) “Tout le monde mange quelque chose” (pour toute
personne, il existe quelque chose qu’il mange)

Liens entre ∀ et ∃ : Les deux quantificateurs sont liés par le biais de la
négation :

∀x Mange(x,Glace) est équivalent à ￢ ∃x￢ Mange(x,Glace)

∃x Mange(x,Brocoli) est équivalent à ￢ ∀x￢ Mange(x,Brocoli)

31
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
MODELISATION D’EXPRESSIONS

Exemples
x est un lion , -------------> L(x) : x est un lion
x est féroce, -------------> F(x) : x est féroce
x boit du café, -------------> C(x) : x boit du café
x est un singe -------------> S(x) : x est un singe

Tous les lions sont féroces : -------------> ∀x L(x) ⇒ F(x)

Quelques lions ne boivent pas de café : -------------> ∃x L(x) ∧¬C(x)
Aucun singe n’est un lion : -------------> ∀x, S(x) ⇒ ¬L(x)
Tous les singes boivent du café : -------------> ∀x S(x) ⇒ C(x)

32
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
VARIABLES LIBRES / LIEES (1)

Portée portée d'un quantificateur : formule à laquelle il s'applique

Exemples ∃x ( Riche(x) ∧ Avare(x) )
∃x Riche(x) ∧ ∃x Avare(x)
Variable libre / liée
une variable x est dite variable libre (respectivement liée) d’une
formule P ssi x a toutes ses occurrences en dehors (resp. en
dedans) de la portée des quantificateurs de P
Formule close / ouverte
Une formule est dite close ssi elle n'a aucune variable libre.
On parle sinon de formule ouverte
Exemples
Dans

∀ x ( Humain(x) ∧ Humain(y) ∧ Chien(Toto) ) , x est liée, y est libre
(formule ouverte)

∃ y ¬ (Amis(Hakim,y)) , y est liée (formule close )
33
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
VARIABLES LIBRES / LIEES (2)

Exemples:

F1 : Q(A,f (x))
• Formule atomique comportant une occurrence de x, x est donc libre.

F2 : ∀z Q(A,f (x))
• F2 = ∀z F1, comme z ≠ x, le fait que x soit libre dans F1 entraine que
x est libre dans F2.

F3 : ∀x ∀y Q(x,y) ⇒ ∃z P(z)
• F3 est une formule close (x et y liées par ∀ et z liée par ∃).

F4 : Q(B,B) ⇒ ∀x (P(x) ∨ ∃x Q(x,y)
• y est libre.
• ∀x ne peut lier qu’une variable libre c’est à dire x dans P(x).
• L’occurrence de x dans Q(x,y) est liée par ∃x.
• Donc les deux variables x sont liées (mais différemment).
34
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
VARIABLES LIBRES / LIEES (3)
Forme propre Ecriture d’une fbf où il n’y a aucun conflit de portée
Exemple ∀x (∃y Père(x,y) ∧ ∃y Mere(x,y) )
Standardisation Mise sous forme propre d’une fbf

 Variable dépendant de plusieurs portées : Formule mal formée,

renommer les variables dans les quantificateurs pour la rendre
cohérente
Exemple ∀x (∃y Père(x,y) ∧ ∃x Mere(x,Khaled) )
∀x (∃y Père(x,y) ∧ ∃z Mere(z,Khaled) )
 Conflit variable libre et liée : Renommer la variable libre
Exemple ∀x (∃y Père(x,y) ∧ Mere(x,y) )
∀x (∃y Père(x,y) ∧ Mere(x,z) )

 Variables liées de portées différentes : Renommer les variables

pour éviter toute erreur ultérieure
Exemple ∀x ∀z (∃y P(x,y) ∧ ∃y Q(z,y) )
∀x ∀z (∃y P(x,y) ∧ ∃w Q(z,w) )
35
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
VARIABLES LIBRES / LIEES (4)
Exemple
Soit F : x < y ⇒ ∀x (x = y ∨ ∃y y < x)

Les variables x et y sont à la fois libres et liées. Il vaut mieux

renommer les variables libres:

F : t < z ⇒ ∀x (x = z ∨ ∃y y < x)

36
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
CALCUL DES PREDICATS
Interprétation en LP1 I = { D, Iv, If, Ip }
Domaine d'interprétation : D = {valeurs que peuvent prendre les
termes}
Interprétation des variables Iv : application qui assure une valeur à
toute variable
Interprétation des fonctions If : application qui associe à toute fonction
d'arité n et à tout n-uplet de termes une valeur dans le domaine
d'interprétation
Interprétation des prédicats Ip : application qui associe à tout prédicat
d'arité n et à tout n-uplet de termes une valeur de vérité

Calcul des prédicats

∀x (P) vrai ssi P est vraie pour toute interprétation Iv(x)

∀
∃x (P) vrai ssi il existe une interprétation Iv(x) tq P est vraie

∃

Corollaire ¬∀ A ≡ ∃x ¬A
¬∀x ¬ ∃ x A ≡ ∀x ¬ A
37
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
FORMULES UNIVERSELLES

Une formule où les quantificateurs (∀ et ∃) apparaissent tous en tête

est dite prénexe
Une formule universelle (resp. existentielle) est une formule
prénexe close dont les seuls quantificateurs sont universels (resp.
existentiels)
Exemples :
• ∀x ∀y ∀z enfant(x,y) ∧ enfant(y,z) ⇒ petit_enfant(x,z)
est une formule universelle
•∀x enfant(x,y) ∧ ∃z enfant(x,z)
n'est pas une formule universelle, ni existentielle

38
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
CLAUSES

 Une clause est une formule universelle dont les sous-formules

non quantifiées sont des littéraux ou des disjonctions de littéraux.
Une clause (en calcul des prédicats) a donc pour forme générale
∀x1,... , ∀ xn a1 ∨ .. ∨ ap ∨ ¬b1 ∨ .. ∨ ¬bq
Exemple : ∀x homme(x) ∨ femme(x) ∨ ¬humain(x).
Cette clause correspond à la formule
∀x humain(x) ⇒ (homme(x) ∨ femme(x))
 La clause vide, notée □ , ne contient aucun littéral : elle est toujours
fausse

39
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
SUBSTITUTION (1)

Substitution
On appelle substitution toute application σ de l'ensemble des variables V
vers l'ensemble des termes T :
σ : V ---------> T
x --------> σ(x) = nom_fonct(terme1, ..., terme n)
σ (x) = Constante
σ (x) = variable

Substituée d’une fbf

Soit f une fbf de LP1. On appelle substituée de f par une substitution
σ = [x → σ(x)] la fbf obtenue par remplacement de toute occurrence de la
variable x dans f par le terme substitué σ(x). Par extension, on note σ(f) la
substituée.
Remarque :
L’écriture : σ = [x → σ(x)] peut être écrite : σ = {x / σ(x)}
40
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
SUBSTITUTION (2)
Composition de substitution :
Soit : θ = {x1/t1, x2/t2, ..., xn/tn} et σ ={y1/u1, y2/u2, ..., ym/um}

la composition de deux substitutions θ et σ, notée µ = σ o θ, est obtenue
en 4 étapes
1. appliquer σ aux termes de θ
θ={x1/ σ(t1), x2/ σ(t2), ..., xn/ σ(tn)}
2. retirer de σ les couples yi /ui tel que : yi ϵ {x1, x2, ..., xn} (yi est une
variable de θ)
3. retirer de θ les couples xj / σ(tj) tel que : xj = σ(tj)
4. rassembler les couples obtenues en 1 et 2 (µ = θ U σ)

Exemple : θ = {x/f(y), y/z} et σ = {x/A , y/B , z/y}
1. la première étape donne θ= {x/f(B), y/y}
2. la deuxième donne σ= {z/y}
3. la troisième donne θ = {x/f(B)}
4. la quatrième étape donne µ = {x/f(B), z/y}
41
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
SUBSTITUTION (3)

Substitutions interdites :
• Constante / ?
• x / f(x)
• fonction / ?

La composition est associative et possède un élément neutre
(substitution vide notée ?)

Couple de désaccord : Le couple de désaccord D(t1, t2) entre deux
termes t1 et t2 est le couple le plus à gauche et ne débutant pas par un
symbole identique.
Exemple :
• t1 = f(g(u), z) ; t2 = f(g(h(t)), r(a)) -----> D1(t1,t2) ={u, h(t) }
• w1 = P(x, g(x), f(x, y)) ; w2=P(x, g(x), f(g(T,y), z))
-----> D(w1,w2) = {x, g(T,y)}

42
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
UNIFICATION (1)

Unification de deux fbf
Deux termes t1 et t2 sont dits unifiables (1) s'il existe une substitution σ (2)
telle que σ(t1) = σ(t2). L’ensemble σ = {x / σ(x)} est appelé : l’unificateur
Exemples
• S1 ≡ P(x) ∨ R(A) ; S2 ≡ P(B) ∨ R(y) ; S1 et S2 sont unifiables.
(1) Un unificateur est : σ= [x → B , y → A] ou bien on écrit σ= {x / B , y / A}
(2) σ(S1)= σ(S2)= P(B) ∨ R(A)
• S1 ≡ P(x) ∨ R(A) ; S2 ≡ P(B) ∨ R(B) ; S1 et S2 sont non unifiables.
(1) l’unificateur n’existe pas pour S1 et S2

Une substitution σ unifie un ensemble de clauses E = {C1, ... , Cn} si
σ(C1) = ... = σ(Cn)
Exemple
σ={x/f(A) , y/A} unifie {C1, C2} , C1=P(A,x), C2=P(A,f(y))}
σ(C1) = P(A,f(A)) ; σ(C2) = P(A,f(A)) donc σ(C1) = σ(C2)
43
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
UNIFICATION (2)

l'unificateur le plus général : l'unificateur le plus général d'un ensemble

de clauses E est un unificateur σ de E tel que pour tout autre unificateur
µ de E, il existe une substitution S telle que µ = S o σ

Terme T1 Terme T2 substitution unificateur

R(x,g(C,z)) R(f(y),g(y,k(x))) S1={x/f(y)} σ1=S1 o σ0 ={x/f(y)}

R(f(y),g(C,z)) R(f(y),g(y,k(f(y)))) S2={y/C} σ2=S2 o σ1 ={x/f(C), y/C}

σ3=S3 o σ2
R(f(C),g(C,z)) R(f(C),g(C, k(f(C)) ) S3={z/k(f(C))}
={x/f(C), y/C, z/k(f(C))}

R(f(C),g(C,k(f(C)))) = R(f(C),g(C,k(f(C))))

44
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
UNIFICATION (3)
Unification : algorithme
• Soient deux termes t1 et t2. L'algorithme qui suit cherche l'unificateur σ s'il existe.

1) S0 = {} ; k = 0

2) SI ( Sk(t1) = Sk(t2) ) alors σ = Sk ; fin avec succès

Sinon Calculer D( Sk(t1), Sk(t2) )
3) SI il existe D( Sk(t1), Sk(t2) ) Soit {d1, d2} alors

SI (d1 est une variable) et (d2 est un terme ne contenant pas d1) alors

Sk+1 = {d1 / d2} o Sk

K= k + 1 ; Aller à l’étape 2

SI (d2 est une variable) et (d1 est un terme ne contenant pas d2) alors

Sk+1 = { d2 / d1} o Sk

K= k + 1 ; Aller à l’étape 2

Sinon « Echec » (t1 et t2 sont non unifiables)

45
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
UNIFICATION (4)
Remarques
• Deux termes ne sont pas toujours unifiables. Exp: f(A), f(B).
• Deux termes peuvent avoir une infinité d'unificateurs, mais il existe un qui est le plus
général (donné par l'algorithme).
• x et f(x) donne une boucle infini.
Exemple 1 : Dérouler l'algorithme pour l'exemple:
t1 = f(g(u), z) ; t2 = f(g(h(t)), r(A))
1) S0 = {} ; k=0
2) D = {u,h(t))
3) S1 = { u/h(t) } o S0 = { u/h(t)}
S1(t1)= f(g(h(t)), z) , S1(t2)= f(g(h(t)), r(A))
4) D = {z, r(A)}
5) S2 = { z/r(A) } o S1 = { u/h(t), z/r(A) }
S2(t1)= f(g(h(t)), r(A)) , S2(t2)= f(g(h(t)), r(A))
6) S2(t1)= S2(t2)
donc t1 et t2 sont unifiables. Et l’unificateur σ = S2= {u/h(t), z/r(A) }
46
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
UNIFICATION (5)
Exemple 2 :
t1 = P(A,x,f(g(y))), t2= P(z,f(z),f(u))
1. S0 = {} ; k = 0 ;
2. D = {A,z} avec z variable et A terme ne contenant pas z ;
3. S1 = {z / A} ᴼ S0 = {z / A}
S1(t1) = P(A,x,f(g(y))), S1(t2) = P(A,f(A),f(u))
4. D = {x,f(A)}, x variable et f(A) terme ne contenant pas x ;
5. S2 = {x / f(A)} ᴼ S1= {x / f(A)} ᴼ {z/ A} = {x/f(A), z/A}
S2(t1) = P(A,f(A),f(g(y))), S2(t2) = P(A,f(A),f(u))
6. D = {g(y), u}, u variable et g(y) terme ne contenant pas u ;
7. S3 = {u/g(y)} ᴼ S2 = {u/g(y), x/f(A), z/A}
S3(t1) = P(A,f(A),f(g(y))) S3(t2) = P(A,f(A),f(g(y)))
8. S3(t1) = S3(t2) ==> S3 est l'upg de t1 et t2
donc t1 et t2 sont unifiables. Et l’unificateur σ = S3= {u/g(y), x/f(A), z/A}
47
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
RESOLUTION (1)
Même principe qu’en LP, mais il faut ici faire l’unification des clauses pour
pouvoir les identifier lors de l’application de la règle de résolution

Règle de résolution en LP1

Soient F1 et F2 deux clauses quelconques de LP1. On dit que F1 et F2
forment une paire résolvable ssi elles contiennent une paire opposée de
formules atomiques ayant pour forme respective P(t1, ..., tn) et ¬P(t'1,...,t'n)
et qui peuvent être unifiées par un unificateur σ.
On appelle alors résolvante de F1 et F2, la clause :
res(F1, F2) = σ(F1 \ {P} ) ∪ σ(F2 \ {¬
¬P} )
Exemple
S1 ≡ Animal(x) ∨ Manger(g(x), x) S2 ≡ ¬ Manger(u,v) ∨ ¬ Tuer(u,v)
u / g(x) ,
v/x

unificateur : σ={u/g(x),v/x} résolvante : R ≡ Animal(x) ∨ ¬ Tuer(g(x),x)

48
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
RESOLUTION (2)
Principe de résolution (Robinson 65)

En utilisant la résolution et l'unification nous pouvons montrer que
l'ensemble { C1, C2, ...Cn, Non D) est inconsistant ( par la déduction
d'une contradiction).

Si l'ensemble des clauses est inconsistant, la résolution et l'unification
génère toujours la clause vide( Complétude).
Algorithme général de résolution
• Soit à démontrer C1, C2, ...., Cn╞ But (C1, C2, ...,Cn et but sont des
clauses.
1. A0 ={C1, C2, ...Cn}U{ Non but}
2. Ai+1 = Ai U {Toutes les résolvantes de clauses prises dans Ai}
3. SI ( Ai+1 contient la clause vide ) alors Arrêt, (But est une conséquence
logique de C1,…,Cn )
4. Si ( Ai+1 = Ai ) alors Arrêt, (But n'est pas une conséquence logique de
C1,…,Cn)
5. Aller a l’étape 2
49
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
FORME NORMALE CONJONCTIVE (1)

Transformation en CNF
1. Élimination des implications et des équivalences
2. Réécriture en forme prénexe (mettre les quantificateurs en début)
3. Skolémisation (suppression du ∃)
4. Suppression des quantificateurs universels (∀)
5. Distribution de ∨ sur ∧

Exemple:
∀x(∀y Animal(y)⇒Manger(x,y)) ⇒ (∃yManger (y,x))

50
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
FORME NORMALE CONJONCTIVE (2)
1. Elimination des implications et des équivalences
Comme en logique propositionnelle :

P ⇔ Q ≡ (P ⇒ Q) ∧ (Q ⇒ P)

P ⇒ Q ≡ ¬P ∨ Q

¬ ∀x P ≡ ∃x ¬P

¬ ∃x P ≡ ∀x ¬P

∀x(∀y Animal(y)⇒Manger(x,y)) ⇒ (∃yManger(y,x))

∀x(∀y¬Animal(y)∨Manger(x,y)) ⇒ (∃yManger(y,x))
∀x(¬ (∀y¬Animal(y) ∨ Manger(x,y)) ∨(∃yManger(y,x))
∀x(∃y ¬ (¬Animal(y) ∨ Manger(x,y))) ∨(∃yManger(y,x))
∀x(∃y Animal(y) ∧ ¬ Manger(x,y)) ∨ (∃yManger(y,x))

51
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
FORME NORMALE CONJONCTIVE (3)
2. Mettre sous forme prénexe
Définition : Une formule G est dite en forme prénexe ssi elle est de la
forme Q1x1 … Qnxn A, où chaque Qi est un quantificateur ∀ ou ∃ et A ne
contient pas de quantificateur.
Théorème : Pour toute formule G il existe une formule G0 en forme
prénexe t.q G≡G0.
Pour cela on utilise les équivalences suivantes :

(∀x A) ∨ B ≡ ∀x (A ∨ B) ssi x n’est pas liée dans B

(∃x A) ∨ B ≡ ∃x (A ∨ B) ssi x n’est pas liée dans B

(∀x A) ∧ B ≡ ∀x (A ∧ B) ssi x n’est pas liée dans B

(∃x A) ∧ B ≡ ∃x (A ∧ B) ssi x n’est pas liée dans B

Remarque :
Si x est liée dans B alors il faut renommer x avec une substitution

52
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
FORME NORMALE CONJONCTIVE (4)

2. Mettre sous forme prénexe (suite)

∀x(∃
∃y Animal(y) ∧ ¬ Manger(x,y)) ∨(∃
∃y Manger(y,x))
∀x(∃
∃y Animal(y) ∧ ¬ Manger(x,y)) ∨(∃
∃z Manger(z,x))
∀x(∃
∃y Animal(y) ∧ ¬ Manger(x,y)) ∨(∃
∃z Manger(z,x))
∀x∃
∃y∃∃z (Animal(y) ∧ ¬ Manger(x,y)) ∨ Manger(z,x)

53
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
FORME NORMALE CONJONCTIVE (5)
3. Skolémisation
Définition
Il s’agit de remplacer les variables quantifiées existentiellement
• par une constante si la variable est dans la portée d'aucune autre
quantification universelle.
• par une fonction f(x1, ... , xn) où les xi sont les variables quantifiées
universellement précédant la variable quantifiées existentiellement.
(f est appelé fonction de Skolem).
Exemples :
∃x∀yA(x,y) devient ∀yA(B,y) (remplacé par la constante B).
∀y∃xA(x,y) devient ∀yA(f(y),y) (remplacé par la fonction f(y).
Attention:
Les deux formules ne sont pas équivalentes. mais si on déduit G de la
première alors on peut la déduire de la seconde.
54
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
FORME NORMALE CONJONCTIVE (6)

3. Skolémisation (suite)

∀x∃
∃y∃∃z (Animal(y) ∧ ¬ Manger(x,y)) ∨ Manger(z,x)
∀x∃
∃y (Animal(y) ∧ ¬ Manger(x,y)) ∨ Manger(g(x),x)
∀x∃
∃y (Animal(y) ∧ ¬ Manger(x,y)) ∨ Manger(g(x),x)
∀x (Animal(f(x)) ∧ ¬ Manger(x,f(x))) ∨ Manger(g(x),x)

4. Suppression des quantificateurs universels

Comme toutes les variables sont maintenant universellement
quantifiées on peut supprimer les ∀ (ils deviennent implicites).

(Animal(f(x)) ∧ ¬ Manger(x,f(x))) ∨ Manger(g(x),x)

55
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
FORME NORMALE CONJONCTIVE (7)

4. Distribution de ∨ sur ∧
Comme pour la logique des propositions :

(P ∧ Q) ∨ R ≡ (P ∨ R) ∧ (Q ∨ R)

(Animal(f(x)) ∧ ¬ Manger(x,f(x))) ∨ Manger(g(x),x)

(Animal(f(x)) ∨ Manger(g(x),x)) ∧ (¬
¬ Manger(x,f(x)) ∨ Manger(g(x),x))

La formule est en FNC. Elle comporte deux clauses :

(Animal(f(x)) ∨ Manger(g(x),x))
¬ Manger(x,f(x)) ∨ Manger(g(x),x))

(¬

56
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
EXEMPLE DE RÉSOLUTION

Faits

Pour tout crime, il y a quelqu’un qui l’a commis.

Seuls les malhonnêtes commettent des crimes.

Ne sont arrêtés que les gens malhonnêtes.

Les gens malhonnêtes arrêtés ne commettent pas de crimes.

Il y a des crimes.
Question

Il y a des gens malhonnêtes non arrêtés.
Codage en prédicats

x est un crime : Crime(x).

x a commis y : Commis(x,y).

x est malhonnête : Malhonnete(x).

x est arrêté : arrete(x).

57
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
EXEMPLE DE RÉSOLUTION

Faits

Pour tout crime, il y a quelqu’un qui l’a commis.
∀x (Crime(x) ⇒ ∃y Commis(y,x)). (F1)

Seuls les malhonnêtes commettent des crimes.
∀x ∀y(Crime(x) ∧ Commis(y,x) ⇒ Malhonnete(y)). (F2)

Ne sont arrêtés que les gens malhonnêtes.
∀x(Arrete(x) ⇒ Malhonnete(x)). (F3)

Les gens malhonnêtes arrêtés ne commettent pas de crimes.
∀x ∀y(Malhonnete(x) ∧ Arrete(x) ∧ Crime(y) ⇒ ¬Commis(x,y)).
(F4)

Il y a des crimes.
∃x(Crime(x)). (F5)

58
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
EXEMPLE DE RÉSOLUTION

But
•Il y a des gens malhonnêtes non arrêtés.
•∃x(Malhonnete(x) ∧ ¬Arrete(x)), (Q).
•∀
∀x(¬
¬(Malhonnete(x) ∧ ¬Arrete(x))), (¬
¬Q).

On cherche à montrer
{F1, F2, F3, F4, F5, ¬Q} ╞ □

59
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
EXEMPLE DE RÉSOLUTION

Traduction en FNC (F1)
Pour tout crime, il y a quelqu’un qui l’a commis.
∀x (Crime(x) ⇒ ∃y Commis(y,x)). (F1)
∀x∃y(¬Crime(x) ∨ Commis(y,x)).
∀x(¬Crime(x) ∨ Commis(f(x),x)).
¬Crime(x) ∨ Commis(f(x),x). (F1)

Traduction en FNC (F2)

Seuls les malhonnêtes commettent des crimes.
∀x ∀y(Crime(x) ∧ Commis(y,x) ⇒ Malhonnete(y)). (F2)
∀x ∀y(¬(Crime(x) ∧ Commis(y,x)) ∨ Malhonnete(y)).
(¬
¬Crime(x) ∨ ¬Commis(y,x) ∨ Malhonnete(y)). (F2)

60
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
EXEMPLE DE RÉSOLUTION

Traduction en FNC (F3)
Ne sont arrêtés que les gens malhonnêtes.
∀x(Arrete(x) ⇒ Malhonnete(x)). (F3)
∀x(¬Arrete(x) ∨ Malhonnete(x)).
¬ Arrete(x) ∨ Malhonnete(x). (F3).

Traduction en FNC (F4)

Les gens malhonnêtes arrêtés ne commettent pas de crimes.
∀x ∀y(Malhonnete(x) ∧ Arrete(x) ∧ Crime(y) ⇒ ¬Commis(x,y)). (F4)
∀x ∀y(¬(Malhonnete(x) ∧ Arrete(x) ∧ Crime(y)) ∨ ¬Commis(x,y)).
∀x ∀y(¬Malhonnete(x) ∨ ¬Arrete(x) ∨ ¬Crime(y) ∨ ¬Commis(x,y)).
(¬
¬Malhonnete(x) ∨ ¬Arrete(x) ∨ ¬Crime(y) ∨ ¬Commis(x,y)). (F4).

61
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
EXEMPLE DE RÉSOLUTION

Traduction en FNC (F5)

Il y a des crimes.
∃x(Crime(x)). (F5)
(Crime(C1)). (F5).

Traduction en CNF
Il y a des gens malhonnêtes non arrêtés.
∀x(¬(Malhonnete(x) ∧ ¬Arrete(x))), (¬Q)
∀x(¬Malhonnete(x) ∨ Arrete(x))
¬Malhonnete(x) ∨ Arrete(x) (¬
¬Q)

62
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
EXEMPLE DE RÉSOLUTION

¬Crime(x) ∨ Commis(f (x),x). (F1)

¬Crime(x) ∨ ¬Commis(y,x) ∨ Malhonnete(y). (F2)

¬ Arrete(x) ∨ Malhonnete(x). (F3)

¬Malhonnete(x) ∨ ¬ Arrete(x) ∨ ¬Crime(y) ∨ ¬Commis(x,y). (F4)

Crime(C1). (F5)

¬Malhonnete(x) ∨ Arrete(x). (¬Q)

F1,F5 avec σ = {x / C1}.

¬Crime(C1) ∨ Commis(f(C1),C1) ∨ Crime(C1)
F6 : Commis(f (C1),C1)

F2, F6 avec σ = {x/C1, y/f(C1)}.
¬Crime(C1) ∨ ¬Commis(f(C1),C1) ∨ Malhonnete(f(C1)) ∨ Commis(f (C1),C1)
F7 : ¬Crime(C1) ∨ Malhonnete(f(C1))

F7 , ¬Q avec σ = {x/f(C1) }.
¬Malhonnete(f(C1)) ∨ Arrete(f (C1)) ∨ ¬Crime(C1) ∨ Malhonnete(f(C1))
F8 : Arrete(f(C1)) ∨ ¬Crime(C1)

F8,F5 avec σ = {}
Arrete(f(C1)) ∨ ¬Crime(C1) ∨ Crime(C1)
F9 : Arrete(f(C1))
63
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
EXEMPLE DE RÉSOLUTION

F9,F3 avec σ = {x / f(C1)}

¬Arrete(f(C1)) ∨ Malhonnete(f(C1)) ∨ Arrete(f(C1))
F10 : Malhonnete(f(C1)).

F10,F4 avec σ = {x / f(C1)}

¬Malhonnete(x) ∨ ¬Arrete(x) ∨ ¬Crime(y) ∨ ¬Commis(x,y) ∨ Malhonnete(f(C1))
F11 : ¬Arrete(x) ∨ ¬Crime(y) ∨ ¬Commis(x,y).

F11,F6 avec σ = {x / f(C1), y / C1}

¬ Arrete(f(C1)) ∨ ¬Crime(C1) ∨ ¬Commis(f(C1),C1) ∨ Commis(f(C1),C1)
F12 : ¬Arrete(f(C1)) ∨ ¬Crime(C1).

F12,F5 avec σ ={}

¬Arrete(f(C1)) ∨ ¬Crime(C1) ∨ Crime(C1)
F13 : ¬Arrete(f(C1)).

F13,F9 avec σ = {}
¬Arrete(f(C1)) ∨ Arrete(f(C1))
□ (clause vide)
64
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
CLAUSES DE HORN (1)

Une clause de Horn est une clause comportant au plus un littéral

positif. Une clause de Horn a donc pour forme générale:
ܽ∨¬ܾ1∨⋯∨¬ܾm
Où ܾ݅ sont des atomes. Une clause de Horn peut également s'écrire:
ܾ1∧⋯∧ܾ‫ܽ⇒ݍ‬
Exemple
•(￢P(x)∨￢B ∨C) est une clause de Horn
•(￢C ∨P1,2 ∨P2,1) n’est pas une clause de Horn
•‫ݔ(݁ݎ݁݌‬,‫ݕ(݁ݎ݁݌ ∨ )ݕ‬,‫ݔ(݁ݎ݁݌_݀݊ܽݎ݃¬ ∨ )ݖ‬,‫ )ݖ‬n’est une clause de
Horn

Les seules formules pouvant être écrites en Prolog sont des
clauses de Horn.

65
 LOGIQUE DES PRÉDICATS DU 1ER ORDRE
CLAUSES DE HORN (2)

Une clause de Horn est une clause possédant au plus un littéral positif.
Faits : pas de littéral négatif
P(x,y,f(x,z))
Règles : un littéral positif et au moins un littéral négatif
P(x, y, f(x, z)) ∨ ¬ Q(x, y) ∨ ¬ R(y, z)
Questions : pas de littéral positif
¬ Q(x, y) ∨ ¬ R(y, z)

66