Սարգսյան, Լուսինե Արամայիսի

Մաթեմատիկա

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