Algoritmul Skolem

Algoritmul Skolem este un algoritm ce servește la restrângerea unei formule la forma normală Skolem. Pentru aceasta formula trebuie să treacă prin mai multe transformări.

Primul pas în rezolvarea acestor tipuri de exerciții este de a trece formula în forma normală rectificată(FNR). O formulă este în FNR dacă nu conține variabile care sunt atât libere cât și legate și nu are cuantificatori care să lege aceeași variabilă dar pe poziții diferite. O variabilă x este considerată legată dacă apare într-o subformulă G a unei subformule a lui F de forma: H = (∀x)(G) (sau (∃x)(G)). În restul cazurilor apariția considerată este numită liberă.

Fie formula:
F = (∀x)(∃y)(P(x,f(x,y))∧Q(a,y))∨(∀x)P(x,x).

Pentru ca formula F să ajungă la forma normală rectificată trebuie făcute substituții pentru variabilele ce sunt legate de cuantificatori pe poziții diferite.
Substituția necesară se face în cel de-al doilea termen în care x va fi înlocuit cu variabila z. Formula rezultată va fi tare echivalentă cu formula inițială.
Substituția folosită: [x/z].

F' = (∀x)(∃y)(P(x,f(x,y))∧Q(a,y))∨(∀z)P(z,z).

Următorul pas este de a trece formula F' de la forma normală rectificată la forma normală prenex. O formulă din LP1 se află în FNP dacă este de forma: F = (o₁y₁)....(o_ny_n)G unde n∈N, o_i∈{∀, ∃}, iar y₁...y_n sunt toate variabilele care apar în G. În plus G nu mai conține alți cuantificatori.
Tot ce avem de făcut pentru ca această formulă să fie în FNP, este să mutăm cuantificatorul "∀" din ultimul termen în fața formulei.
O problemă ce poate apărea aici este atunci când în formula noastră apare una sau mai multe variabile care nu sunt cuantificate. Atunci acele variabile vor fi cuantificate conform închiderii existențiale, adică apar în fața formulei însoțite de cuantificatorul "∃".
Formula F' va arăta cam așa după ce a fost adusă la forma normală prenex.

F'' = (∀x)(∃y)(∀z)((P(x,f(x,y))∧Q(a,y))∨P(z,z)).
Deoarece formula se afla în FNR, spunem că F'' se află în FNPR(forma normală prenex rectificată).

Următorul pas din algoritmul Skolem este cel de a trece formula rezultată anterior la forma normală Skolem(FNS). O formulă F din LP1 se află în FNS dacă are următorul aspect:
F = (∀x₁) ... (∀x_k)G, unde G nu mai conține alți cuantificatori și x₁ ... x_n sunt exact variabilele care apar în G.

Pentru ca formula de mai sus aflată în FNPR să treacă în FNS aceasta trebuie să conțină doar cuatificatori universali. Se aplică diferite substituții pentru a elimina cuantificatorii existențiali iar formula F'' va arăta cam așa:

F''' = (∀x)(∀z)((P(x,f(x,g(x)))∧Q(a,g(x)))∨P(z,z)).

Ultimul pas este de a aduce formula la FNSC(forma normală Skolem cauzală) adică de a aplica distributivitatea operației "∨" față de "∧". Forma finală a formulei este:

F = (∀x)(∀z)(P(x,f(x,g(x)))∨P(z,z))∧(Q(a,g(x))∨P(z,z))).

Asta este tot cu privire la trecerea unei formule la FNSC folosind algoritmul Skolem.