Պատրաստի նյութեր

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