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:
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.
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:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Példa Hozzuk a
formulát prenexalakra.
Változóiban tiszta alakra hozás:
De Morgan törvényeinek alkalmazása:
Kvantorkiemelés:
Kvantorkiemelés:
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.
Az implikációk átírása:
A kétszeres tagadás és De Morgan törvényeinek alkalmazása:
Az egzisztenciális kvantor kétoldali kiemelésére vonatkozó ekvivalencia alkalmazása:
Változóiban tiszta alakra hozás:
Most már mindegyik kvantor kiemelhető:
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ű:
