Urgent ! Skolémisation, clauses étranges?

[invite62588872]

Bonsoir,

en revoyant les derniers exercices de logique qu'il nous reste avant l'examen, nous sommes tombés sur des clauses incompréhensibles :

On considère les clauses suivantes, dans lesquelles f est une fonction de Skolem.

clause 1 : {.....,anim( f(u)) }
clause 2 : {.....,broll( f(z)) }

Mais pourtant, avant de transformer en clauses, les quantificateurs universels portent sur tout ce qui se trouve à leur droite, donc il est (selon nous) interdit de renommer les variables dans différentes clauses !

Selon nous, il est impossible d'avoir f(u) et f(z) dans 2 clauses différentes .. Ce serait f(u) et g(z), ou f(u) et f(z,w)..

J'espere avoir été assez clair, l'examen est demain et nous sommes 3 dans le kot à nous prendre la tête là-dessus

Merci d'avance pour votre aide !
-----

[Médiat]

Une fonction de Skolem n'est pas une fonction au sens analytique, elle exprime une dépendance, pas un calcul.

Le point qui permet de changer le nom des variables est :

est équivalent à