http://www.lambda.ee/w/index.php?action=history&feed=atom&title=ITV0081_arhiiv_2014
ITV0081 arhiiv 2014 - Redigeerimiste ajalugu
2026-11-07T00:47:08Z
Selle lehekülje redigeerimiste ajalugu
MediaWiki 1.43.11
http://www.lambda.ee/w/index.php?title=ITV0081_arhiiv_2014&diff=12178&oldid=prev
Tammet: Uus lehekülg: 'Ainekood: ITV0081<br> Lektor: Tanel Tammet<br> Kontakt: tanel.tammet@ttu.ee, 6203457, TTÜ AK223<br> Arhiiv: ITV0081 arhiiv 2012 == <font color="red">See on 2013 aasta arhii...'
2015-02-02T16:07:26Z
<p>Uus lehekülg: 'Ainekood: ITV0081<br> Lektor: Tanel Tammet<br> Kontakt: tanel.tammet@ttu.ee, 6203457, TTÜ AK223<br> Arhiiv: <a href="/wiki/ITV0081_arhiiv_2012" title="ITV0081 arhiiv 2012">ITV0081 arhiiv 2012</a> == <font color="red">See on 2013 aasta arhii...'</p>
<p><b>Uus lehekülg</b></p><div>Ainekood: ITV0081<br><br />
Lektor: Tanel Tammet<br><br />
Kontakt: tanel.tammet@ttu.ee, 6203457, TTÜ AK223<br><br />
Arhiiv: [[ITV0081 arhiiv 2012]]<br />
<br />
== <font color="red">See on 2013 aasta arhiiv, mitte käimasoleva kursuse materjalid!</font> ==<br />
<br />
Eksamiajad:<br />
<br />
* Reede, 24 mai kell 10:00 ruumis X-310 (majanduse maja). Seejuures:<br />
** 10:00 kodutööde esitamine<br />
** 11:00 eksam<br />
<br />
* Kolmapäev, 5. juuni kell 10:00 ruumis X-210 (majanduse maja). Seejuures:<br />
** 10:00 kodutööde esitamine<br />
** 11:00 eksam<br />
<br />
<br />
Eksamil on küsimusi kolmest teemast:<br />
<br />
* Lausearvutus:<br />
** Lausearvutuse semantika (tõeväärtustabelid) <br />
** DPLL: oskus teha väikest näidet käsitsi. Liigagi põhjalikud materjalid ntx siit: [[Media:SatLecture1.ppt]], [[Media:SatLecture2.ppt]],[[Media:SatLecture3.ppt]]<br />
* Predikaatarvutus:<br />
** Arusaamine järgmiste materjalide tasemel:<br />
*** [http://dspace.utlib.ee/dspace/bitstream/handle/10062/24397/9985562313.pdf Loogika: mõtlemisest tõestamiseni. TÜ Kirjastus, 2002], semantika ehk mudelite osa & teor tõestamise osa.<br />
*** [[Media:Geoffreasoningnotes.pdf|Geoff reasoning course notes]]<br />
*** Võrdus [[Media:Equality_lecture15.ppt]] ja [[Media:Rewritesystems.pdf]]<br />
** Oskus teha resolutsioonimeetodi ülesandeid: unifitseerimine ja väikeste näidete lahendamine, seejuures baasstrateegiad.<br />
** Oskus kodeerida väikesi ülesandeid predikaatarvutusse.<br />
<br />
* Indekseerimine:<br />
** McCune klassikalise artikli tasemel: [[Media: Mccuneindexing.pdf]]<br />
** Oskus ehitada väikesi discrimination tree indeksipuid (trie termi jaoks).<br />
<br />
== Muutused loengukohas ==<br />
<br />
Loengud toimuvad nüüd ja edaspidi uues IT majas Akadeemia 15, 4 korrus arvutiteaduse seminariruumis 411.<br />
<br />
== Koht ja aeg ==<br />
<br />
Semester: kevad<br><br />
Hindamine: eksam + praktikumid<br><br />
Loengud: iga esmaspäev kell 17:45-19:15 ruumis IT-140<br><br />
Praktikumid: neljapäeviti paarisnädalatel kell 16:00-17:30 ruumis IT-213D, IT-213H.<br><br />
<br />
<br />
==Soovitatav kirjandus:==<br />
* T.Tamme, T.Tammet, R.Prank. [http://dspace.utlib.ee/dspace/bitstream/handle/10062/24397/9985562313.pdf Loogika: mõtlemisest tõestamiseni. TÜ Kirjastus, 2002]<br />
* [[Media:Geoffreasoningnotes.pdf|Geoff reasoning course notes]]<br />
<br />
<br />
== 2013 aasta kodused ülesanded ==<br />
<br />
Praktikumide kuupäevad: 14., 28. veebruar, 14., 28. märts, 11., 25. aprill, 9., ja 23. mai.<br />
<br />
Ülesanded jagunevad kaheks: <br />
* käsitsi väikeste ülesannete lahendamine<br />
* tõestajatega eksperimenteerimine mittetriviaalsete ülesannete automaatseks lahendamiseks<br />
<br />
=== 1. prax ===<br />
<br />
14. veebruar: [[lausearvutuse ja lihtsamate predikaatarvutuse ülesannete lahendamine]].<br />
<br />
=== 2. prax ===<br />
<br />
14. märts: lausearvutuse tõestajatega eksperimenteerimine.<br />
<br />
Ülesandel on kaks varianti - lihtsam ja keerulisem - ning võid ise valida, kumbat teed.<br />
<br />
Lihtsam: [[Prax 2: lausearvutuse lahendajatega eksperimenteerimine]]<br />
<br />
Keerulisem: [[Prax 2: lihtsa DPLL lahendaja realiseerimine]]<br />
<br />
=== 3. prax ===<br />
<br />
9. mai: predikaatarvutuse tõestajatega eksperimenteerimine.<br />
<br />
Kaks osa: soendus ja põhiosa.<br />
<br />
A) Soendus:<br />
<br />
1. osa: lihtsad katsed tõestajaga<br />
<br />
Geoff:<br />
<br />
* lk 36 ülesanded 1,3,4,5,6,8<br />
* lk 43 ülesanne 7: joonista puu<br />
* lk 47 ülesanne 2<br />
<br />
Eesti õpik:<br />
<br />
* lk 319 ülesanne 3<br />
<br />
B) Põhiosa: katsed tõestajaga, kus Otter automaatrezhiim ei leia mõistliku<br />
aja jooksul lahendust, vaja on ise proovida eri strateegiaid. <br />
Ülesanded: [[Media:Problems.tar.gz]]. Mõned neist (ntx ex_1) on lihtsad, ja Otteri automaatrezhiim leiab kiirelt tõestuse. Alustagi lihtsatest. Enamik ülesandeid on keerulisemad.<br />
<br />
<br />
Mida sa pead nende ülesannetega tegema? Leidma Otteriga lahenduse, kusjuures pead ise seadma sellised otsingustrateegiad ja piirangud, et Otter sinu masinas hakkama saaks.<br />
Seejuures <b>ei tohi</b> kasutada automaatrezhiimi ja GEO ülesannete juures ei tohi kasutada splittimist. Sa võid küll automaatrezhiimi ja splittimisega katsetada (see on täiesti soovitav) <br />
aga lõpuks pead leidma ise fikseeritud strateegia ja piirangud, millega Otter lahenduse leiab.<br />
Vaata kindlasti ka <br />
* [[soovitusi Otteri otsingu suunamiseks]].<br />
* [http://www.cs.miami.edu/~tptp/ TPTP] ja sealt [http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems Problems] ja selle alt leiad ülesannete tõestused ja saad online katsetada hulga eri tõestajatega: eriti head on Vampire ja E.<br />
* [https://www.cs.unm.edu/~mccune/mace2/ Otter]<br />
<br />
=== 4. prax ===<br />
<br />
See on vabatahtlik praks, mis annab hulgaliselt ekstrapunkte.<br />
<br />
Ülesanne on tõestada <br />
<pre><br />
All x All y Exists z All u ((m(u,x) & m(u,y)) <=> m(u,z))<br />
</pre><br />
eeldades, et on defineeritud member funktsioon<br />
<pre><br />
-m(X,n).<br />
m(X,c(X,Y)).<br />
X=Z | m(X,Y) | -m(X,c(Z,Y)).<br />
-m(X,Y) | m(X,c(Z,Y)).<br />
</pre><br />
Ja Otteri jaoks ära unusta ka lisada aksioomi<br />
<pre><br />
X=X<br />
</pre><br />
<br />
Tõestuse jaoks on vaja kasutada induktsiooni, st tõestada nii<br />
induktsiooni baas<br />
<pre><br />
All y Exists z All u ((m(u,n) & m(u,y)) <=> m(u,z))<br />
</pre><br />
kui induktsiooni samm<br />
<pre><br />
All x ((All y Exists z All u ((m(u,x) & m(u,y)) <=> m(u,z))) <br />
=><br />
(All h All y1 Exists z1 All u1 ((m(u1,c(h,x)) & m(u1,y1)) <br />
<=> m(u1,z1)))<br />
</pre><br />
<br />
<br />
<br />
<br />
== 2013 aasta loengute materjalid ==<br />
<br />
# [[Media:RakLoogika_1_tz_tt.ppt|Sissejuhatus, süntaks, semantika (ppt)]] <br><br />
# [[Media:RakLoogika_2_tz_tt.ppt|Resolutsioonimeetod ja DPLL lausearvutuses (ppt)]] <br><br />
# DPLL tehnoloogia: hea väga detailne kolmeosaline loengukomplekt Eugene Goldbergilt: [http://eigold.tripod.com/presentations/Lecture1.zip loeng1], [http://eigold.tripod.com/presentations/Lecture1.zip loeng2],[http://eigold.tripod.com/presentations/Lecture1.zip loeng3]<br />
<br />
== Vanad 2012 aasta loengute materjalid ==<br />
<br />
# [http://www.tud.ttu.ee/~zingel/RakLoogika_1.ppt Meeldetuletus lausearvutusest. (ppt)] <br><br />
# [http://www.tud.ttu.ee/~zingel/RakLoogika_2.ppt Meeldetuletus predikaatarvutusest. (ppt)] <br><br />
# [[Sekventsarvutus.]]<br />
# [[Tõestuseotsingu strateegiad.]] <br><br />
# [[Media:RakLoogika_7.ppt|Unifitseerimine. (ppt)]] <br><br />
# [[Sissejuhatus automaattõestamisse.]] <br><br />
# [[Media:RakLoogika_5_2.ppt|Davis-Putnami meetod. (ppt)]] <br><br />
# [[Media:RakLoogika_5_1.ppt|Resolutsioonimeetod lausearvutuses. (ppt)]]<br><br />
# [[Media:RakLoogika_8.ppt|Resolutsioonimeetod predikaatarvutuses. (ppt).]]<br><br />
# [[Media:RakLoogika_10.ppt|Resolutsioonistrateegiad. (ppt)]]<br><br />
# [[Media:RakLoogika_9.ppt|Võrdusega predikaatarvutus. (ppt)]]<br><br />
# [[Mitteklassikalised loogikad.]] <br><br />
<br />
<br />
== Eelmise aasta kodused ülesanded tutvumiseks: 2012 aasta arhiiv ==<br />
<br />
Kodused ülesanded jagunevad kohustuslikeks ja mittekohustuslikeks. Eksamile pääsemiseks tuleb ära teha kõik kohustuslikud ülesanded ja 50% mittekohustuslikest ülesannetest. Tehes rohkem kui 50% mittekohustuslikest ülesannetest, on võimalik saada boonuspunkte, mis lähevad arvesse eksamihindes.<br />
<br />
[[Kodused ülesanded 1]]: tähtaeg 9.märts 2012 <br />
<br />
[[Media:RLSKodu2.pdf|Kodused ülesanded 2]]: tähtaeg 23.märts 2012<br />
<br />
[[Media:RLSülesanded3.pdf|Kodused ülesanded 3]]: tähtaeg 4.mai 201<br />
<br />
[[Media:Vastused.pdf|Lahendused]]<br />
<br />
[[Kodutööde punktid]]<br />
<br />
<br />
[[Kohustuslik kodune ülesanne 1]] : tähtaeg 20.aprill 2012<br />
<br />
[[Kohustuslik kodune ülesanne 2]] : tähtaeg 18.mai 2012</div>
Tammet