Discussione:Skolemizzazione

Domanda

Una domanda su questo passo dell'algoritmo di skolemizzazione:

Se il quantificatore Q_n-1 era di tipo ∃ ovvero ∃x_n-1∃x_n allora si ripete il punto precedente con ∃x_n sostituendo però ad ogni occorrenza della variabile x_n 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 x_n delle semplici costanti.

Si dice di analizzare il quantificatore precedente, Q_n-1, e di controllare se è di tipo ∃. Però ( o sbaglio? ) non è possibile che lo sia, in quanto passo a passo tutti i quantificatori ∃ precedenti sono stati sostituiti... Sono io che sbaglio o questo passo sembra non centrare? — Questo commento senza la firma utente è stato inserito da 79.24.168.179 (discussioni · contributi) 20:04, 15 giu 2011 (CEST).