See also ebooksgratis.com: no banners, no cookies, totally FREE.

CLASSICISTRANIERI HOME PAGE - YOUTUBE CHANNEL
Privacy Policy Cookie Policy Terms and Conditions
Forma preneksowa - Wikipedia, wolna encyklopedia

Forma preneksowa

Z Wikipedii

Forma preneksowa (ang. prenex form lub prenex normal form) to taka postać formuły logicznej, w której wszystkie kwantyfikatory przesunięte są na początek formuły. Inna jej nazwa to postać normalna.

Każde zdanie rachunku predykatów pierwszego rzędu można sprowadzić do postaci preneksowej. Najpierw należy zmienić nazwy wszystkim zmiennym, które kolidują, na przykład:

(\forall x . R(x)) \implies (\exists x. R(x)) na (\forall x . R(x)) \implies (\exists y. R(y))


co w żaden sposób nie zmienia znaczenia formuły. Następnie należy przenosić kwantyfikatory coraz wyżej, zmieniając je na przeciwny za każdym razem, gdy napotkają negację:

(\forall x . R(x)) \implies (\exists y. R(y))
(\neg \forall x . R(x)) \or (\exists y. R(y))
\exists x . (\neg R(x) \or (\exists y. R(y))
\exists x . \exists y . (\neg R(x) \or R(y))

Jeśli p \or (\forall x . q(x)) czy też p \and (\forall x . q(x)), i x nie występuje w p (co sobie zagwarantowaliśmy zmieniając nazwy wszystkich kolidujących zmiennych), przeniesienie kwantyfikatora wyżej nie zmienia znaczenia formuły. Można to uogólnić na ogólny operator koniunkcyjny i dysjunkcyjny.

Forma preneksowa jest bardzo wygodna dla komputera, w mniejszym zaś stopniu dla ludzi.

[edytuj] Przykłady

  • \forall x . \exists y . y > x jest w formie preneksowej
  • (\forall x . R(x)) \implies (\exists x. R(x)) nie jest w formie preneksowej.

[edytuj] Zobacz też


aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -