Kood: ITI 0041
Punkte: 3.5
Nädalatunde: 4, sh loenguid 3, harjutusi 1
Kontrollivorm: eksam
Õppejõud: prof. Tarmo Uustalu, arvutiteaduse instituut
Kontakt: firstname(at)cs.ioc.ee, 620 4250
Tunniplaan:
Kuupäev | L/H | Teema | Slaidid |
---|---|---|---|
E 1.9. | L/H1 | Sissejuhatus kursusesse; lauseloogika süntaks ja semantika | l1 |
E 8.9. | L/H2 | Lauseloogika normaalkujud, lauseloogika üldkehtivuse lahenduvus; binaarsed otsustusdiagrammid | l2 |
E 15.9. | L/H3 | Lauseloogika Hilberti süsteem | l3 |
E 22.9. | L/H4 | Lauseloogika loomulik tuletus, sekventsiarvutus, korrektsus ja täielikkus | l4 |
E 29.9. | L/H5 | Predikaatloogika süntaks ja semantika | l5 |
E 6.10. | L/H6 | Predikaatloogika prenekskuju ja skolemiseerimine; predikaatloogika üldkehtivuse poollahenduvus | l6 |
E 13.10. | L/H7 | Predikaatloogika Hilberti süsteem ja loomulik tuletus + kontrolltöö | l7-8 |
E 20.10. | L/H8 | Predikaatloogika sekventsiarvutus, korrektsus ja täielikkus | vt eelm |
E 27.10. | L/H9 | Aksiomaatilised teooriad; aritmeetika ja selle mittetäielikkus | l9 |
E 3.11. | L/H10 | Modaalloogikate süntaks ja Kripke semantika, modaalloogikate tõlkimine predikaatloogikasse | l10 |
E 10.11. | L/H11 | Modaalloogikate Hilberti süsteemid, "korrespondentsiteooria" | l11 |
E 17.11. | L/H12 | Dünaamiline loogika, mittedeterministlike programmide esitamine aktsiooniavaldistega, verifitseerimine teoreemitõestamisega + kontrolltöö | l12 |
E 24.11. | L/H13 | (üle viidud T 9.12.) | |
E 1.12. | L/H14 | Hoare'i loogika |   |
E 8.12. | L/H15 | Teadmiste ja tõekspidamiste loogikad | l15 |
T 9.12. kl 10-13.30 |
L/H13 | Ajaloogikad LTL ja CTL*, süsteemide modelleerimine oleku-üleminekusüsteemidega, verifitseerimine mudelikontrolliga | l13 |
E 15.12. | L/H16 | Kordamine + kontrolltöö |
Eestikeelne kirjandus: Täpselt sobivat ei ole, aga abiks on:
Võõrkeelne kirjandus: Kõige sobivam on:
Aga abiks on ka nt:
Matemaatilisemad: