Loogika arvutiteaduses (sügis 2009)

Kood: ITT 0040 (asendab endist ainet ITI 0041)

Punkte: 3.5 AP (5.0 EAP)

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 1.9.	L/H1	Sissejuhatus kursusesse; lauseloogika süntaks ja semantika	l1
K 16.9.	L/H2	Lauseloogika normaalkujud, lauseloogika üldkehtivuse lahenduvus; binaarsed otsustusdiagrammid	l2
E 28.9.	L/H3	Lauseloogika Hilberti süsteem	l3
K 30.9.	L/H4	Lauseloogika loomulik tuletus, sekventsiarvutus, korrektsus ja täielikkus	l4
E 5.10.	L/H5	Predikaatloogika süntaks ja semantika	l5
K 7.10.	L/H6	Predikaatloogika prenekskuju ja skolemiseerimine; predikaatloogika üldkehtivuse poollahenduvus + kontrolltöö	l6
E 12.10.	L/H7	Predikaatloogika Hilberti süsteem ja loomulik tuletus	l7
E 19.10.	L/H8	Predikaatloogika sekventsiarvutus, korrektsus ja täielikkus	vt eelm
E 26.10.	L/H9	Aksiomaatilised teooriad; aritmeetika ja selle mittetäielikkus	l9
E 2.11.	L/H10	Modaalloogikate süntaks ja Kripke semantika, modaalloogikate tõlkimine predikaatloogikasse + kontrolltöö	l10
E 9.11.	L/H11	Modaalloogikate Hilberti süsteemid, "korrespondentsiteooria"	l11
E 16.11.	L/H12	Dünaamiline loogika, mittedeterministlike programmide esitamine aktsiooniavaldistega, verifitseerimine teoreemitõestamisega	l12
E 23.11.	L/H13	Teadmiste ja tõekspidamiste loogikad	l13
E 30.11.	L/H14	Ajaloogikad LTL ja CTL^*, süsteemide modelleerimine oleku-üleminekusüsteemidega, verifitseerimine mudelikontrolliga
E 7.12.	L/H15	Intuitsionistlik loogika ja funktsionaalprogrammeerimine + kontrolltöö
E 14.12.	L/H16	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 30.11.2009