Rakendusliku loogika süvakursus: erinevus redaktsioonide vahel
| 46. rida: | 46. rida: | ||
== 2013 aasta loengute materjalid (jooksvalt täiendatakse) == | == 2013 aasta loengute materjalid (jooksvalt täiendatakse) == | ||
# [[Media:RakLoogika_1_tz_tt.ppt|Sissejuhatus, | # [[Media:RakLoogika_1_tz_tt.ppt|Sissejuhatus, süntaks, semantika (ppt)]] <br> | ||
# [[Media:RakLoogika_2_tz_tt.ppt|Resolutsioonimeetod ja DPLL lausearvutuses (ppt)]] <br> | # [[Media:RakLoogika_2_tz_tt.ppt|Resolutsioonimeetod ja DPLL lausearvutuses (ppt)]] <br> | ||
Redaktsioon: 11. veebruar 2013, kell 18:50
Ainekood: ITV0081
Lektor: Tanel Tammet
Kontakt: tanel.tammet@ttu.ee, 6203457, TTÜ AK223
Arhiiv: ITV0081 arhiiv 2012
Koht ja aeg
Semester: kevad
Hindamine: eksam + praktikumid
Loengud: iga esmaspäev kell 17:45-19:15 ruumis IT-140
Praktikumid: neljapäeviti paarisnädalatel kell 16:00-17:30 ruumis IT-213D, IT-213H.
Soovitatav kirjandus:
- T.Tamme, T.Tammet, R.Prank. Loogika: mõtlemisest tõestamiseni. TÜ Kirjastus, 2002
- Geoff reasoning course notes
2013 aasta kodused ülesanded
Praktikumide kuupäevad: 14., 28. veebruar, 14., 28. märts, 11., 25. aprill, 9., ja 23. mai.
Ülesanded jagunevad kaheks:
- käsitsi väikeste ülesannete lahendamine
- tõestajatega eksperimenteerimine mittetriviaalsete ülesannete automaatseks lahendamiseks
1. prax
14. veebruar: lausearvutuse ja lihtsamate predikaatarvutuse ülesannete lahendamine.
2. prax
14. märts: lausearvutuse tõestajatega eksperimenteerimine.
3. prax
11. aprill: predikaatarvutuse ülesannete lahendamine.
4. prax
9. mai: predikaatarvutuse tõestajatega eksperimenteerimine.
2013 aasta loengute materjalid (jooksvalt täiendatakse)
Vanad 2012 aasta loengute materjalid
- Meeldetuletus lausearvutusest. (ppt)
- Meeldetuletus predikaatarvutusest. (ppt)
- Sekventsarvutus.
- Tõestuseotsingu strateegiad.
- Unifitseerimine. (ppt)
- Sissejuhatus automaattõestamisse.
- Davis-Putnami meetod. (ppt)
- Resolutsioonimeetod lausearvutuses. (ppt)
- Resolutsioonimeetod predikaatarvutuses. (ppt).
- Resolutsioonistrateegiad. (ppt)
- Võrdusega predikaatarvutus. (ppt)
- Mitteklassikalised loogikad.
Eelmise aasta kodused ülesanded tutvumiseks: 2012 aasta arhiiv
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.
Kodused ülesanded 1: tähtaeg 9.märts 2012
Kodused ülesanded 2: tähtaeg 23.märts 2012
Kodused ülesanded 3: tähtaeg 4.mai 201
Kohustuslik kodune ülesanne 1 : tähtaeg 20.aprill 2012
Kohustuslik kodune ülesanne 2 : tähtaeg 18.mai 2012