Թեորեմների ավտոմատացված ապացուցում

Ավտոմատացված թեորեմների ապացուցումը (որը նաև հայտնի է որպես ATP կամ ավտոմատացված դեդուկցիա) ավտոմատացված հիմնավորման և մաթեմատիկական տրամաբանության ենթածրագիր է, որը վերաբերում է համակարգչային ծրագրերով մաթեմատիկական տեսությունների հաստատմանը։ Մաթեմատիկական ապացույցի վերաբերյալ ավտոմատացված հիմնավորումը խթան հանդիսացավ համակարգչային գիտության զարգացման համար։

Առաջին իրականացումներ[խմբագրել | խմբագրել կոդը]

Երկրորդ համաշխարհային պատերազմից կարճ ժամանակ անց առաջին համակարգիչները հասանելի դարձան։ 1954 թ.-ին Մարտին Դևիսը ծրագրում էր Պրովսբերգերի ալգորիթմը, JOHNNIAC վակուումային համակարգչի համար, Պրինսետոնի ինստիտուտի խորացված ուսումնասիրության ինստիտուտում։ Դևիսի խոսքերով, «Նրա մեծ հաղթանակը պետք է ապացուցի, որ երկու զույգ թվերի գումարը կրկին զույգ թիվ է»։ Ավելի հավակնոտ էր Logic Theory Machine-ը 1956 թ.-ին, Allia Newell-ի կողմից մշակված Principia Mathematica-ի պնդման տրամաբանության դեդուկցիոն համակարգը:Այս ծրագիրը՝, տրամաբանության տեսության մեքենան (Logic Theory Machine-ը), որը նաև աշխատում էր JOHNNIAC-ում, կառուցում էր ապացույցներ փոքրիկ պնդում աքսիոմներից և երեք դեդուկցիոն կանոններից. Modus ponens, (propositional) փոփոխականի փոխարինում և բանաձևերի փոխարինում դրանց սահմանմամբ։ Համակարգը օգտագործեց էվիրիական ուղեցույց և հաջողեց ապացուցել Principia-ի առաջին 52 տեսության 38-ը։

Տրամաբանության տեսության մեքենայի «էվիրիստական» մոտեցումը փորձել է մրցել մաթեմատիկոսների հետ, սակայն չի կարող երաշխավորել, որ ապացույց կարելի է գտնել կամայական հիմնավոր թեորեմի համար։ Ի տարբերություն մյուս, ավելի համակարգված ալգորիթմների, առնվազն տեսականորեն, ամբողջականությունն առաջին կարգի տրամաբանության համար է։ Նախնական մոտեցումները հիմնված էին Հերբրանդի և Սքոեմի արդյունքների վրա, որպեսզի առաջին կարգի բանաձևը դառնան առաջադեմ բանաձևերի ավելի մեծ հավաքածուներ, դարձնելով փոփոխականները Հերբրեն տիեզերքի տերմիններով։ Այնուհետև առաջարկվող բանաձևերը կարող են ստուգվել մի քանի մեթոդների կիրառմամբ անբավարարելիության համար։ Gilmore-ի ծրագիրն օգտագործեց ձևափոխման նորմալ ձևը, որում ձևակերպված է բանաձևի բավարարելիությունը։

Խնդրի լուծելիությունը[խմբագրել | խմբագրել կոդը]

Կախված հիմքում ընկած տրամաբանությունից, բանաձևի վավերականության որոշման խնդիրը տատանվում է պարզագույնից մինչ անհնարին։ Առաջարկվող տրամաբանության հաճախակի դեպքի համար խնդիրը վճռական է, սակայն համահունչ NP-ը ամբողջական է, և հետևաբար, ընդհանուր ապացույցների առաջադրանքների համար ենթադրվում է միայն ժամանակային ժամանակի ալգորիթմներ։ Առաջին պատվին նախորդ հաշվարկի համար Գեելի ամբողջականության տեսությունը նշում է, որ թեորեմները (ապացուցելի պնդումները) հենց տրամաբանորեն վավեր են լավ ձևավորված բանաձևերը, ուստի վավեր բանաձևերը նույնականացնող թվացյալ են. Հաշվի առնելով անսահման ռեսուրսները, ցանկացած վավեր բանաձև, ի վերջո, կարող է ապացուցել։ Այնուամենայնիվ, անվավեր ձևակերպումները (որոնք չեն ենթարկվում տվյալ տեսության մեջ), չեն կարող միշտ ճանաչվել։

Արտաքին հղումներ[խմբագրել | խմբագրել կոդը]

Գրականություն[խմբագրել | խմբագրել կոդը]