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