Rakendusliku loogika süvakursus

Ainekood: ITV0081
Lektor: Tanel Tammet
Kontakt: tanel.tammet@ttu.ee, 6203457, TTÜ IT-426
Arhiiv: 2013, 2012

Koht ja aeg

Semester: kevad
Hindamine: 60% eksam + 40% praktikumid
. Kolm kohustuslikku praktikumi, üks valikuline. Loengud: iga neljapäev kell 12:00-13:30 ruumis IT-A2
Praktikumid: neljapäeviti paarisnädalatel kell 10:00-11:30 ruumis IT-637

Soovitatav kirjandus:

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

Lahendajad testimiseks

• Test and compare simple propositional solver algorithms

Kodused ülesanded

Esimesed kolm ülesannet on kohustuslikud, neljas on vabatahtlik ja annab potentsiaalselt suure hulga lisapunkte.

• 26. veebruar: käsitsi lausearvutuse ja lihtsamate predikaatarvutuse ülesannete lahendamine.
• 14. märts: lausearvutuse tõestajatega eksperimenteerimine. Vali kas lihtsam variant Prax 2: lausearvutuse lahendajatega eksperimenteerimine või keerukam variant: Prax 2: lihtsa DPLL lahendaja realiseerimine
• Prax3: tõestajatega eksperimenteerimine 2015
• Vabatahtlik Prax4: induktiivne tõestus 2015

Loenguteemad ja materjalid

1. Sissejuhatus. Süntaks ja semantika.

5. veebruar

Loengukonspekt (ppt)

2. Resolutsioonimeetod ja DPLL lausearvutuses

12. veebruar.

NB! Praktikum kell 10.

Loengukonspekt (ppt)

Täiendavalt väga detailne kolmeosaline loengukomplekt Eugene Goldbergilt: loeng1, loeng2,loeng3

3. DPLL optimeeringud ja algus: resolutsioonimeetod predikaatarvutuses: põhialgoritm

19. veebruar.

4. Resolutsioonimeetod predikaatarvutuses: põhialgoritm jätkub

26. veebruar.

NB! Praktikum kell 10. Esimese ülesannetekomplekti vastuste tähtaeg.

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.
    

Eksam

NB! see on näitekirjeldus 2013 eksamist: 2015 eksam tuleb veidi teistsugune

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).