b'\n_START_ARTICLE_\nAutomatizuotas teoremos \xc4\xafrodymas\n_START_SECTION_\nProblemos sprendimas\n_START_PARAGRAPH_\nPriklausomai nuo logikos, kuria vadovaujamasi, gali kilti menka ar kur kas sud\xc4\x97tingesn\xc4\x97 problema sprend\xc5\xbeiant, ar formul\xc4\x97 tinkama ar ne. D\xc4\x97l da\xc5\xbenai pasitaikan\xc4\x8di\xc5\xb3 matematin\xc4\x97s logikos atvej\xc5\xb3, problema yra i\xc5\xa1sprend\xc5\xbeiama, ta\xc4\x8diau neturinti ND baigtumo (Nedeterminuotasis Daugianaris laikas). Taigi, manoma, kad tik eksponentinio laiko algoritmai tinka spr\xc4\x99sti bendr\xc4\x85sias \xc4\xafrodym\xc5\xb3 u\xc5\xbeduotis. _NEWLINE_Kalbant apie pirmojo lygmens predikatini\xc5\xb3 skai\xc4\x8diavimus, be joki\xc5\xb3 ("tinkam\xc5\xb3") aksiom\xc5\xb3, Godelio u\xc5\xbebaigtumo teorema teigia, kad teoremos (\xc4\xafrodomi teiginiai) yra visi\xc5\xa1kai logi\xc5\xa1kai pagr\xc4\xafstos gerai sudarytos formul\xc4\x97s. Vadinasi, tinkam\xc5\xb3 formuli\xc5\xb3 nustatymas yra rekursi\xc5\xa1kai i\xc5\xa1vardijamas (recursively enumerable): turint neribotus i\xc5\xa1teklius, bet kuri svarbi formul\xc4\x97 galiausiai gali b\xc5\xabti \xc4\xafrodyta._NEWLINE_Ta\xc4\x8diau, neteisingos formul\xc4\x97s (kurios yra nesusijusios su tam tikra teorija) ne visada gali b\xc5\xabti suvoktos. Pagal Godelio neu\xc5\xbebaigtumo teorem\xc4\x85, atitinkama oficiali teorija, \xc4\xaf kuria \xc4\xafeina pirmojo lygmens nat\xc5\xabrali\xc5\xb3 skai\xc4\x8di\xc5\xb3 teorija (turinti tam tikras "tinkamas aksiomas"), apima teisingus teiginius, kuri\xc5\xb3 ne\xc4\xafmanoma \xc4\xafrodyti. Tokiais atvejais, gali nepavykti \xc4\xafrodyti automatizavimo teoremos, kol bus atliekama patikra. Nepaisant \xc5\xa1i\xc5\xb3 teorini\xc5\xb3 apribojim\xc5\xb3, praktikoje teoremos \xc4\xafrodymas gali i\xc5\xa1spr\xc4\x99sti daugel\xc4\xaf sud\xc4\x97ting\xc5\xb3 problem\xc5\xb3, netgi ir \xc5\xa1i\xc5\xb3, paremt\xc5\xb3 nei\xc5\xa1sprend\xc5\xbeiama logika.\n_START_SECTION_\nSusijusios problemos\n_START_PARAGRAPH_\nPaprastesn\xc4\x97, ta\xc4\x8diau susijusi problema yra \xc4\xafrodym\xc5\xb3 patikrinimas, kai teoremos \xc4\xafrodymas yra pripa\xc5\xbe\xc4\xafstamas svariu. \xc5\xa0iuo atveju paprastai reikalaujama, kad kiekvieno \xc4\xafrodymo pakopa b\xc5\xabt\xc5\xb3 patikrinama pagal primityvi\xc4\x85 rekursyvin\xc4\x99 funkcij\xc4\x85, tod\xc4\x97l problema yra visada i\xc5\xa1sprend\xc5\xbeiama._NEWLINE_Interaktyvios teoremos \xc4\xafrodymas reikalauja, kad \xc5\xbemogus pateikt\xc5\xb3 u\xc5\xbeuomin\xc5\xb3 sistemai. Priklausomai nuo automatizavimo lygio, patikra gali b\xc5\xabti i\xc5\xa1 esm\xc4\x97s sutrumpinta iki \xc4\xafrodymo tikrinimo, kai vartotojas pateikia \xc4\xafrodym\xc4\x85 formaliu b\xc5\xabdu arba svarbi\xc5\xb3 \xc4\xafrodym\xc5\xb3 u\xc5\xbeduotys atliekamos automati\xc5\xa1kai. Interaktyvus \xc4\xafrodymas naudojamas \xc4\xafvairioms u\xc5\xbeduotims atlikti, ta\xc4\x8diau daugelis automatini\xc5\xb3 sistem\xc5\xb3 \xc4\xafrod\xc4\x97 daugyb\xc4\x99 \xc4\xafdomi\xc5\xb3 ir sunki\xc5\xb3 teorem\xc5\xb3, \xc4\xafskaitant kelet\xc4\x85 toki\xc5\xb3, kuri\xc5\xb3 matematikams ilg\xc4\x85 laik\xc4\x85 nepavyko \xc4\xafrodyti. Ta\xc4\x8diau, tokie atvejai yra pavieniai, o sprend\xc5\xbeiant sunkias problemas da\xc5\xbeniausiai reikia patyrusio vartotojo._NEWLINE_Kitas skirtumas yra tarp teoremos \xc4\xafrodymo ir kit\xc5\xb3 metodik\xc5\xb3, kuriose procesas yra laikomas teoremos \xc4\xafrodymu jei jis susideda i\xc5\xa1 tradicinio \xc4\xafrodymo, pradedant aksiomomis ir pateikiant naujos i\xc5\xa1vados \xc5\xbeingsnius naudojantis i\xc5\xa1vados taisykl\xc4\x97mis. Kiti metodai apima modelio tikrinim\xc4\x85, kuris yra ekvivalenti\xc5\xa1kas daugelio galim\xc5\xb3 pad\xc4\x97\xc4\x8di\xc5\xb3 i\xc5\xa1vardijimui j\xc4\x97gos metodu (nors realaus modelio \xc4\xafgyvendinimo patikrinimas reikalauja didesnio sumanumo ir taip paprastai nesutrumpinamas iki j\xc4\x97gos metodo)._NEWLINE_Yra mi\xc5\xa1ri\xc5\xb3 teoremos \xc4\xafrodymo sistem\xc5\xb3, kurios naudoja modelio patikrinim\xc4\x85 kaip i\xc5\xa1vados darymo taisykl\xc4\x99. Taip pat yra program\xc5\xb3, kurios buvo sukurtos tam tikr\xc5\xb3 teorem\xc5\xb3 \xc4\xafrodymui. Jos pateikia \xc4\xafrodym\xc4\x85 (da\xc5\xbenai neformal\xc5\xb3), kuris parodo, kad programai gavus tam tikr\xc4\x85 rezultat\xc4\x85, teorema yra teisinga. Geras tokios programos darbo pavyzdys yra ma\xc5\xa1ininis keturi\xc5\xb3 spalv\xc5\xb3 teoremos \xc4\xafrodymas, kuris buvo labai prie\xc5\xa1taringas kaip ir pirmasis pasiektas matematinis \xc4\xafrodymas. Jo \xc5\xbemon\xc4\x97ms buvo i\xc5\xa1 esm\xc4\x97s ne\xc4\xafmanoma patvirtinti d\xc4\x97l mil\xc5\xbeini\xc5\xa1k\xc5\xb3 programos atlikt\xc5\xb3 skai\xc4\x8diavim\xc5\xb3 (tokie \xc4\xafrodymai vadinami netiriamais). Kitas pavyzdys gal\xc4\x97t\xc5\xb3 b\xc5\xabti \xc4\xafrodymas, kad \xc5\xbeaidime ,,Sujunk keturis\xe2\x80\x9d (angl. Connect Four) visada laimi pirmasis \xc5\xbeaid\xc4\x97jas.\n_START_SECTION_\nPramoninis naudojimas\n_START_PARAGRAPH_\nKomercijai AT\xc4\xae daugiausiai naudojamas integrin\xc4\x97s schemos projektavimui ir atestacijai. Nuo Pentuim FDIV klaidos, sud\xc4\x97tingos moderni\xc5\xb3 mikroprocesori\xc5\xb3 slankiojo kablelio grandys buvo projektuojamos ypatingai kruop\xc5\xa1\xc4\x8diai. Naujausiuose procesoriuose po AMD, Intel ir kit\xc5\xb3, AT\xc4\xae buvo naudojamas patvirtinti, kad paskirstymas ir kiti procesai vyksta teisingai.\n_START_SECTION_\nDeontin\xc4\x97s teoremos \xc4\xafrodymas\n_START_PARAGRAPH_\nDeontin\xc4\x97 logika yra susijusi su normatyviniais teiginiais, naudojamais tokiose srityse kaip teis\xc4\x97, technin\xc4\x97s instrukcijos ar kompiuterin\xc4\x97s programos. Kitaip tariant, \xc5\xa1ie teiginiai yra komand\xc5\xb3 vertimai arba kasdienin\xc4\x97s kalbos parei\xc5\xa1kimai ,,tur\xc4\x97tum\xe2\x80\x9d arba ,,privalai (nedaryti)\xe2\x80\x9d. Deontinis tokios logikos po\xc5\xbeymis reikalauja formalumo, kuris i\xc5\xa1pl\xc4\x97st\xc5\xb3 pirmojo lygmens predikatinius skai\xc4\x8diavimus. T\xc4\x85 padaryti padeda priemon\xc4\x97 ,,KED\xe2\x80\x9d.\n_START_SECTION_\nRa\xc5\xa1tai\n_START_PARAGRAPH_\n1. ^ W.W. McCune (1997). "Solution of the Robbins Problem". Journal of Automated Reasoning 19 (3). http://www.springerlink.com/content/h77246751668616h/. _NEWLINE_2. ^ Gina Kolata (December 10, 1996). "Computer Math Proof Shows Reasoning Power". The New York Times. http://www.nytimes.com/library/cyber/week/1210math.html. Retrieved 2008-10-11. _NEWLINE_3. ^ http://www.cs.miami.edu/~tptp/_NEWLINE_4. ^ Artosi, Alberto, Cattabriga, Paola and Governatori, Guido (1994-01-01). KED: A Deontic Theorem Prover. In: Biagioli, Carlo, Sartor, Giovanni and Tiscornia, Daniela Workshop on Legal Application of Logic Programming, Santa Margherita Ligure, Italy, (60-76).'