Loogika arvutiteaduses (sügis 2011)

Kood: ITT 0040 (asendab endist ainet ITI 0041)

Punkte: 5.0 EAP (= 3.5 AP)

Nädalatunde: 4, sh loenguid 2, harjutusi 2

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 29.8.	L/H1	Sissejuhatus kursusesse; lauseloogika süntaks, semantika, üldkehtivuse lahenduvus	pdf
E 5.9.	L/H2	Lauseloogika normaalkujud, lauseloogika Hilberti süsteem (Danel Ahman)	pdf
E 12.9.	L/H3	Lauseloogika loomulik tuletus	pdf
E 19.9.	L/H4	Lauseloogika sekventsiarvutus (Danel Ahman)	pdf
E 26.9.	L/H5	Predikaatloogika süntaks ja semantika	pdf
E 3.10.	L/H6	Predikaatloogika prenekskuju ja skolemiseerimine; predikaatloogika üldkehtivuse mittelahenduvus + kontrolltöö	pdf
E 10.10.	L/H7	Predikaatloogika Hilberti süsteem ja loomulik tuletus	pdf
E 17.10.	L/H8	Predikaatloogika sekventsiarvutus	pdf
E 24.10.	L/H9	Aksiomaatilised teooriad; aritmeetika ja selle aksiomatisatsioonide mittetäielikkus	pdf
E 31.10.	L/H10	Modaalloogikate süntaks ja Kripke semantika, modaalloogikate tõlkimine predikaatloogikasse + kontrolltöö	pdf
E 7.11		EI TOIMU
E 14.11.		EI TOIMU
E 21.11.	L/H11	Modaalloogikate Hilberti süsteemid, "korrespondentsiteooria"	pdf
E 28.11.	L/H12	Dünaamiline loogika, mittedeterministlike programmide esitamine aktsiooniavaldistega, verifitseerimine teoreemitõestamisega	pdf
E 5.12.	L/H13	Ajaloogika LTL, süsteemide modelleerimine oleku-üleminekusüsteemidega, verifitseerimine mudelikontrolliga; teadmiste ja tõekspidamiste loogikad	pdf, pdf
N 8.12 kl 12 (ekstra aeg)	K	Konsultatsioon
E 12.12.	L/H14	Teadmiste ja tõekspidamiste loogikad (jätk) + kontrolltöö
E 19.12. (asendusaeg)	L/H15	Kordamine

Eestikeelne kirjandus: Täpselt sobivat ei ole, aga abiks on:

(esmaselt) R Palm, R Prank. Sissejuhatus matemaatilisse loogikasse. TÜ, 2004. [olemas TTÜ rmtk (12 eks), RR, TLÜ AR]
R Prank. Matemaatiline loogika ja algoritmiteooria. TÜ, 2004. [olemas TTÜ rmtk (12 eks), RR, TLÜ AR]
T Tamme, T Tammet, R Prank. Loogika: Mõtlemisest tõestamiseni., 2. trükk. TÜ, 2002. [olemas TTÜ rmtk, RR, TLÜ AR, Tln keskrmtk] [läbi müüdud]
P Lorents. Keel ja loogika. EBS, 2000. [olemas TTÜ rmtk (10 eks), RR, TLÜ AR] [Raamatukoi]

Võõrkeelne kirjandus: Kõige sobivam on:

S Reeves, M Clarke. Logic for Computer Science. Addison Wesley, 1990. [olemas KübI rmtk] [läbi müüdud, tasuta elektrooniline versioon]

Aga abiks on ka nt:

M R A Huth, M D Ryan. Logic in Computer Science: Modelling and Reasoning about Systems, 2nd ed. Cambridge Univ Press, 2004. [autorite lk] [olemas TTÜ rmtk, KübI rmtk, TLÜ AR] [amazon.co.uk]
R Bornat. Formal Proof and Disproof: An Introduction for Programmers. Oxford Univ Press, 2005. [olemas KübI rmtk] [amazon.co.uk]
M Ben-Ari. Mathematical Logic for Computer Science, 2nd ed. Springer-Verlag, 2001. [autori lk] [olemas TTÜ rmtk, KübI rmtk] [amazon.co.uk]

Matemaatilisemad:

J Gallier. Logic for Computer science. Wiley & Sons, 1986. [olemas KübI rmtk] [läbi müüdud, tasuta elektrooniline uustrükk, 2003]
A Nerode, R A Shore. Logic for Applications, 2nd ed. Springer-Verlag, 2001. [olemas TTÜ rmtk, KübI rmtk] [amazon.co.uk]
D van Dalen. Logic and Structure, 4th ed. Springer-Verlag, 2004. [olemas TTÜ rmtk, KübI rmtk] [amazon.co.uk]
R Lalement. Computation as Logic. Prentice Hall, 1993. [olemas KübI rmtk] [amazon.co.uk]
J-Y Girard, Y Lafont, P Taylor. Proofs and Types. Cambridge Univ Press, 1989. [läbi müüdud, tasuta elektrooniline versioon]

Tarmo Uustalu
Viimane uuendus 28.12.2011