Skolemizarea

Această intrare sau secțiune despre matematică nu citează sursele necesare sau cei prezenți sunt insuficienți . Puteți îmbunătăți această intrare adăugând citate din surse de încredere în conformitate cu liniile directoare privind utilizarea surselor . Urmați sfaturile de proiectare de referință .

În logica matematică , spune Skolem în formă normală , aplicarea algoritmului Thoralf Skolem care transformă o propoziție în formă normală într-o afirmație universală. Propoziția în cauză, după aplicarea algoritmului lui Skolem, pierde echivalența semantică cu propoziția inițială. Este interesant, totuși, să vedem că rămâne neschimbată satisfacția .

O propoziție α ∈ L (limbă) este o propoziție universală dacă:

1. α este o afirmație (Nu există variabile libere)
2. α este în formă normală și singurii cuantificatori, dacă există, sunt de tip ∀.

Exemplu de propoziții universale.

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

NB Algoritmul Skolem nu menține echivalența semantică. Propoziția rezultată din aplicarea algoritmului Skolem este satisfăcătoare dacă propoziția normală de pornire este satisfăcătoare.

Algoritmul lui Skolem

1. Transformarea în formă normală prenex . Cuantificatorii (∀, ∃) trebuie grupați la începutul propoziției. ∀x ∃x _{1 2 3} ∀x (...)
2. Determinați variabilele libere și legate. Nu trebuie să existe variabile libere în propoziție, dacă există, trebuie efectuată o înlocuire.
3. Dacă Q ₁ (primul cuantificator) este ∀ se trece direct la pasul următor.
   Dacă Q ₁ este ∃ atunci ștergeți ∃x ₁ și înlocuiește fiecare apariție a x ₁ α o constantă în sine care nu apare deja în α. Exemplu: ∃x∀y (A (a, x) ∧ B (b, x, y)) devine ∀y (A (a, c) ∧ B (b, c, y))
   După cum puteți vedea cu ușurință, am eliminat cuantificatorul ∃ și am înlocuit variabila x cu constanta c.
   Alegerea constantei c nu este întâmplătoare, deoarece „a” și „b” erau deja utilizate.
4. Voi examina Q _n
   • Dacă Q este un _n ∀ începe de la acest punct cu Q _{n + 1.}
   • Dacă Q _n este atunci ∃ cazurile pot fi următoarele:
     • Dacă cuantificatorul Q _{n-1 a} fost de tip ∃ sau ∃x _n-1 ∃x _n atunci punctul anterior se repetă cu ∃x _n, înlocuind, totuși, pentru fiecare apariție a variabilei x _n un functor care revizuiește toate variabilele utilizate anterior de cuantificatori ∀.
       După cum se poate vedea până când apar cuantificatori ∀ tip de înlocuire a variabilelor x _n ale constantelor simple.
     • Dacă cuantizatorul Q _n-1 este de tip or sau _n-1 ∀x ∃x ∃x _{n n} se șterge și înlocuiește fiecare apariție a lui x _n în α cu un funcțional f () care ia în considerare variabilele utilizate de cuantificatori ∀ care o precedă. Dacă ar fi ∀y∀z∃u (α) ar trebui mai întâi să șterg ∃u apoi să înlocuiesc în propoziția α variabila u cu functorul f (y, z) (functorul nu trebuie să existe deja).
   Exemplu: ∀x∃y (A (x, f (x), y) ∧ C (y)) devine ∀x (A (x, f (x), g (x)) ∧ C (g (x)) )
   După cum puteți vedea cu ușurință, am eliminat cuantificatorul ∃ și am înlocuit variabila y cu functorul g (x).
   Alegerea variabilei aleatoare x nu se vede că x ₁ în acest caz este exact x.

Exemplu practic

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

• Șterg ∃x și în interiorul lui α înlocuiesc x cu constante (care nu au fost deja utilizate)

Deveniți ∀y∀z∃u∀t∃v (α ¹⁾ (α ¹ este propoziția noastră după aplicarea înlocuirii)

• Omit cele două cuantificatoare ∀ și șterg ∃u amintind să înlocuiesc fiecare apariție a lui u în α ¹ cu un functor (care nu a fost deja utilizat) care revizuiește variabilele utilizate anterior de cuantificatorii ∀. În cazul nostru va fi h (z, y).

Deveniți ∀y∀z∀t∃v (α ²⁾ (α ² este propoziția noastră după aplicarea substituției u -> h (z, y))

• Rămâne doar un ultim cuantificator existențial (∃), ștergerea și înlocuirea în α ² a tuturor aparițiilor unui functor v care analizează toate variabilele utilizate de cuantificatorul ∀ utilizat anterior. Înlocuirea va fi v -> i (y, z, t).

Algoritmul se va termina atunci când cuantificatoarele sunt toate de tipul ∀.

Portalul de matematică : accesați intrările Wikipedia care se ocupă de matematică