Loogika arvutiteaduses (sügis 2013)
NB! Muutunud ruum - ICT-414!
Kood:ITT 0040
Punkte: 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:
- loengud:
E 14.00-15.30 (1., 3., 5., 7.-9., 11.-16. nädal),
R 10.00.-11.30 (1., 3., 8., 11. nädal), IT-maja (Akadeemia tee 15a), ruum 414
- harjutused:
E 16.00-17.30 (1., 3., 5., 7.-9., 11.-16. nädal),
R 12.00-13.30 (1., 3., 8., 11. nädal), IT-maja (Akadeemia tee 15a), ruum 414
- konsultatsioon: R 3.1.2014 kl 16, IT-maja, ruum A2
- eksam: K 8.1.2014 kl 10-13, IT-maja, ruum A2
- eksam: E 13.1.2014 kl 10-13, IT-maja, ruum A2
Loengud, harjutused
| Kuupäev |
L/H |
Teema |
Slaidid |
|---|
| E 2.9. |
L/H1 |
Sissejuhatus kursusesse; lauseloogika
süntaks,
semantika, üldkehtivuse lahenduvus |
pdf |
| R 6.9. |
L/H2 |
Lauseloogika normaalkujud,
lauseloogika Hilberti süsteem |
pdf |
| E 16.9. - I-202 |
|
From electronic brains to ubiquitous computing: recollections and visions of a participating observer (Reino Kurki-Suonio) (TTÜ audoktori loeng) |
|
| R 20.9. |
L/H3 |
Lauseloogika loomulik tuletus |
pdf |
| E 30.9. |
L/H4 |
Lauseloogika sekventsiarvutus |
pdf |
| E 14.10. |
L/H5 |
Predikaatloogika süntaks ja semantika + kontrolltöö |
pdf |
| E 21.10. |
L/H6 |
Predikaatloogika prenekskuju ja skolemiseerimine; predikaatloogika üldkehtivuse mittelahenduvus |
pdf |
| R 25.10. |
L/H7 |
Predikaatloogika Hilberti süsteem ja loomulik tuletus |
pdf |
| E 28.10. |
L/H8 |
Predikaatloogika sekventsiarvutus |
pdf |
| E 11.11. |
L/H9 |
Aksiomaatilised teooriad; aritmeetika ja selle aksiomatisatsioonide mittetäielikkus + kontrolltöö |
pdf |
| R 15.11. |
L/H10 |
Modaalloogikate süntaks ja Kripke semantika, modaalloogikate Hilberti süsteemid |
pdf |
| E 18.11. |
L/H11 |
Modaalloogikate tõlkimine predikaatloogikasse, "korrespondentsiteooria" |
pdf |
| E 25.11. |
L/H12 |
Dünaamiline loogika, mittedeterministlike programmide esitamine aktsiooniavaldistega, verifitseerimine teoreemitõestamisega |
pdf |
| E 2.12. |
L/H13 |
Ajaloogika LTL, süsteemide modelleerimine oleku-üleminekusüsteemidega, verifitseerimine mudelikontrolliga |
pdf |
| E 9.12. |
L/H14 |
Teadmiste ja tõekspidamiste loogikad + kontrolltöö |
pdf |
| E 16.12. |
L/H15 |
Teadmiste ja tõekspidamiste loogikad (jätk) |
|
Lugemist
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:
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]
Viiteid
Tarmo Uustalu
Viimane uuendus 26.11.2013