Skolemizzazione

Da Wikipedia, l'enciclopedia libera.
Se riscontri problemi nella visualizzazione dei caratteri, clicca qui.

In logica matematica, si dice skolemizzazione l'applicazione dell'algoritmo di 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à.

Una frase α ∈ l (linguaggio) è un enunciato universale se:

  1. α è un enunciato (Non ci sono variabili libere)
  2. α è in forma normale e gli unici quantificatori, se esistono, sono di tipo ∀.

Esempio di enunciati universali.

  • A(b) ∧ C(a)
  • ∀x∀y(A(y) ∧ ⌉C(x))


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[modifica | modifica wikitesto]

  1. Trasformazione in forma normale prenessa I quantificatori (∀,∃) devono essere raggruppati all'inizio della frase. ∀x1∃x2∀x3(...)
  2. Determinare le variabili libere e vincolate. Nella frase non ci devono essere variabili libere, nel caso ci siano è necessario eseguire una sostituzione.
  3. Se Q1 (primo quantificatore) è ∀ si passa direttamente al punto successivo.
    Se Q1 è ∃ allora si cancella ∃x1 e si sostituisce ad ogni occorrenza di x1 in α una stessa costante che non compaia già in α. Esempio: ∃x∀y(A(a, x) ∧ B(b, x,y)) diventa ∀y(A(a, c) ∧ B(b, c,y))
    Come si può facilmente notare si è tolto il quantificatore ∃ e si è sostituita la variabile x con la costante c.
    La scelta della costante c non è casuale visto che "a" e "b" erano già utilizzate.
  4. Prendo in rassegna Qn
    • Se Qn è un ∀ si riparte da questo punto con Qn+1.
    • Se Qn è ∃ allora i casi possono essere i seguenti:
      • Se il quantificatore Qn-1 era di tipo ∃ ovvero ∃xn-1∃xn allora si ripete il punto precedente con ∃xn sostituendo però ad ogni occorrenza della variabile xn 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 xn delle semplici costanti.
      • Se il quantificatore Qn-1 è di tipo ∀ ovvero ∀xn-1∃xn si cancella ∃xn e si sostituisce ogni occorrenza di xn in α con un funtore f() che prenda in rassegna le variabili utilizzate dai quantificatori ∀ che lo precedono. Se fosse ∀y∀z∃u (α) dovrei in primis cancellare ∃u poi sostituire nella frase α la variabile u con il funtore f(y, z) (il funtore non deve esistere già).
    Esempio: ∀x∃y(A(x, f(x), y) ∧ C(y)) diventa ∀x(A(x, f(x), g(x)) ∧ C(g(x)))
    Come si può facilmente notare si è tolto il quantificatore ∃y e si è sostituita la variabile y con il funtore g(x).
    La scelta della variabile x non è casuale visto che x1 in questo caso è proprio x.

Esempio pratico[modifica | modifica wikitesto]

∃x∀y∀z∃u∀t∃v (α)

  • Cancello ∃x e dentro α sostituisco le x con delle costanti (che non siano già state utilizzate)

Diventa ∀y∀z∃u∀t∃v (α1) (α1 è la nostra frase dopo aver applicato la sostituzione)

  • Salto i due quantificatori ∀ e cancello il ∃u ricordando di sostituire ogni occorrenza di u in α1 con un funtore (che non sia stato già utilizzato) che prende in rassegna le variabili utilizzate precedentemente dai quantificatori ∀.Nel nostro caso sarà h(z, y).

Diventa ∀y∀z∀t∃v (α2) (α2 è la nostra frase dopo aver applicato la sostituzione u -> h(z, y))

  • Rimane solo un ultimo quantificatore esistenziale (∃), lo elimino e sostituisco in α2 a tutte le occorrenze di v un funtore che prenda in rassegna tutte le variabili utilizzate dai quantificatori ∀ utilizzati in precedenza. La sostituzione sarà v -> i(y, z,t).

L'algoritmo terminerà quando i quantificatori saranno tutti del tipo ∀.