ITV0081 arhiiv 2014

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

See on 2013 aasta arhiiv, mitte käimasoleva kursuse materjalid!

Eksamiajad:

• Reede, 24 mai kell 10:00 ruumis X-310 (majanduse maja). Seejuures:
  • 10:00 kodutööde esitamine
  • 11:00 eksam

• Kolmapäev, 5. juuni kell 10:00 ruumis X-210 (majanduse maja). Seejuures:
  • 10:00 kodutööde esitamine
  • 11:00 eksam

Eksamil on küsimusi kolmest teemast:

• Lausearvutus:
  • Lausearvutuse semantika (tõeväärtustabelid)
  • DPLL: oskus teha väikest näidet käsitsi. Liigagi põhjalikud materjalid ntx siit: Media:SatLecture1.ppt, Media:SatLecture2.ppt,Media:SatLecture3.ppt
• Predikaatarvutus:
  • Arusaamine järgmiste materjalide tasemel:
    • Loogika: mõtlemisest tõestamiseni. TÜ Kirjastus, 2002, semantika ehk mudelite osa & teor tõestamise osa.
    • Geoff reasoning course notes
    • Võrdus Media:Equality_lecture15.ppt ja Media:Rewritesystems.pdf‎
  • Oskus teha resolutsioonimeetodi ülesandeid: unifitseerimine ja väikeste näidete lahendamine, seejuures baasstrateegiad.
  • Oskus kodeerida väikesi ülesandeid predikaatarvutusse.

• Indekseerimine:
  • McCune klassikalise artikli tasemel: Media: Mccuneindexing.pdf
  • Oskus ehitada väikesi discrimination tree indeksipuid (trie termi jaoks).

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.

Mida sa pead nende ülesannetega tegema? Leidma Otteriga lahenduse, kusjuures pead ise seadma sellised otsingustrateegiad ja piirangud, et Otter sinu masinas hakkama saaks. Seejuures ei tohi kasutada automaatrezhiimi ja GEO ülesannete juures ei tohi kasutada splittimist. Sa võid küll automaatrezhiimi ja splittimisega katsetada (see on täiesti soovitav) aga lõpuks pead leidma ise fikseeritud strateegia ja piirangud, millega Otter lahenduse leiab. Vaata kindlasti ka

• soovitusi Otteri otsingu suunamiseks.
• TPTP ja sealt Problems ja selle alt leiad ülesannete tõestused ja saad online katsetada hulga eri tõestajatega: eriti head on Vampire ja E.
• Otter

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

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