Skolemizarea

Această intrare sau secțiune pe matematică nu citează sursele necesare sau cele prezente sunt insuficiente. 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ă , skolemizarea este aplicarea algoritmului lui Albert Thoralf Skolem care transformă o propoziție în formă normală într-o propoziție universală. Propoziția în cauză, după aplicarea algoritmului lui Skolem, pierde echivalența semantică cu propoziția inițială. Cu toate acestea, este interesant de observat că satisfacția rămâne neschimbată.

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ă de preness . Cuantificatorii (∀, ∃) trebuie grupați la începutul propoziției. ∀x ₁ ∃x ₂ ∀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 ∀ mergem direct la punctul următor.
   Dacă Q ₁ este ∃ atunci ∃x ₁ este anulat și fiecare apariție a x ₁ în α este înlocuită cu aceeași constantă 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. Revizuiesc Q _n
   • Dacă Q _n este a ∀ începem din 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, totuși, înlocuind la fiecare apariție a variabilei x _n un functor care revizuiește toate variabilele anterior folosit de cuantificatori ∀.
       După cum puteți vedea, până când apar cuantificatori de tip ∀, variabilele x _n sunt înlocuite cu constante 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ță, cuantificatorul ∃ a fost eliminat, iar variabila y a fost înlocuită cu funcționorul g (x).
   Alegerea variabilei x nu este aleatorie, deoarece x ₁ în acest caz este doar 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)

Devine ∀y∀z∃u∀t∃v (α ¹ ) (α ¹ este propoziția noastră după aplicarea substituției)

• 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).

Devine ∀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 (∃), îl șterg și îl înlocuiesc în α ² pentru toate aparițiile v un funcționar care revizuiește toate variabilele utilizate de cuantificatoarele ∀ utilizate 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ă