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

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

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

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

Մաթեմատիկական արտահայտությունների ապացույցներ գտնող համակարգչային ծրագրերից է Ռոբինի վարկածի **([[:en:Robbins algebra|Robbin’s conjecture]])** ապացույցը 1997 թվականին։

¬ (¬ (a ∨ b) ∨ ¬ (a ∨ ¬b)) = a

Ընդհանուր առմամբ առաջընթացը հիասթափեցնող է։ Խնդիրների որոշակի դասի համար մենք կարծես փակուղու մեջ լինենք, որոնք լուծելի են թվում միայն մարդկանց սրամտության շնորհիվ։ Ավտոմատ թեորեմների ապացուցման երկու հիմնական ձև կա։ Մարդկային ուղղվածություն **([https://dspace.mit.edu/handle/1721.1/5807 human-oriented approach])** ունեցող մոտեցում, որը համակարգիչը սերտորեն փորձում է ըդնօրինակել՝ այն ճանապարհը, որով մարդը ապացույց կգտնի, և մեքենայական մոտեցումը **([https://dl.acm.org/citation.cfm?id=321253 machine-oriented approach])**, որը նպատակ ունի գերազանցել այն, ինչ մարդիկ կարող են անել՝ օգտագործելով համակարգիչների հսկայական գերազանցությունը և հիշողությունը։ Ներկայումս մեքենայական մոտեցումը ավելի նորաձև է և գրավիչ, բայց դե փակուղուց դուրս գալու համար պետք է վերադառնալ մարդկային ուղղվածության (human-oriented approach)։

## Պատմություն
Թեորեմների ավտոմատ ապացուցումը արհեստական բանականության ամենահին ճյուղերից մեկն է։ Թեորեմների ավտոմատ ապացույցների բնագավառում կատարված հետազոտությունների շնորհիվ ձևակերպվել են որոնման ալգորիթմները(Օրինակ '''Binary Search Tree''') և ձևավորվել են պաշտոնական լեզուներ, ինչպիսին է օրինակ՝ տրամաբանական ծրագրավորման լեզուն PROLOG-ը։

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

Այժմ համակարգիչը հիմնականում իր արագագործության հաշվին քննարկում է բոլոր հնարավոր դեպքերը, ասենք օրինակ՝ թերի ինդուկցիայի մեթոդով և այլն, բայց վերջում երկար աշխատանքից հետո ընտրում է ամենակարճ լուծումը։ Օրինակ ծրագրավորված մեքենային տրվել է հետևյալ խնդիրը՝

Գտնել այնպիսի 100 անընդմեջ թվերի հաջորդականություն, որոնցից ոչ մեկը պարզ թիվ չէ։

Այս դեպքում մարդիկ ավելի հեշտ են գտել լուծումը քան համակարգիչը։ Նկարում պատկերված խնդիրը օգտագործվել է 2016 թվականին կատարված **Turing Test**-ի Ժամանակ, որում հարցվածների 60%-ը սխալվել է ընտրելով համակարգչի տված լուծումը՝ դա նշանակում է, որ հարցվածների գերակշռող մասի կարծիքով համակարգչի տված լուծումը ավելի նման է եղել մարդու բանականությանը մոտ լուծմանը։

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

## Ծանոթագրություններ

## Գրականություն
*Automated Theorem Proving
*Automated Theorem Proving Scott Sanner, Guest Lecture Topics in Automated Reasoning Thursday, Jan. 19, 2006
*THE  PHILOSOPHY  OF  AUTOMATED  THEOREM  PROVING
*Automated Theorem Proving Frank Pfenning Carnegie Mellon University
*Machine learning and automated theorem proving
*Logic and Proof Computer Science Tripos Part IB Michaelmas Term
*Automated theorem proving: theory and practice
*Logic for Computer Science: Foundations of Automatic Theorem Proving, Second Edition Jean Gallier

## Արտաքին հղումներ
*An overview of automated theorem proving 
*What is automated theorem proving
*https://www.youtube.com/watch?v=OLxbIXwpMes
*https://www.youtube.com/watch?v=9a_sHJ4OS8c
*https://www.youtube.com/watch?v=Nydg-N83VYc
*https://www.youtube.com/watch?v=UAa2o0W7vcg

Կատեգորիա:Արհեստական բանականություն
Կատեգորիա:Էքսպերտ համակարգեր
Կատեգորիա:Տրամաբանություն
Կատեգորիա:Ֆորմալ մեթոդներ