http://www.lambda.ee/w/index.php?action=history&feed=atom&title=Sissejuhatus_automaatt%C3%B5estamisse. 2026-11-07T02:06:32Z Selle lehekülje redigeerimiste ajalugu MediaWiki 1.43.11 http://www.lambda.ee/w/index.php?title=Sissejuhatus_automaatt%C3%B5estamisse.&diff=7864&oldid=prev 2006-03-01T15:33:30Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="et"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">←Vanem redaktsioon</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Redaktsioon: 1. märts 2006, kell 17:33</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l22">22. rida:</td> <td colspan="2" class="diff-lineno">22. rida:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>#Automaattõestaja ja inimese vahelise suhtluse hõlbustamine (näpunäidete andmine, suunamine teatud alamprobleemide juurde, jne.)</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>#Automaattõestaja ja inimese vahelise suhtluse hõlbustamine (näpunäidete andmine, suunamine teatud alamprobleemide juurde, jne.)</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del style="font-weight: bold; text-decoration: none;">Vaata </del>näiteks <del style="font-weight: bold; text-decoration: none;">ka</del>:&lt;br&gt;</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">Veidi põhjalikumalt võid selle kohta lugeda </ins>näiteks:&lt;br&gt;</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>http://www.cs.miami.edu/~tptp/OverviewOfATP.html</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>http://www.cs.miami.edu/~tptp/OverviewOfATP.html</div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-866:rev-7864:php=table --> </table>

Zingel http://www.lambda.ee/w/index.php?title=Sissejuhatus_automaatt%C3%B5estamisse.&diff=866&oldid=prev 2006-03-01T15:32:09Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="et"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">←Vanem redaktsioon</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Redaktsioon: 1. märts 2006, kell 17:32</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l22">22. rida:</td> <td colspan="2" class="diff-lineno">22. rida:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>#Automaattõestaja ja inimese vahelise suhtluse hõlbustamine (näpunäidete andmine, suunamine teatud alamprobleemide juurde, jne.)</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>#Automaattõestaja ja inimese vahelise suhtluse hõlbustamine (näpunäidete andmine, suunamine teatud alamprobleemide juurde, jne.)</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>Vaata ka:&lt;br&gt;</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>Vaata <ins style="font-weight: bold; text-decoration: none;">näiteks </ins>ka:&lt;br&gt;</div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">http://www.cs.miami.edu/~tptp/OverviewOfATP.html</ins></div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-865:rev-866:php=table --> </table>

Zingel http://www.lambda.ee/w/index.php?title=Sissejuhatus_automaatt%C3%B5estamisse.&diff=865&oldid=prev 2006-03-01T15:18:28Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="et"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">←Vanem redaktsioon</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Redaktsioon: 1. märts 2006, kell 17:18</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l21">21. rida:</td> <td colspan="2" class="diff-lineno">21. rida:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>#Selliste otsingustrateegiate väljatöötamine, mis annavad suurema kiiruse spetsiaalsete ülesannete puhul.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>#Selliste otsingustrateegiate väljatöötamine, mis annavad suurema kiiruse spetsiaalsete ülesannete puhul.</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>#Automaattõestaja ja inimese vahelise suhtluse hõlbustamine (näpunäidete andmine, suunamine teatud alamprobleemide juurde, jne.)</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>#Automaattõestaja ja inimese vahelise suhtluse hõlbustamine (näpunäidete andmine, suunamine teatud alamprobleemide juurde, jne.)</div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">Vaata ka:&lt;br&gt;</ins></div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-864:rev-865:php=table --> </table>

Zingel http://www.lambda.ee/w/index.php?title=Sissejuhatus_automaatt%C3%B5estamisse.&diff=864&oldid=prev 2006-03-01T15:15:36Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="et"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">←Vanem redaktsioon</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Redaktsioon: 1. märts 2006, kell 17:15</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1">1. rida:</td> <td colspan="2" class="diff-lineno">1. rida:</td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del style="font-weight: bold; text-decoration: none;">==5. Sissejuhatus automaattõestamisse.==</del></div></td><td colspan="2" class="diff-side-added"></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div> </div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div> </div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>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.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>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.</div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-862:rev-864:php=table --> </table>

Zingel http://www.lambda.ee/w/index.php?title=Sissejuhatus_automaatt%C3%B5estamisse.&diff=862&oldid=prev 2006-03-01T15:15:14Z

<p></p> <p><b>Uus lehekülg</b></p><div>==5. Sissejuhatus automaattõestamisse.==<br /> <br /> 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.<br /> <br /> Kasutatavad valemid pannakse kirja loogika keeles, sageli klassikalise loogika keeles, kuid on võimalik kasutada ka mitteklassikalisi ja kõrgema järgu loogikaid. <br /> <br /> 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.<br /> <br /> 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:<br /> <br /> #süsteem tahab saada probleemi täpse kirjelduse, mis on kirja pandud loogika keeles,<br /> #kasutaja peab hoolikalt probleemi läbi mõtlema, et suudaks seda õieti formuleerida,<br /> #süsteem üritab probleemi lahendada,<br /> #kui see õnnestub, siis annab välja tõestuse,<br /> #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,<br /> #ja nii edasi.<br /> <br /> ATSe on edukalt kasutatud probleemide lahendamiseks loogika, matemaatika, arvutiteaduse, tehnika ja sotsiaalteaduste valdkondades. Potentsiaalsed valdkonnad võiksid olla veel nt. bioloogia, arstiteadus, majandus jne.<br /> <br /> Edasise arendamise põhilised suunad:<br /> #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).<br /> #Selliste otsingustrateegiate väljatöötamine, mis annavad suurema kiiruse spetsiaalsete ülesannete puhul.<br /> #Automaattõestaja ja inimese vahelise suhtluse hõlbustamine (näpunäidete andmine, suunamine teatud alamprobleemide juurde, jne.)</div>

Zingel