Mantiqê rêza yekem, ku wekî mantiqa rêza yekem (FOL) jî tê zanîn, pergalek fermî ye ku di matematîk, felsefe, zimannasî û zanistiya kompîturê de tê bikar anîn. Ew mentiqê pêşniyarê bi tevlêkirina pîvan û pêşdaçekan dirêj dike, ku rê dide zimanek bêtir diyarker ku bikaribe komek berfireh a gotinan li ser cîhanê temsîl bike. Ev pergala mentiqî di warên cihêreng de bingeh e, di nav de teoriya tevliheviya hesabkerî û ewlehiya sîber, ku ew ji bo ramana li ser algorîtma, pergal û taybetmendiyên ewlehiyê girîng e.
Di mantiqa pêşdaçekê ya rêza yekem de, pêşdaçek fonksiyonek e ku yek an çend argumanan digire û nirxek rastîn, an rast an xelet, vedigerîne. Pêşgotin ji bo îfadekirina taybetmendiyên nesneyan an têkiliyên di navbera nesneyan de têne bikar anîn. Mînakî, di domenek axaftinê de li ser mirovan, pêşdarek dibe ku "isTall(x)" be ku yek argumanek x digire û rast vedigerîne heke x dirêj be û wekî din xelet be. Nimûneyek din dikare "isSibling(x, y)" be ku du argumanên x û y digire û heke x û y xwişk û bira bin rast vedigerîne, û wekî din jî xelet vedigere.
Ji bo ku fêm bikin ka çima di mentiqê rêza yekem de predîkatan nirxên rastiyê didin, pêdivî ye ku meriv avahî û semantîka vê pergala mentiqî bihesibîne. Mantiqa rêza yekem ji hêmanên jêrîn pêk tê:
1. guherbarên: Sembolên ku ji hêmanên di warê axaftinê de radiwestin. Wek mînak x, y, z.
2. Berdewam: Sembolên ku di domanê de hêmanên taybetî vedibêjin. Wek mînak a, b, c.
3. Predicates: Sembolên ku taybetmendî an têkiliyan nîşan didin. Ew pir caran bi tîpên mezin ên wekî P, Q, R têne destnîşan kirin.
4. Kar û: Sembolên ku hêmanên domainê bi hêmanên din re nexşîne. Nimûne f, g, h.
5. Quantifiers: Sembolên ku radeya pêşdarazekê li ser domanekê diyar dikin. Du hejmarkerên seretayî jimarkera gerdûnî (∀) û mîqdara hebûnî (∃) ne.
6. Têkiliyên Mantiqî: Sembolên ku bireser û gotinan li hev dikin. Di nav wan de pevgirêdan (∧), veqetandin (∨), negatîf (¬), îmkan (→), û dubendî (↔) hene.
Hevoksaziya mentiqê rêza yekem diyar dike ka van pêkhateyan çawa dikarin werin berhev kirin da ku formulên xweş-çêkirî (WFF) çêbikin. WFF rêzek sembolan e ku ji hêla rêzimanî ve li gorî rêgezên pergala mentiqî rast e. Mînakî, heke P pêşdarazek û x guhêrbar e, wê demê P(x) WFF ye. Bi heman awayî, heke Q bi du argumanan pêşdarazek be, wê hingê Q(x, y) jî WFF e.
Semantîka mantiqa rêza yekem wateya van formulan dide. Şirovekirina zimanekî rêza yekem van tiştan pêk tîne:
1. Domain of Discourse: Komeke ne vala ya hêmanan ku guhêrbar di ser wan re derbas dibin.
2. Fonksiyona şirovekirinê: Nexşeya ku di zimên de maneyan dide domdar, fonksîyon û pêşdaçekan. Bi taybetî, ew destnîşan dike:
- Elementek domainê ji bo her sabit.
- Ji bo her sembola fonksiyonê fonksiyonek ji domê heya domanê.
- Têkiliyek li ser domainê bi her nîşanek pêşdaraz re.
Bi şirovekirin û veqetandina nirxan ji guhêrbaran re, nirxa rastiya WFF dikare were destnîşankirin. Mînakî, pêşdaçeka "isTall(x)" di domenek mirovan de bihesibînin. Ger fonksiyona şîrovekirinê taybetmendiya dirêjbûnê bi pêşdaçeka "isTall" re destnîşan bike, wê hingê "isTall(x)" dê rast be heke kesê ku bi x tê temsîl kirin dirêj be, û wekî din xelet be.
Pîvanker di mantiqa rêza yekem de rolek girîng dileyzin bi destûrdana daxuyaniyên li ser hemî an hin hêmanên domainê. Pîvana gerdûnî (∀) destnîşan dike ku pêşdaçek ji bo hemî hêmanên di domanê de derbas dibe, lê hêjmara hebûnê (∃) destnîşan dike ku di qada ku pêvek jê re heye herî kêm hêmanek heye.
Bo nimûne:
- Gotina "∀x isTall(x)" tê wateya "Her mirov dirêj e."
- Gotina "∃x isTall(x)" tê wateya "Bi kêmanî kesek dirêj heye."
Van pîvanan, bi pêşdaçekan re têne berhev kirin, avakirina vegotinên mentiqî yên tevlihev ên ku li ser bingeha şîroveyê dikarin wekî rast an xelet werin nirxandin.
Ji bo ronîkirina vê yekê, domainek ku ji sê kesan pêk tê bifikirin: Alice, Bob, û Carol. Bila pêşdaçeka "isTall(x)" wisa were şîrove kirin ku Alice û Bob dirêj in, lê Carol ne. Fonksiyona şîrovekirinê nirxên rastiyê yên jêrîn destnîşan dike:
– isTall (Alice) = rast
– dirêj e (Bob) = rast
– isTall (Carol) = derewîn
Niha, gotinên jêrîn bifikirin:
1. "∀x isTall(x)" - Ev gotin derew e ji ber ku ne her kes di domanê de dirêj e (Carol ne dirêj e).
2. "∃x isTall(x)" - Ev gotin rast e ji ber ku di domanê de kesên dirêj hene (Alice û Bob).
Nirxên rastiyê yên van gotinan ji hêla şirovekirina pêşgotin û qada axaftinê ve têne destnîşankirin.
Di teoriya tevliheviya hesabkerî û ewlehiya sîberê de, mantiqa rêza yekem tê bikar anîn da ku li ser taybetmendiyên algorîtmayan, protokol û pergalan bifikirin. Mînakî, di verastkirina fermî de, mantiqa rêza yekem dikare were bikar anîn da ku rastdariya pergalên nermalavê û hardware diyar bike û verast bike. Pêşniyarek dibe ku taybetmendiyek ewlehiyê temsîl bike, wekî "isAuthenticated(bikarhêner)" e ku rast vedigere heke bikarhêner rasthatî be û wekî din xelet be. Bi karanîna mantiqa rêza yekem, meriv dikare bi fermî îspat bike ka pergalek hin taybetmendiyên ewlehiyê di bin hemî şert û mercên gengaz de têr dike.
Wekî din, mantiqa rêza yekem di lêkolîna biryardarbûn û tevliheviya hesabkirinê de bingehîn e. Entscheidungsproblem, ku ji hêla David Hilbert ve hatî pêşkêş kirin, pirsî gelo algorîtmayek heye ku dikare rastî an nerastiya her gotinek mentiqê ya rêza yekem diyar bike an na. Alan Turing û Dêra Alonzo bi rengek serbixwe îsbat kirin ku algorîtmayek wusa tune, bêçarebûna mantiqa rêza yekem saz kirin. Ev encam ji bo sînorên hesabkirinê û tevliheviya ramana mentiqî bandorên kûr hene.
Di sepanên pratîkî de, amûrên îsbatkirina teorema otomatîk û amûrên kontrolkirina modelê bi gelemperî mantiqa rêza yekem bikar tînin da ku taybetmendiyên pergalan verast bikin. Van amûran taybetmendiyên mantiqî wekî têketinê digirin û hewl didin ku îspat bikin ka taybetmendiyên diyarkirî hene. Mînakî, kontrolkerek modelê dikare verast bike ka protokolek torê hin taybetmendiyên ewlehiyê têr dike bi vegotina van taybetmendiyan di mantiqa rêza yekem de û vekolîna hemî rewşên gengaz ên protokolê.
Pêşniyarên di mantiqa rêza yekem de, li gorî şîroveya xwe û qada axaftinê, nirxên rastiyê, rast an derewîn, derdixin. Ev taybetmendî mentiqê rêza yekem dike pergalek fermî ya hêzdar û diyarker ji bo ramana li ser taybetmendî û têkiliyên di warên cihêreng de, di nav de matematîk, felsefe, zimannasî, zanistiya computer, û ewlehiya sîber.
Pirs û bersivên din ên vê dawiyê di derbarê EITC/IS/CCTF Bingehên Teoriya Tevliheviya Hesabkirinê:
- Bi berçavgirtina PDA-yên ne-determînîst, lihevkirina dewletan ji hêla pênasê ve gengaz e. Lêbelê, PDA-yên ne-determînîst tenê stekek heye ku nekare bi hevdemî di gelek dewletan de be. Ev çawa gengaz e?
- Mînaka PDA-yan çi ye ku ji bo analîzkirina seyrûsefera torê û nasîna qalibên ku binpêkirinên ewlehiyê yên potansiyel destnîşan dikin tê bikar anîn?
- Wateya wê çi ye ku zimanek ji yê din bi hêztir e?
- Ma zimanên hesas ên kontekstê ji hêla Makîneya Turing ve têne nas kirin?
- Çima ziman U = 0^n1^n (n>=0) ne rêkûpêk e?
- Meriv çawa FSM rêzikên binary bi hêjmarên '1' yên zewac nas dike pênase bike û nîşan bide ku dema ku rêzika têketinê 1011 hildiweşîne çi diqewime?
- Nedetermînîzm çawa bandorê li fonksiyona veguherînê dike?
- Ma zimanên birêkûpêk bi Makîneyên Dewleta Dawî re hevwate ne?
- Ma pola PSPACE ne bi pola EXPSPACE re wekhev e?
- Li gorî Teza Church-Turing pirsgirêka ku ji hêla algorîtmîkî ve tê hesibandin pirsgirêkek e ku ji hêla Makîneyek Turing ve tê hesibandin?
Pirs û bersivan bêtir li Bingehên Teoriya Tevliheviya Hesabkirinê ya EITC/IS/CCTF bibînin