4.2. Prenex alakú formulák

Definíció Egy

alakú formulát, ahol a

kvantormentes formula, prenex alakú formulának nevezünk.

a prenex alakú formula magja .

Példa A

, a

és a

formulák prenexformulák, viszont a

formula nem prenexformula.

Tétel Egy elsőrendű logikai nyelv tetszőleges formulájához konstruálható vele logikailag ekvivalens prenex alakú formula.

Definíció Egy formulával ekvivalens prenex alakú formula a formula prenex alakja.

A prenex alakra hozás lépései:

  1. A formulában a kötött változók szabályos átnevezésével elérjük, hogy a kötött változók nevei különbözzenek a formula paramétereitől, és bármely két különböző kvantor más-más változót nevezzen meg a kvantoros előtagban. Az így nyert, az eredeteivel kongruens, így az eredetivel ekvivalens formulát az eredeti változóiban tiszta alakjának nevezzük.

  2. Alkalmazzuk De Morgan kvantoros törvényeit és a kvantorkiemelésre vonatkozó logikai törvényeket, amíg a formulánk prenex alakú nem lesz.

Felhasználható ekvivalenciák:

Table 4.11. kvantoros De Morgan-törvények

Table 4.12. kvantorok egyoldali kiemelése,

Table 4.13. kvantorok kétoldali kiemelése

Table 4.14. kvantorhatáskör-átjelölés,

Példa Hozzuk a

Equation 4.. 


formulát prenexalakra.

  1. Változóiban tiszta alakra hozás:

    Equation 4.. 


  2. De Morgan törvényeinek alkalmazása:

    Equation 4.. 


  3. Kvantorkiemelés:

    Equation 4.. 


  4. Kvantorkiemelés:

    Equation 4.. 


Ha a magot normálformára akarjuk hozni, akkor célszerű előbb eltüntetni az implikációkat, és a negációkat az atomi formulák elé vinni. Ekkor (újabb) lehetőségek adódhatnak a kvantorok kétoldali kiemelésére vonatkozóan.

  1. Az implikációk átírása:

    Equation 4.. 


  2. A kétszeres tagadás és De Morgan törvényeinek alkalmazása:

    Equation 4.. 


  3. Az egzisztenciális kvantor kétoldali kiemelésére vonatkozó ekvivalencia alkalmazása:

    Equation 4.. 


  4. Változóiban tiszta alakra hozás:

    Equation 4.. 


  5. Most már mindegyik kvantor kiemelhető:

    Equation 4.. 


  6. A formula magja diszjunktív normálforma, de átírható konjunktív normálformába, ha az a további feldolgozás szempontjából úgy célszerű:

    Equation 4..