Rakendusliku loogika süvakursus

Ainekood: ITV0081
Lektor: Tanel Tammet
Kontakt: tanel.tammet@ttu.ee, 6203457, TTÜ AK223
Arhiiv: ITV0081 arhiiv 2012

Koht ja aeg

Semester: kevad
Hindamine: eksam + praktikumid
Loengud: iga esmaspäev kell 17:45-19:15 ruumis IT-140
Praktikumid: neljapäeviti paarisnädalatel kell 16:00-17:30 ruumis IT-213D, IT-213H.

Soovitatav kirjandus:

• T.Tamme, T.Tammet, R.Prank. Loogika: mõtlemisest tõestamiseni. TÜ Kirjastus, 2002
• Geoff reasoning course notes

2013 aasta kodused ülesanded

Praktikumide kuupäevad: 14., 28. veebruar, 14., 28. märts, 11., 25. aprill, 9., ja 23. mai.

Ülesanded jagunevad kaheks:

• käsitsi väikeste ülesannete lahendamine
• tõestajatega eksperimenteerimine mittetriviaalsete ülesannete automaatseks lahendamiseks

1. prax

14. veebruar: lausearvutuse ja lihtsamate predikaatarvutuse ülesannete lahendamine.

2. prax

14. märts: lausearvutuse tõestajatega eksperimenteerimine.

Ülesandel on kaks varianti - lihtsam ja keerulisem - ning võid ise valida, kumbat teed.

Lihtsam: Prax 2: lausearvutuse lahendajatega eksperimenteerimine

Keerulisem: Prax 2: lihtsa DPLL lahendaja realiseerimine

3. prax

11. aprill: predikaatarvutuse ülesannete lahendamine.

4. prax

9. mai: predikaatarvutuse tõestajatega eksperimenteerimine.

2013 aasta loengute materjalid (jooksvalt täiendatakse)

1. Sissejuhatus, süntaks, semantika (ppt)
   
2. Resolutsioonimeetod ja DPLL lausearvutuses (ppt)
   
3. DPLL tehnoloogia: hea väga detailne kolmeosaline loengukomplekt Eugene Goldbergilt: loeng1, loeng2,[http://eigold.tripod.com/presentations/Lecture1.zip loeng3

Vanad 2012 aasta loengute materjalid

1. Meeldetuletus lausearvutusest. (ppt)
   
2. Meeldetuletus predikaatarvutusest. (ppt)
   
3. Sekventsarvutus.
4. Tõestuseotsingu strateegiad.
   
5. Unifitseerimine. (ppt)
   
6. Sissejuhatus automaattõestamisse.
   
7. Davis-Putnami meetod. (ppt)
   
8. Resolutsioonimeetod lausearvutuses. (ppt)
   
9. Resolutsioonimeetod predikaatarvutuses. (ppt).
   
10. Resolutsioonistrateegiad. (ppt)
    
11. Võrdusega predikaatarvutus. (ppt)
    
12. Mitteklassikalised loogikad.
    

Eelmise aasta kodused ülesanded tutvumiseks: 2012 aasta arhiiv

Kodused ülesanded jagunevad kohustuslikeks ja mittekohustuslikeks. Eksamile pääsemiseks tuleb ära teha kõik kohustuslikud ülesanded ja 50% mittekohustuslikest ülesannetest. Tehes rohkem kui 50% mittekohustuslikest ülesannetest, on võimalik saada boonuspunkte, mis lähevad arvesse eksamihindes.

Kodused ülesanded 1: tähtaeg 9.märts 2012

Kodused ülesanded 2: tähtaeg 23.märts 2012

Kodused ülesanded 3: tähtaeg 4.mai 201

Lahendused

Kodutööde punktid

Kohustuslik kodune ülesanne 1 : tähtaeg 20.aprill 2012

Kohustuslik kodune ülesanne 2 : tähtaeg 18.mai 2012