Sissejuhatus automaattõestamisse.
Automaatse teoreemitõestamise eesmärgiks on selliste arvutiprogrammide loomine, mis näitaksid, et mingi väide (oletus) on mingi väidete hulga (aksioomide ja hüpoteeside) loogiliseks järelduseks. Inimene formaliseerib täpselt probleemi ja annab selle arvutile lahendamiseks, oodates tulemust mõistliku aja jooksul. Automaattõestamissüsteeme (ATS) kasutatakse väga mitmesugustes valdkondades, kus aga on võimalik väljendada oma probleemi aksioomide, hüpoteeside ja oletuse abil.
Kasutatavad valemid pannakse kirja loogika keeles, sageli klassikalise loogika keeles, kuid on võimalik kasutada ka mitteklassikalisi ja kõrgema järgu loogikaid.
ATSde poolt väljastatud tõestused kirjeldavad, kuidas ja miks oletus aksioomidest ja hüpoteesidest järeldub, ja see kirjeldus antakse üldiselt tunnustatud kujul, millest kõik, ka teised arvutiprogrammid, on võimelised aru saama. Alati pole vastuseks vaid “jah, oletus järeldub loogiliselt aksioomidest ja hüpoteesidest”, sageli on vastuseks probleemile lahendust andva protsessi kirjeldus.
ATSd on võimsad programmid, mis suudavad lahendada ülimalt keerukaid ülesandeid. Samas on nende rakendamisel ja kasutamisel sageli vaja eksperdi abi. Sageli kasutatakse ATSe interaktiivsel moel:
- süsteem tahab saada probleemi täpse kirjelduse, mis on kirja pandud loogika keeles,
- kasutaja peab hoolikalt probleemi läbi mõtlema, et suudaks seda õieti formuleerida,
- süsteem üritab probleemi lahendada,
- kui see õnnestub, siis annab välja tõestuse,
- kui ei õnnestu, siis võib kasutaja anda edasisi näpunäiteid või proovida lahendada mõnd vahetulemust või kontrollida, kas probleem on ikka korrektselt kirja pandud,
- ja nii edasi.
ATSe on edukalt kasutatud probleemide lahendamiseks loogika, matemaatika, arvutiteaduse, tehnika ja sotsiaalteaduste valdkondades. Potentsiaalsed valdkonnad võiksid olla veel nt. bioloogia, arstiteadus, majandus jne.
Edasise arendamise põhilised suunad:
- Uute otsingumeetodite väljatöötamine, mis võimaldaksid igasuguse ülesande korral vanade meetoditega võrreldes suuremat otsingukiirust (paremad insenerilahendused nii tarkvara kirjutamisel kui riistvara rakendamisel).
- Selliste otsingustrateegiate väljatöötamine, mis annavad suurema kiiruse spetsiaalsete ülesannete puhul.
- Automaattõestaja ja inimese vahelise suhtluse hõlbustamine (näpunäidete andmine, suunamine teatud alamprobleemide juurde, jne.)
Veidi põhjalikumalt võid selle kohta lugeda näiteks:
http://www.cs.miami.edu/~tptp/OverviewOfATP.html
