Automatizuotas teoremos įrodymas

Problemos sprendimas

Priklausomai nuo logikos, kuria vadovaujamasi, gali kilti menka ar kur kas sudėtingesnė problema sprendžiant, ar formulė tinkama ar ne. Dėl dažnai pasitaikančių matematinės logikos atvejų, problema yra išsprendžiama, tačiau neturinti ND baigtumo (Nedeterminuotasis Daugianaris laikas). Taigi, manoma, kad tik eksponentinio laiko algoritmai tinka spręsti bendrąsias įrodymų užduotis. 
Kalbant apie pirmojo lygmens predikatinių skaičiavimus, be jokių ("tinkamų") aksiomų, Godelio užbaigtumo teorema teigia, kad teoremos (įrodomi teiginiai) yra visiškai logiškai pagrįstos gerai sudarytos formulės. Vadinasi, tinkamų formulių nustatymas yra rekursiškai išvardijamas (recursively enumerable): turint neribotus išteklius, bet kuri svarbi formulė galiausiai gali būti įrodyta.
Tačiau, neteisingos formulės (kurios yra nesusijusios su tam tikra teorija) ne visada gali būti suvoktos. Pagal Godelio neužbaigtumo teoremą, atitinkama oficiali teorija, į kuria įeina pirmojo lygmens natūralių skaičių teorija (turinti tam tikras "tinkamas aksiomas"), apima teisingus teiginius, kurių neįmanoma įrodyti. Tokiais atvejais, gali nepavykti įrodyti automatizavimo teoremos, kol bus atliekama patikra. Nepaisant šių teorinių apribojimų, praktikoje teoremos įrodymas gali išspręsti daugelį sudėtingų problemų, netgi ir šių, paremtų neišsprendžiama logika.

Susijusios problemos

Paprastesnė, tačiau susijusi problema yra įrodymų patikrinimas, kai teoremos įrodymas yra pripažįstamas svariu. Šiuo atveju paprastai reikalaujama, kad kiekvieno įrodymo pakopa būtų patikrinama pagal primityvią rekursyvinę funkciją, todėl problema yra visada išsprendžiama.
Interaktyvios teoremos įrodymas reikalauja, kad žmogus pateiktų užuominų sistemai. Priklausomai nuo automatizavimo lygio, patikra gali būti iš esmės sutrumpinta iki įrodymo tikrinimo, kai vartotojas pateikia įrodymą formaliu būdu arba svarbių įrodymų užduotys atliekamos automatiškai. Interaktyvus įrodymas naudojamas įvairioms užduotims atlikti, tačiau daugelis automatinių sistemų įrodė daugybę įdomių ir sunkių teoremų, įskaitant keletą tokių, kurių matematikams ilgą laiką nepavyko įrodyti. Tačiau, tokie atvejai yra pavieniai, o sprendžiant sunkias problemas dažniausiai reikia patyrusio vartotojo.
Kitas skirtumas yra tarp teoremos įrodymo ir kitų metodikų, kuriose procesas yra laikomas teoremos įrodymu jei jis susideda iš tradicinio įrodymo, pradedant aksiomomis ir pateikiant naujos išvados žingsnius naudojantis išvados taisyklėmis. Kiti metodai apima modelio tikrinimą, kuris yra ekvivalentiškas daugelio galimų padėčių išvardijimui jėgos metodu (nors realaus modelio įgyvendinimo patikrinimas reikalauja didesnio sumanumo ir taip paprastai nesutrumpinamas iki jėgos metodo).
Yra mišrių teoremos įrodymo sistemų, kurios naudoja modelio patikrinimą kaip išvados darymo taisyklę. Taip pat yra programų, kurios buvo sukurtos tam tikrų teoremų įrodymui. Jos pateikia įrodymą (dažnai neformalų), kuris parodo, kad programai gavus tam tikrą rezultatą, teorema yra teisinga. Geras tokios programos darbo pavyzdys yra mašininis keturių spalvų teoremos įrodymas, kuris buvo labai prieštaringas kaip ir pirmasis pasiektas matematinis įrodymas. Jo žmonėms buvo iš esmės neįmanoma patvirtinti dėl milžiniškų programos atliktų skaičiavimų (tokie įrodymai vadinami netiriamais). Kitas pavyzdys galėtų būti įrodymas, kad žaidime ,,Sujunk keturis” (angl. Connect Four) visada laimi pirmasis žaidėjas.

Pramoninis naudojimas

Komercijai ATĮ daugiausiai naudojamas integrinės schemos projektavimui ir atestacijai. Nuo Pentuim FDIV klaidos, sudėtingos modernių mikroprocesorių slankiojo kablelio grandys buvo projektuojamos ypatingai kruopščiai. Naujausiuose procesoriuose po AMD, Intel ir kitų, ATĮ buvo naudojamas patvirtinti, kad paskirstymas ir kiti procesai vyksta teisingai.

Deontinės teoremos įrodymas

Deontinė logika yra susijusi su normatyviniais teiginiais, naudojamais tokiose srityse kaip teisė, techninės instrukcijos ar kompiuterinės programos. Kitaip tariant, šie teiginiai yra komandų vertimai arba kasdieninės kalbos pareiškimai ,,turėtum” arba ,,privalai (nedaryti)”. Deontinis tokios logikos požymis reikalauja formalumo, kuris išplėstų pirmojo lygmens predikatinius skaičiavimus. Tą padaryti padeda priemonė ,,KED”.

Raštai

1. ^ W.W. McCune (1997). "Solution of the Robbins Problem". Journal of Automated Reasoning 19 (3). http://www.springerlink.com/content/h77246751668616h/. 
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. 
3. ^ http://www.cs.miami.edu/~tptp/
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).