Loogika arvutiteaduses (sügis 2004)

Kood: ITI 0040

Punkte: 3.0

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

Kontrollivorm: eksam

Õppejõud: prof. Tarmo Uustalu, arvutiteaduse instituut

Kontakt: firstname(at)cs.ioc.ee, 620 4250

Tunniplaan:

• loengud: E 8.00-9.30 aud VI-102, esimene loeng 30.8.2004
• harjutused (paaris nädalad): E 10.00-11.30 aud VI-102
• laborid (paaritud nädalad): E 10.00-11.30 ruum IT-213F, esimene laboritund 27.9.2004

• konsultatsioon: T 4.1.2005, 15.00, aud VI-203
• eksam: N 6.1.2005, 9.00-12.00, aud VI-223
• ülesanded: ps.gz, pdf

• konsultatsioon: E 10.1.2005, 15.00, aud VI-203
• eksam: K 12.1.2005, 9.00-12.00, aud VI-223

Loengud, harjutused

Kuupäev	L/H	Teema	Slaidid
E 30.8.	L1	Sissejuhatus kursusesse; lauseloogika süntaks ja semantika	ps.gz,pdf
E 6.9.	L2	Lauseloogika normaalkujud, Hilberti süsteem	ps.gz,pdf
E 6.9.	H1
E 13.9.	L3	Predikaatloogika süntaks ja semantika	ps.gz,pdf
E 20.9.	L4	Predikaatloogika normaalkujud, Hilberti süsteem	ps.gz,pdf
E 20.9.	H2
E 27.9.	L5	Loomulik tuletus	ps.gz,pdf
E 27.9.	P1	Tõestusteredaktor Jape ja loomulik tuletus Jape'is	ps.gz,pdf
E 4.10.	L6	Loomulik tuletus	ps.gz,pdf
E 4.10.	H3
E 11.10.	L7	Sekventsiarvutus
E 11.10.	P2	Sekventsiarvutus Jape'is	ps.gz,pdf
E 18.10.	L8	Semantilised tabelid	ps.gz,pdf
E 18.10.	H4	Kontrolltöö!
E 25.10.	L9	Kontrolltöö analüüs
E 25.10.	P3	Laboriülesanded	ps.gz,pdf
E 1.11.	L10	Aksiomaatilised teooriad	ps.gz,pdf
E 1.11.	H5
E 8.11.	L11	Modaalloogika	ps.gz,pdf
E 8.11.	P4
E 15.11.	L12	(jäi ära)
E 15.11.	H6	(jäi ära)
E 22.11.	L13	Modaalloogika (jätk)	ps.gz,pdf
E 22.11.	P5
E 29.11.	L14	Modaalloogika semantilised tabelid	ps.gz,pdf
E 29.11.	H7	Kontrolltöö!
E 6.12.	L15	Kontrolltöö analüüs; dünaamiline loogika	ps.gz,pdf
E 6.12.	P6
E 13.12.	L16	Dünaamiline loogika (jätk)	ps.gz,pdf
E 13.12.	H8

Lugemist

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

• (esmaselt) R Palm, R Prank. Sissejuhatus matemaatilisse loogikasse. TÜ, 2004. [olemas Ü rmtk, RR]
• R Prank. Matemaatiline loogika ja algoritmiteooria. TÜ, 2004. [olemas TTÜ rmtk, RR]
• T Tamme, T Tammet, R Prank. Loogika: Mõtlemisest tõestamiseni. TÜ, 1997. 2. trükk, 2002. [olemas TTÜ rmtk, RR, EAR, TPÜ rmtk, Tln keskrmtk mitmed eks igas ühes] [läbi müüdud]
• P Lorents. Keel ja loogika. EBS, 2000. [olemas TTÜ rmtk, RR, EAR, TPÜ rmtk, Tln keskrmtk mitmed eks igas ühes, sh TTÜ rmtk õpikute osakonnas 10 eks] [Raamatukoi hind 73.-, viit]

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

• S Reeves, M Clarke. Logic for computer science. Addison Wesley, 1990 . [läbi müüdud, tasuta elektrooniline versioon]

Aga abiks on ka nt:

• J Gallier. Logic for computer science. Wiley & Sons, 1986. [läbi müüdud, tasuta elektrooniline versioon]
• J-Y Girard, Y Lafont, P Taylor. Proofs and types. Cambridge Univ Press, 1989. [läbi müüdud, tasuta elektrooniline versioon]

Tarkvara

• Jape (Yet Another Proof Editor)
• otter

Viiteid

• Eesti Arvutiteaduse Talvekool '05
• Arvutiteaduse teooriapäevad Veskisillal
• Arvutiteaduse teooriaseminar '04/'05

---

Tarmo Uustalu
Viimane uuendus 12.12.2004