Skolemizzazione
Da Wikipedia, l'enciclopedia libera.
La skolemizzazione è la trasformazione di una una formula in una forma detta Forma di Skolem.
Per la skolemizzazione è necessario:
- Trasformare la formula in forma normale prenessa
- Determinare le variabili libere e vincolate
- Sostituire il nome delle variabili vincolate in accordo con il relativo quantificatore che le vincola
- Sostituire le variabili vincolate da quantificatori esistenziali con una costante solo se questo non è preceduto da un quantificatore universale
- Se il quantificatore esistenziale è preceduto da uno universale si sostituiscono le variabili vincolate con un simbolo di funzione