[LOGICA FOL] Interpretazione di Herbrand

[GlaDos1]

Salve a tutti,
avrei un quesito da portvi. Sto preparando l'esame di logica e negli esercizi sono incappato in questa domanda , ma non so come rispondere.
Considera il linguaggio del primo ordine contenente le due costanti a e b la funzione unaria f e quella binaria g, ed il predicato unario P ed il predicato binario Q:
Dire se esiste un’interpretazione di Herbrand che soddisfa la formula ∀xyP(f(x))∧¬P(g(x, y)).Se si descrivila.

Essendo già in pnf ho fatto la skolemizzazione e ho fatto la sostituzine delle variabili e sono arrivato a questo punto
x->a
y->b
¬P(f(a))∧P(g(a, b)) e qui mi sono bloccato.
Ho inoltre provato a creare un possibile insieme di interpretazione e ho trovato che in un caso esiste , anche se la nella soluzione data dalle slide non dovrebbe esistere.

Help

Grazie dell'attenzione.

[marysax90]

Qual è la soluzione della slide?

Purtroppo ho visto poche applicazioni riguardo la skolemizzazione e formule soddisfacibili o meno.

Vedi se questo link può esserti d'aiuto:
http://homepage.sns.it/lolli/dispense00/corso4.pdf

soprattutto le pagine 85-87.

[GlaDos1]

Grazie per la risposta

Ho consultato il pdf linkato , devo dire che è fatto molto bene, il quale mi ha portato un po' più vicino alla soluzione , ora se ho capito bene posso riportare tutto in clausal normal form , però l'insieme non diventa vuoto quindi è soddisfacibile .
La soluzione sulle slide ahimè consiste solo nella risposta "No.".