Skolemizzazione
In logica matematica, si dice skolemizzazione l'applicazione dell'algoritmo di Albert Thoralf Skolem che trasforma un enunciato in forma normale in un enunciato universale. L'enunciato in questione, dopo l'applicazione dell'algoritmo di Skolem, perde l'equivalenza semantica con l'enunciato di partenza. È interessante però constatare che rimane invariata la soddisfacibilità[1] (ovvero, preso un qualsiasi enunciato , esiste un modello per se e solo se ne esiste uno per la forma normale di Skolem di ).[2]
Dato un linguaggio , una frase è un enunciato universale se:
- è un enunciato (non ci sono variabili libere)
- è in forma normale e gli unici quantificatori, se esistono, sono di tipo .
Esempio di enunciati universali.
N.B. L'algoritmo di Skolem non mantiene l'equivalenza semantica. La frase risultante dall'applicazione dell'algoritmo di Skolem è soddisfacibile se lo è la frase normale di partenza.
Algoritmo di Skolem
- Trasformazione in forma prenessa. I quantificatori e devono essere raggruppati all'inizio della frase.
- Determinare le variabili libere e vincolate. Nella frase non ci devono essere variabili libere, nel caso ci siano è necessario eseguire una sostituzione.
- Se (primo quantificatore) è si passa direttamente al punto successivo.
Se è allora si cancella e si sostituisce ad ogni occorrenza di in una stessa costante (nota come "costante di Skolem")[2][3] che non compaia già in . Esempio: diventa
Come si può facilmente notare si è tolto il quantificatore e si è sostituita la variabile con la costante .
La scelta della costante non è casuale visto che e erano già utilizzate. - Prendo in rassegna
- Se è un si riparte da questo punto con .
- Se è allora i casi possono essere i seguenti:
- Se il quantificatore era di tipo ovvero allora si ripete il punto precedente con sostituendo però ad ogni occorrenza della variabile un funtore che prenda in rassegna tutte le variabili precedentemente utilizzate dai quantificatori .
Come si può notare finché non appaiono quantificatori di tipo si sostituiscono alle variabili delle semplici costanti. - Se il quantificatore è di tipo ovvero si cancella e si sostituisce ogni occorrenza di in con un funtore che prenda in rassegna le variabili utilizzate dai quantificatori che lo precedono. Se fosse dovrei in primis cancellare poi sostituire nella frase la variabile con il funtore (il funtore non deve esistere già).
- Se il quantificatore era di tipo ovvero allora si ripete il punto precedente con sostituendo però ad ogni occorrenza della variabile un funtore che prenda in rassegna tutte le variabili precedentemente utilizzate dai quantificatori .
Come si può facilmente notare, si è tolto il quantificatore e si è sostituita la variabile con il funtore .
La scelta della variabile non è casuale, visto che in questo caso è proprio .
Esempio pratico
- Cancello e dentro sostituisco le con delle costanti (che non siano già state utilizzate)
Diventa ( è la nostra frase dopo aver applicato la sostituzione)
- Salto i due quantificatori e cancello il ricordando di sostituire ogni occorrenza di in con un funtore (che non sia stato già utilizzato) che prende in rassegna le variabili utilizzate precedentemente dai quantificatori . Nel nostro caso sarà .
Diventa ( è la nostra frase dopo aver applicato la sostituzione )
- Rimane solo un ultimo quantificatore esistenziale, lo elimino e sostituisco in a tutte le occorrenze di un funtore che prenda in rassegna tutte le variabili utilizzate dai quantificatori universali utilizzati in precedenza. La sostituzione sarà .
L'algoritmo terminerà quando i quantificatori saranno tutti del tipo .
Note
- ^ Daniele Nardi, Rappresentazione della Conoscenza - Lezione 2 (PDF), su diag.uniroma1.it, Università degli Studi di Roma "La Sapienza" - Dipartimento di Ingegneria informatica automatica e gestionale Antonio Ruberti, 2008, p. 15. URL consultato il 25 marzo 2022 (archiviato il 25 marzo 2022).
- ^ a b Marco Piastra, Logica del primo ordine: (semi)decidibilità (PDF), su unipv.it, Università degli Studi di Pavia - Computer Vision and Multimedia Laboratory, p. 8. URL consultato il 25 marzo 2022 (archiviato il 25 marzo 2022).
- ^ Paolo Salvaneschi, Inferenza nella logica del primo ordine (PDF), su unibg.it, Università degli Studi di Bergamo - Facoltà di Ingegneria, p. 11. URL consultato il 25 marzo 2022 (archiviato il 23 novembre 2020).
![](http://upload.wikimedia.org/wikipedia/commons/thumb/a/af/Crystal128-kmplot.svg/25px-Crystal128-kmplot.svg.png)