Forma prenessa e forma di skolem

[crestini]

Salve ragazzi, c'è qualcuno di voi che mi può aiutare con le forme prenesse e forma di skolem? Avrei bisogno di regole sintetiche e chiare sull'argomento! Ho studiato sugli appunti del professore ma sono alquanto confusi! Ho solo capito che per poter scrivere una formula in forma di Skolen devo prima ridurla in forma prenessa, ovvero?

[Pappappero1]

Una formula si dice in forma prenessa quando tutti i quantificatori sono in testa (con variabili quantificate rinominate in modo da essere tutte diverse) e il resto della formula è in CNF (quindi congiunzione di tante disgiunzioni).

Una volta che hai la formula in questa forma, puoi fare i passi di skolem per eliminare tutti i quantificatori esistenziali.

Il risultato è una formula, in qui compaiono solo variabili libere o variabili quantificate da quantificatori universali. In questa forma è facile applicare DPP se si vuole confutare la formula. Viceversa, personalmente, almeno in esempi piccoli, trovo più facile usare la formula con i quantificatori esistenziali se devo trovare un modello, e poi tradurre il modello attraverso le funzioni di skolem per adattarlo alla forma skolemizzata.