Exercice De Logique Et Deduction

[saf123]

Bonjour je suis en licence informatique et je bloque sur un exercice:

Démontrer le théorème suivant à l’aide de la méthode de résolution de Robinson.

{

Pour tout X.S(X.X) => U(X.X),

Pour tout X, Z. NON (T(Z,F(X)) ET U (Z, F(X))),

Pour tout Y,Z.R(Y,Z) OU S (Y,Z)

}

|- Il existe X, Y.T(X,Y) => R(X,Y)

Un peu d'aide serait la bienvenue^^

Merci!!