Quello che devo fare io è applicare l'algoritmo di skolemizzazione.
Devo acquisire una formula in Forma Normale Prenessa (FNP), e trasformarla in una formula in Forma Normale di Skolem (FNS).
Vi riporto direttamente tutto l'algoritmo:
La FNP è una formula in cui i quantificatori compaiono tutti nel prefisso (le FNP e le FNS sono formate da 2 parti: prefisso e matrice)
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.
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.
Gia vi dico che io l'algoritmo l'ho capito e lo saprei applicare (sfortunatamente solo su carta ^_^)
Il mio problema, come vi avevo detto è che ci sono delle parti della stringa che devo eliminare, ma non li si conosce a priori: come potrei fare ?