Logique mathématique

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Langage

Termes

Atome

Quanticateur

Formules bien form ees

Quanticateur

Avec P(x) autre P(a), (b)..., on a :

xP(x) donne proposition vrai pour toutes les valeurs x du domaine

xP(x) donne proposition vrai pour au moins une valeur x du

domaine

D enition (Port e de quanticateur)

On d enit la port ee dun quanticateur comme etant la formule `a la

quelle il sapplique

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(13/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Langage

Termes

Atome

Quanticateur

Formules bien form ees

Formules bien form ees (fbf)

D enition

Les formules bien form ees (fbf) sont deni par :

toute formule atomique est une formule.

si et sont des formules, alors ( ), ( ), ( ' ),

( ( ) et ( ) sont des formules.

si est une formule et si x est une variable quelconque alors (x)( )

est une formule, on dit que est la port e du quanticateur x

si est une formule et si x est une variable quelconque alors (x)( )

est une formule, on dit que est la port e du quanticateur x

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(14/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Exemple 1

Exemple 2

Tout le monde aime quelquun

symbole de variable : x et y

symbole de pr edicat : aime(x, y ) : x aime y

Domaine de x est lensemble des etres humain de m eme pour y

Domaine de pr edicat : couple des ensembles humain

Repr esentation : xyaime(x, y )

il y a des gens qui sont aim es de tous

Symbole de pr edicat : aime(x,y)

Repr esentation : y xaime(x, y )

Rque : inverser lordre de quanticateurs, on a dux phrases

s emantiquement di erentes

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(15/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Exemple 1

Exemple 2

On consid`ere les symboles de pr edicats suivants :

C(x) pour x est une cigarette, P(x) pour x est brun,

B(x) pour x est blond, F(x) pour x est fumeur,

R(x,y) pour x fume y et N(x) pour x est nocive

1

Il y a des cigarettes brunes et il y a des cigarettes blondes.

