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)