Esercizio metodo di risoluzione logica primo ordine

[yoghi871]

Salve stò facendo un esercizio di risoluzione sulla logica al primo ordine ma sapete dirmi perchè la prof nelle soluzioni ha messo queste clausole provenienti da questo pezzo di esercizio:
{notA(w)} {notB(f(x))}

Provenienti da :
∀x∃ynot(A(x) v B(y)

[Lord K]

Non mi è molto chiara la tua domanda... potresti essere più chiaro/a?

[yoghi871]

nel metodo di risoluzione bisogna trovare le clausole, in quell'esempio che ti ho scritto la prof ha dedotto quelle clausole e come le ha dedotte non mi è chiaro...

[adaBTTLS1]

∀x∃ynot(A(x) v B(y))
∀x∃y[(not(A(x)) & not(B(y))]
in corrispondenza di ciascun x esiste almeno un y=f(x) per cui sono false sia A(x) sia B(f(x)).
spero che questa traduzione ti possa aiutare, perché io non conosco la notazione usata da te nella prima riga.
ciao.