http://www.lambda.ee/w/index.php?action=history&feed=atom&title=Soovitusi_Otteri_otsingu_suunamiseks 2026-11-07T02:49:41Z Selle lehekülje redigeerimiste ajalugu MediaWiki 1.43.11 http://www.lambda.ee/w/index.php?title=Soovitusi_Otteri_otsingu_suunamiseks&diff=10126&oldid=prev 2013-04-11T18:05:44Z

<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: 11. aprill 2013, kell 20:05</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;">= Meetodid keerulise tõestuse leidmiseks =</del></div></td><td colspan="2" class="diff-side-added"></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;"></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;"><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"></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>== Põhistrateegia valik ==</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>== Põhistrateegia valik ==</div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-10125:rev-10126:php=table --> </table>

Tammet http://www.lambda.ee/w/index.php?title=Soovitusi_Otteri_otsingu_suunamiseks&diff=10125&oldid=prev 2013-04-11T18:05:27Z

<p><span class="autocomment">Splittimine</span></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: 11. aprill 2013, kell 20:05</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l30">30. rida:</td> <td colspan="2" class="diff-lineno">30. 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>== Splittimine ==</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>== Splittimine ==</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>Vaatame, kas saab ülesande splittida alamülesanneteks a la</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>Vaatame, kas saab ülesande splittida alamülesanneteks a la <ins style="font-weight: bold; text-decoration: none;"> </ins>p(a) | p(b)</div></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;">  </del>p(a) | p(b)</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> </div></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;">siis </del>teeme kaks eraldi tõestuseotsingut</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;">Siis </ins>teeme kaks eraldi tõestuseotsingut <ins style="font-weight: bold; text-decoration: none;"> </ins>p(a) ja <ins style="font-weight: bold; text-decoration: none;"> </ins>p(b) jaoks<ins style="font-weight: bold; text-decoration: none;">.</ins></div></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;">  </del>p(a) ja</div></td><td colspan="2" class="diff-side-added"></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;">  </del>p(b) jaoks</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;"><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"></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>== Võrduse orienteerimine ==</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>== Võrduse orienteerimine ==</div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-10124:rev-10125:php=table --> </table>

Tammet http://www.lambda.ee/w/index.php?title=Soovitusi_Otteri_otsingu_suunamiseks&diff=10124&oldid=prev 2013-04-11T18:04:44Z

<p><span class="autocomment">Põhistrateegia valik</span></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: 11. aprill 2013, kell 20:04</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l13">13. rida:</td> <td colspan="2" class="diff-lineno">13. 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;"><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"></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>set(factor).</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>set(factor).</div></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;"></del></div></td><td colspan="2" class="diff-side-added"></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;">---</del></div></td><td colspan="2" class="diff-side-added"></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;"></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;"><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"></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>== Given ratio valik ==</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>== Given ratio valik ==</div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-10123:rev-10124:php=table --> </table>

Tammet http://www.lambda.ee/w/index.php?title=Soovitusi_Otteri_otsingu_suunamiseks&diff=10123&oldid=prev 2013-04-11T18:04:32Z

<p>Uus lehekülg: &#039;= Meetodid keerulise tõestuse leidmiseks = == Põhistrateegia valik == * hyperres ilma goal-directed searchita, kui on horni lähedased reeglid: set(hyper_res). * binary res ...&#039;</p> <p><b>Uus lehekülg</b></p><div>= Meetodid keerulise tõestuse leidmiseks =<br /> <br /> <br /> == Põhistrateegia valik ==<br /> <br /> * hyperres ilma goal-directed searchita, kui on horni lähedased reeglid: set(hyper_res).<br /> * binary res koos goal-directed searchiga (kasuta sos ja usable): set(binary_res).<br /> * binary res ilma goal-directed searchita, aga lisapiirangutega: set(binary_res) ja vaata lisaks.<br /> ** üks eeldus peab olema unit<br /> ** mingi spetsiifiline literaalide järjestus, kus tohib kasutada ainult järjestuse mõttes suuremaid disjunkte<br /> <br /> Alati ka:<br /> <br /> set(factor).<br /> <br /> ---<br /> <br /> <br /> == Given ratio valik ==<br /> <br /> * N korda vali kõige väiksem disjunkt<br /> * 1 kord vali queuest<br /> <br /> Enamasti on mõistlik panna ratio ca 4: assign(pick_given_ratio,4).<br /> <br /> == Piirangud järeldatavatele disjunktidele ==<br /> <br /> * piirame ära sügavuse (saab teha weight templatede abil).<br /> * piirame ära literaalide arvu disjunktis, a la assign(max_literals,3).<br /> * piirame ära disjunkti elementide koguarvu (weight), a la assign(max_weight,13).<br /> <br /> <br /> == Splittimine ==<br /> <br /> Vaatame, kas saab ülesande splittida alamülesanneteks a la<br /> p(a) | p(b)<br /> siis teeme kaks eraldi tõestuseotsingut<br /> p(a) ja<br /> p(b) jaoks<br /> <br /> == Võrduse orienteerimine ==<br /> <br /> Võrduse juures on võimalik määrata, kuidas orienteeritakse<br /> võrdusi (otteril lex parameeter) a la kas orienteerida f(x)=g(x) <br /> * f(x)-&gt;g(x) või<br /> * g(x)-&gt;f(x)</div>

Tammet