Rakendusliku loogika süvakursus: erinevus redaktsioonide vahel
Resümee puudub |
|||
| 43. rida: | 43. rida: | ||
9. mai: predikaatarvutuse tõestajatega eksperimenteerimine. | 9. mai: predikaatarvutuse tõestajatega eksperimenteerimine. | ||
== | |||
== 2013 aasta loengute materjalid (jooksvalt täiendatakse) == | |||
# [http://www.tud.ttu.ee/~zingel/RakLoogika_1.ppt Meeldetuletus lausearvutusest. (ppt)] <br> | |||
# [http://www.tud.ttu.ee/~zingel/RakLoogika_2.ppt Meeldetuletus predikaatarvutusest. (ppt)] <br> | |||
# [[Sekventsarvutus.]] | |||
# [[Tõestuseotsingu strateegiad.]] <br> | |||
# [[Media:RakLoogika_7.ppt|Unifitseerimine. (ppt)]] <br> | |||
# [[Sissejuhatus automaattõestamisse.]] <br> | |||
# [[Media:RakLoogika_5_2.ppt|Davis-Putnami meetod. (ppt)]] <br> | |||
# [[Media:RakLoogika_5_1.ppt|Resolutsioonimeetod lausearvutuses. (ppt)]]<br> | |||
# [[Media:RakLoogika_8.ppt|Resolutsioonimeetod predikaatarvutuses. (ppt).]]<br> | |||
# [[Media:RakLoogika_10.ppt|Resolutsioonistrateegiad. (ppt)]]<br> | |||
# [[Media:RakLoogika_9.ppt|Võrdusega predikaatarvutus. (ppt)]]<br> | |||
# [[Mitteklassikalised loogikad.]] <br> | |||
== Vanad 2012 aasta loengute materjalid == | |||
# [http://www.tud.ttu.ee/~zingel/RakLoogika_1.ppt Meeldetuletus lausearvutusest. (ppt)] <br> | # [http://www.tud.ttu.ee/~zingel/RakLoogika_1.ppt Meeldetuletus lausearvutusest. (ppt)] <br> | ||
Redaktsioon: 11. veebruar 2013, kell 18:46
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)
- 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.
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