x(C (x) ' P(x)) ' y (C (y ) ' B(y ))

2 Toutes les cigarettes sont nocives.

x(C (x) N(x))

3 Les seules cigarettes nocives sont les blondes

x((N(x) ' C (x)) B(x))

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(16/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Exemple 1

Exemple 2

1 Certains fumeurs fument des cigarettes brunes, mais pas de

cigarettes blondes.

x(F (x) ' (y (C (y ) ' P(y ) ' R(x, y ))) ' (z((C (z) ' B(z))

R(x, z))))

Certains fumeurs fument des cigarettes brunes, mais pas de

cigarettes blondes veut dire quil existe (au moins) un individu x qui

est un fumeur tels quil existe des individus (des objets) y tels que

ces y sont des cigarettes, brunes, que x fume, mais que pour tout

individu (pour tout objet) z, si z est une cigarette blonde, alors x ne

fume pas z.

2

Il y a des fumeurs qui ne fument que des cigarettes blondes

x(F (x) ' (y (R(x, y ) C (y ) ' B(y ))))

On peut observer qu`a chaque fois le quanticateur existentiel va

avec la conjonction tandis que le quanticateur universel va avec

limplication

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(17/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Interpr etation

Valeur de v erit e

Tautologie, insatisable et satisable

Interpr etation

Logique des propositions : linterpr etation dune formule consiste `a

aecter une valuation aux di erents symboles propositionnels de

cette formule

Logique des pr edicats : une interpr etation donne un sens aux

variables (individus), aux fonctions et aux relations

D enition

Une interpr etation dune formule est la donn ee :

dun domaine (ensemble non vide) D

dune aectation dun el eement de D `a chaque constante

dune aectation dune fonction I(f) de D n I (f )

de fonction n-aire

dune aectation dune relation I(r) de D n I (r )

symbole de pr edicat n-aire

{V , F } `a chaque

D `a chaque symbole

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(18/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Interpr etation

Valeur de v erit e

Tautologie, insatisable et satisable

Exemple

Exemple dinterpr etation : F = {s}, C = {a}, R = {plus grand}

Une interpr etation possible est de prendre :

les r eels R comme domaine

La valeur associ ee `a a est la constante 0 de R

La fonction associ ee `a s est x x + 1

linterpr etation de plus grand est >

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(19/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Interpr etation

Valeur de v erit e

Tautologie, insatisable et satisable

Valeur de v erit e dune fbf pour une interpr etation I

D enition

Pour toute interpr etation dune formule dans un domaine D, est

evalu ee a V ou F selon les regles :

si on conna 1t la valeur de v erit e de et alors la valeur de v erit e

des formules , ' , ( , et est obtenue

conform ement aux r`egles vues au chapitre pr ec edent (CPO).

(x)( ) est evalu e a V si est evalu ee a V pour tout el ement du

domaine D sinon elle est evalu ee `a F .

(x)( ) est evalu e a V si est evalu ee a V pour au moins un

el ement du domaine D sinon elle est evalu ee `a F .

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(20/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Interpr etation

Valeur de v erit e

Tautologie, insatisable et satisable

Exemple 1

Consid erons les formules xP(x) et x P(x) D = {1, 2} Aectation

pour P : P(1) = V , P(2) = F

xP(x) est fausse dans cette interpr etation puisque P(x) nest pas

vraie pour les deux el ements de D

x P(x) est vraie dans cette interpr etation puisquil existe un

el ement de D (x = 2) tel que la formule est vraie.

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(21/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Interpr etation

Valeur de v erit e

Tautologie, insatisable et satisable

Exemple 2

Consid erons la formule : xyP(x, y ) Soit I linterpr etation D = {1, 2}

P(1, 1) = V , P(1, 2) = F , P(2, 1) = F , P(2, 2) = V

Si (x = 1)(y = 1) tq P(1, y ) est vraie

Si (x = 2)(y = 2) tq P(2, y ) est vraie

donc xyP(x, y ) est vraie pour I

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(22/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Interpr etation

Valeur de v erit e

Tautologie, insatisable et satisable

Exemple 3

Consid erons la formule : x(P(x) Q(f (x), a))

Soit I linterpr etation

D = {1, 2}

a = 1, f (1) = 2, f (2) = 1

P(1) = F , P(2) = V , Q(1, 2) = V , Q(2, 1) = F , Q(2, 2) = V ,

Q(1, 1) = V

Si x =1 alors P(x) Q(f (x), a) a P(1) Q(f (1), a)

a P(1) Q(2, 1)

a F F a V

Si x =2 alors P(x) Q(f (x), a) a P(2) Q(f (2), a)

a P(2) Q(1, 1)

a V V a V

puisque P(x) Q(f (x), a) est vraie x D alors est vraie.

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(23/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Interpr etation

Valeur de v erit e

Tautologie, insatisable et satisable

Tautologie, insatisable et satisable

D enition

Une formule est satisable ssi il existe une interpr etation I telle que

est evalu ee a V dans I . I est dit modele de et I satisfait .

D enition

Une formule est insatisable ssi il nexiste aucune interpr etation

satisfaisant .

D enition

Une formule est valide ssi chaque interpr etation I de satisfait .

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(24/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Cons equence logique

Formules equivalentes

Cons equence logique

D enition

Une formule est une cons equence logique des formules 1; 2; ...; n ssi

pour chaque interpr etation I , si 1; 2; ...; n est vraie dans I alors est

aussi vraie dans I .

Rque : Dans le calcul des pr edicats il y a en g en eral une innit e de

domaine et un nombre inni dinterpr etations. On ne peut donc pas

v erier la validit e ou linsatisabilit e dune formule en l evaluant dans

toutes ses interpr etations possible.

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(25/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Cons equence logique

Formules equivalentes

Formules equivalentes

D enition

Deux formules sont equivalentes quand elles ont m eme valeur dans toutes

interpr etation (notation A a B).

On a imm ediatement A a B ssi A B est valide.

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(26/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Cons equence logique

Formules equivalentes

Formules equivalentes

Soient A(x) et B(x) deux formules atomiques bien formees.

Les formules equivalentes de la logique des propositions demeurent

equivalentes en logique des predicats.

xA(x) ' xB(x) a x(A(x) ' B(x))

xA(x) ( xB(x) a x(A(x) ( B(x))

(xA(x)) a x A(x)

(xA(x)) a x A(x)

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(27/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Normalisation et R esolution

Lapplication de r`egles dinf erence telles que le principe de r esolution

exige la mise en forme normale des formules :

Forme pr enexe

Forme standard de Skolem

Forme clausale

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(28/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Formes pr enexes

D enition

Une formule du CP1 est dite en fnp si elle est de la forme

(Q1x1)(Q2x2)...(Qnxn)(M)

o`u Qi est un quanticateur et M une formule sans quanticateurs.

(Q1x1)(Q2x2)...(Qnxn) est appel e pr exe

(M) est appel ee matrice de

Exemple (Voici des formules en fnp)

xy (p(x, y ) ' q(y ))

xy ( p(x, y ) q(y ))

xy z( q(x, y ) r (z))

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(29/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Algorithme de construction (1/2)

1 Supprimer les connecteurs d equivalence et dimplication par les lois

a '

a (

2 Ramener les signes de n egation imm ediatement avant les atomes

avec les lois

a

( ( ) a '

( ' ) a (

(x ) a x

(x ) a x

3 Renommer les variables si n ecessaire

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(30/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Algorithme de construction (2/2)

4 Ramener les quanticateurs au d ebut de la formule pour obtenir la

fnp en utilisant les lois :

Qx ( a Qx( ( ) ;

Qx ' a Qx( ' ) ;

x ' x a x( ' )

x ( x a x( ( )

Q1x ' Q2x a Q1xQ2z( ' )

Q1x ( Q2x a Q1xQ2z( ( )

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(31/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Exemple

Nous allons construire la forme pr enexe equivalente `a la formule :

x p(x) ' y q(y ) y (p(y ) ' q(y ))

1 (x p(x) ' y q(y )) ( y (p(y ) ' q(y )) (suppression de )

2 (x p(x) ' y q(y )) ( z(p(z) ' q(z)) (renommage des variables)

(x p(x) ( y q(y )) ( z(p(z) ' q(z)) (transfert de la n egation)

3

4 x y z( p(x) ( q(y ) ( (p(z) ' q(z))) (d eplacement des

quanticateurs)

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(32/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Mise sous forme standard de Skolem

D enition

Soit une formule en f.n.p. (Q1x1), ..., (Qnxn)M o`u M est sous forme

f.n.c. Supposons que Qr est un quanticateur existentiel dans le pr exe

(Q1x1), ..., (Qnxn), 1 d r d n.

2

1 Si aucun quanticateurs universel nexiste avant Qr alors on choisit

une constante c di erente de toutes les constantes de M et on

remplace toutes les occurrences de xr par cette constante c dans M

et on supprime (Qr xr ) du pr exe.

si Qs1, ..., Qsm sont des quanticateurs universel apparaissant avant

Qr (1 d s1 < ... < sm < r ), on choisit un symbole de fonction

m-aire f des autres symboles de fonction de M et on remplace

toutes les occurrences de xr par f (xs1, xs2, ..., xsm) et on supprime

(Qr xr ) du pr exe. Apr`es l elimination de tous les quanticateurs, on

obtient la forme standard de Skolem. Les constantes et les fonctions

utilis ees pour remplacer les variables existentielles sont appel ees

fonctions de Skolem.

Le calcul des pr edicats ou CP1

(33/52)

I. MOUAKHER-ABDELMOULA

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Exemples

1 x y z u v wp(x, y , z, u, v , w )

x/a, a est une constante

u/f (y , z)

w /g (y , z, v )

on obtient y z vp(a, y , z, f (y , z), v , g (y , z, v ))

2 x y z(( p(x, y ) ' q(x, z)) ( r (x, y , z))

Il faut transformer la matrice en f.n.c.

x y z(( p(x, y ) ( r (x, y , z)) ' (q(x, z) ( r (x, y , z))

on remplace y par f (x) et z par g (x)

x (( p(x, f (x)) ( r (x, f (x), g (x))) ' (q(x, g (x)) ( r (x, f (x), g (x))))

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(34/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Clauses

D enition

Une clause est une disjonction de n litt eraux (n e 0).

si n = 1, la clause est dite clause unitaire

si n = 0, la clause est dite vide (toujours fausse (cid:3))

si n > 0, la clause est dite n-litt eral.

Exemple

( p(x, f (x)) ( r (x, f (x), g (x))) et (q(x, g (x)) ( r (x, f (x), g (x))) sont

des clauses

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(35/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Forme clausale

Un ensemble S de clauses est consid er e comme la conjonction de

toutes les clauses de S o`u toute les variables sont suppos ees

quanti ees universellement.

Notation : la forme standard de Skolem peut etre repr esent ee par un

ensemble S de clauses.

Exemple

S = {( p(x, f (x)) ( r (x, f (x), g (x))), (q(x, g (x)) ( r (x, f (x), g (x)))}

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(36/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Forme standard de Skolem

Cette transformation (Skol emisation) ne pr eserve que la satisabilit e et

non l equivalence. Elle pr eserve donc linsatisabilit e, elle convient ainsi

aux techniques r efutationnelles.

Proposition

Si s est obtenue par skol emisation `a partir de alors s est satisfaisable

si et seulement si est satisfaisable.

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(37/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Exercice

Consid erons les enonc es suivants :

1 : chaque personne qui epargne de largent gagne des int er ets

2 : sil ny a pas dint er et alors personne n epargne de largent

S(x, y ), M(x), I (x) et E (x, y ) repr esentent respectivement x epargne

y, x est de largent, x est un int er et et x gagne y

1 Symboloser 1 et 2

2 Trouvez les ensembles de clauses associ es `a 1, 2 et 2

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(38/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Exercice - Solution

1 Symbolisation

1 : x(zM(z) ' S(x, z) y I (y ) ' E (x, y ))

2 : (zI (z)) (xy (M(y ) ' S(x, y ))

2 `a terminer

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(39/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Substitution

D enition

Une substitution est un ensemble ni de la forme

{v1/t1, v2/t2, ..., vn/tn} tels que :

vi (1 d i d n) sont des variables distincts

ti (1 d i d n) sont des termes

pour chaque couple vi /ti , ti est di erent de vi .

Elle est d enie comme une fonction dun ensemble ni de variables dans

les termes. Le domaine dune substitution est not ee

dom( ) = {v1, v2, ..., vn}.

Exemple

= {x/y , z/a, w /f (x)}, dom( ) = {x, z, w }

La substitution ne comportant aucun el ement est appel ee

substitution vide not e .

Lorsque tous les ti sont clos, on parle de substitution close.

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(40/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Instance dune expression

D enition

Soit = {v1/t1, v2/t2, ..., vn/tn} une substitution. Soit E une expression.

On appelle instance de lexpression E , not e E une expression obtenue `a

partir de E en rempla cant chaque occurence de vi par le terme ti

Exemple

= {x/a, y /f (b), z/c}, E = {p(x, y , z)}, E = {p(a, f (b), c)}

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(41/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

La composition des substitutions

D enition (La composition des substitutions)

Soit = {x1/t1, x2/t2, ..., xn/tn} et

= {y1/u1, y2/u2, ..., yn/um} deux substitutions. La coposition de et ,

not ee est la substitution obtenue `a partir de lensemble

= {x1/t1 , x2/t2 , ..., xn/tn , y1/u1, y2/u2, ..., yn/um} en eliminant :

chaque el ement xj /tj pour lequel tj = xj

chaque el ement yi /ui tel que yi {x1, ..., xn}

Exemple

= {x/f (y ), y /z}, = {x/a, y /b, z/y } alors = {x/f (b), z/y }

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(42/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Unication

D enition

Une substitution est appel ee unicateur de lensemble {E1, ..., Ek } ssi

E1 = E2 = ... = Ek . Lensemble Ei est dit uniable sil existe un

unicateur

D enition

Une substitution de lensemble {E1, ..., Ek } est dit lunicateur le plus

g en eral (pgu) ssi pour Chaque unicateur de E , il existe une

substitution telle que =

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(43/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Ensemble des di erences

D enition

= {E1, ..., En} 6= , ensemble dexpressions. Lensemble des di erences

(ED( )) associ e a est obtenue en localisant le premier symbole (a

partir de la gauche) dans pour lequel il y a des expression de nayant

pas le m eme symbole puis extrait de chaque expression de la

sous-expression commen cant par le symbole occupant cette position.

Exemple

= {P(x, f (y , z)), P(x, a), P(x, g (h(k(x))))}

ED( ) = {f (y , z), a, g (h(k(x)))}

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(44/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Algorithme dunication

Donn ees Ensemble dexpression E

R esultat Si E est uniable rend pgu de E sinon lalgorithme sarr ete en

d etectant limpossibilit e dunier.

Etape 1 : k 0, k et k (initialisation)

Etape 2 : Si k est un singleton alors k est lunicateur le plus g en eral de

stop

sinon chercher lensemble de di erence Dk ED( k )

Etape 3 : Sil existe vk et tk Dk tels que vk est une variable qui napparait

pas dans tk alors aller `a l etape 4 sinon nest pas uniable stop

Etape 4 : k+1 k {vk /tk }, k+1 = k {vk /tk }

Etape 5 : k k + 1 et aller `a l etape 2

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(45/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Exemple

Unication de = {P(x, f (g (x)), a), P(b, y , z)}

(Initialisation) 0 = {P(x, f (g (x)), a), P(b, y , z)}, 0 =

(k=0) D0 = {x, b}, 1 = {x/b}, 1 = {P(b, f (g (b)), a), P(b, y , z)}

(k=1) D1 = {f (g (b)), y },

2 = {x/b} {y /f (g (b))} = {x/b, y /f (g (b))},

2 = {P(b, f (g (b)), a), P(b, f (g (b)), z)}

(k=2) D2 = {a, z}, 3 = {x/b, y /f (g (b)), z/a},

3 = {P(b, f (g (b)), a), P(b, f (g (b)), a)} a {P(b, f (g (b)), a)}

3 est un singleton alors 3 est lunicateur le plus g en eral de

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(46/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Exemple

Unication de = {P(x, f (x), a), P(u, w , w )}

(Initialisation) 0 = {P(x, f (x), a), P(u, w , w )}, 0 =

(k=0) D0 = {x, u}, 1 = {x/u}, 1 = {P(u, f (u), a), P(u, w , w )}

(k=1) D1 = {f (u), w }, 2 = {x/u, w /f (u)},

2 = {P(u, f (u), a), P(u, f (u), f (u))}

(k=2) D2 = {a, f (u)} : echec car ni a ni f (u) ne sont des variables.

Exemple

Unication de = {P(x, f (x)), P(f (y ), y )}

(Initialisation) 0 = {P(x, f (x)), P(f (y ), y )}, 0 =

(k=0) D0 = {x, f (y )}, 1 = {x/f (y )},

1 = {P(f (y ), f (f (y ))), P(f (y ), y )}

(k=1) D1 = {f (f (y )), y } : echec car y appara 1t dans f (f (y )).

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(47/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

Facteur

D enition

Si deux litt eraux L1 et L2 avec le m eme signe dune clause

C = L1 ( L2 ( C 2 ont un pgu (L1 = L2 ), alors F = L1 ( C 2 est

appel e facteur binaire de C . Un facteur dune clause est le r esultat de

lapplication de (z ero, une ou) plusieurs factorisations sur cette clause.

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(48/52)

Introduction

Syntaxique

Formalisation

S emantique

Cons equence logique et Formules equivalentes

Normalisation et R esolution

Formes pr enexes

Forme standard de Skolem, forme clausale

Substitution et unication

Algorithme dunication

Le principe de r esolution pour le CP1

R esolvant

D enition (R esolvant binaire)

Soient C1 et C2 deux clauses nayant pas de variables communes. Soit L1

un litt eral de C1 et soit L2 un litt eral de C2 si L1 et L2 ont un pgu

alors la clause (C1 \L1 ) * (C2 \L2 ) est appel ee r esolvant binaire de

C1 et C2.

C1=L1(C 2

1 ,C2=L2(C 2

1 (C 2

C 2

2

2

(RR)

D enition (R esolvant)

Un r esolvant des clauses c1 et c2 est lun des r esolvants binaires

suivants :

r esolvant binaire de c1 et c2

r esolvant binaire de c1 et de facteur c2

r esolvant binaire de facteur c1 et de c2

r esolvant binaire de facteur c1 et de facteur c2

I. MOUAKHER-ABDELMOULA

Le calcul des pr edicats ou CP1

(49/52)