Rakendusliku loogika süvakursus

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

Muutused loengukohas

Loengud toimuvad nüüd ja edaspidi uues IT majas Akadeemia 15, 4 korrus arvutiteaduse seminariruumis 411.

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

9. mai: predikaatarvutuse tõestajatega eksperimenteerimine.

Kaks osa: soendus ja põhiosa.

A) Soendus:

1. osa: lihtsad katsed tõestajaga

Geoff:

• lk 36 ülesanded 1,3,4,5,6,8
• lk 43 ülesanne 7: joonista puu
• lk 47 ülesanne 2

Eesti õpik:

• lk 319 ülesanne 3

B) Põhiosa: katsed tõestajaga, kus Otter automaatrezhiim ei leia mõistliku aja jooksul lahendust, vaja on ise proovida eri strateegiaid. Ülesanded: Media:Problems.tar.gz‎. Mõned neist (ntx ex_1) on lihtsad, ja Otteri automaatrezhiim leiab kiirelt tõestuse. Alustagi lihtsatest. Enamik ülesandeid on keerulisemad.

4. prax

See on vabatahtlik praks, mis annab hulgaliselt ekstrapunkte.

Ülesanne on tõestada

All x All y Exists z All u ((m(u,x) & m(u,y)) <=> m(u,z))

eeldades, et on defineeritud member funktsioon

-m(X,n).
m(X,c(X,Y)).
X=Z | m(X,Y) | -m(X,c(Z,Y)).
-m(X,Y) | m(X,c(Z,Y)).

Ja Otteri jaoks ära unusta ka lisada aksioomi

X=X

Tõestuse jaoks on vaja kasutada induktsiooni, st tõestada nii induktsiooni baas

All y Exists z All u ((m(u,n) & m(u,y)) <=> m(u,z))

kui induktsiooni samm

All x ((All y Exists z All u ((m(u,x) & m(u,y)) <=> m(u,z))) 
       <=>
 (All h All y1 Exists z1 All u1 ((m(u1,c(h,x)) & m(u1,y1)) 

<=> m(u1,z1)))

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,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