Թամազյան, Հակոբ Արամի

Մաթեմատիկա

Այս աշխատանքը ուսումնասիրում է արտածումների բարդության (proof complexity) հիմնախնդիրը ասույթային հաշվի տարբեր հայտնի և նոր կառուցված համակարգերում՝ կենտրոնանալով այն վրա, թե ինչպես են փոխվում ապացույցների երկարությունը, կառուցվածքը և հաշվարկային ռեսուրսների պահանջները տարբեր տրամաբանական համակարգերում։ Աշխատությունում վերլուծվում են դասական ապացուցման համակարգեր, ինչպիսիք են Հիլբերտյան համակարգերը, բնական դեդուկցիան և ռեզոլյուցիոն մեթոդները, ինչպես նաև նորագույն մոտեցումներ, որոնք կիրառվում են ավտոմատացված ապացուցման և հաշվողական բարդության տեսության մեջ։ Հեղինակը դիտարկում է, թե ինչպես են տարբեր համակարգերում նույն տրամաբանական պնդումների արտածումները կարող ունենալ զգալիորեն տարբեր բարդություն՝ թե՛ քայլերի քանակի, թե՛ կառուցվածքային խորության տեսանկյունից, և ինչպես են այդ տարբերությունները կապված հաշվարկային բարդության դասերի հետ։ Աշխատությունը նաև անդրադառնում է ապացույցների կոմպրեսիայի, էքսպոնենցիալ երկարությունների առաջացման պատճառներին և այն հարցին, թե արդյոք հնարավոր է գտնել ավելի արդյունավետ ապացուցման համակարգեր, որոնք կկրճատեն արտածումների բարդությունը առանց արտահայտչականության կորստի։ Բացի այդ, քննարկվում են ժամանակակից արդյունքներ proof complexity-ի և SAT-խնդիրների լուծման ալգորիթմների միջև կապերի վերաբերյալ, ինչը կարևոր է ինչպես տեսական ինֆորմատիկայի, այնպես էլ կիրառական ալգորիթմների զարգացման համար։ Ընդհանուր առմամբ, աշխատանքը ներկայացնում է խորքային վերլուծություն այն մասին, թե ինչպես են տրամաբանական համակարգերի կառուցվածքային հատկությունները ազդում արտածումների բարդության վրա և ինչ սահմանափակումներ են առաջանում ավտոմատացված դատողությունների համակարգերում։