Rakendusliku loogika süvakursus

Allikas: Lambda
(Ümber suunatud leheküljelt Itv0080)

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


Eksam

Aeg ja koht (kaks eraldi aega):

  • 4. juuni, neljapäev, kell 10:00 ruumis ICT-A1, ülesanded saab samas Ago Lubergi käest (IT maja on esialgu planeeritud SOC-210 asemel, kuna T. Tammet peab olema magistrikaitsmise komisjonis)
  • 11. juuni, neljapäev, kell 10:00 ruumis ICT-A2 (IT-maja)

Eksamiküsimused

Lausearvutus:

  • Ülesanded lahendamiseks DPLL-ga (paar väikest lausearvutuse valemit, mille vastuolulisus või mudel leida käsitsi DPLL algoritmi abil (splitting ja unit propagation), st joonistada otsingupuu)
  • Osata tõestada teoreem 17.5 (muutujateta resolutsioonimeetodi täielikkus) lk 307 Prank, Tamme, Tammeti õpikust.

Predikaatarvutus:

  • Ülesanded lahendamiseks: skolemiseerimine ja normaalkujule viimine.
  • Ülesanded lahendamiseks: unifitseerimine.
  • Ülesanded lahendamiseks: vastuolu tuletamine ilma võrduseta.
  • Ülesanded lahendamiseks: vastuolu tuletamine võrdusega.
  • Ülesanded lahendamiseks: Knuth-Bendixi täielikustamine.

Kõik ülesanded antakse Otteri kujul (muutujad suurte tähtedega) ja vaja on kirjutada välja detailne tõestus, samas otsingut ei ole vaja välja kirjutada. Unifitseerimise juures on vastuseks unifikaator, Knuth-Bendixi puhul on tulemuseks täielikustatud võrduste hulk.

Mõne ülesande juures võib juhtuda, et tõestust ei olegi (ei ole vastuoluline). Sel juhul selgitada, miks ei ole vastuoluline.

Häid linke

https://news.ycombinator.com/item?id=9565577 http://wiremask.eu/hackingweek-2015-reverse-4/

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:

Lahendajad testimiseks

Test and compare simple propositional solver algorithms:

Latest:

Old versions:

Kodused ülesanded

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

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.

Vaata kindlasti ka: Test and compare simple propositional solver algorithms

4. Resolutsioonimeetod predikaatarvutuses: põhialgoritm jätkub

5. märts.

5. Resolutsioonimeetod predikaatarvutuses: strateegiad

12. märts

6. Võrdus predikaatarvutuses

19. märts.

6. Võrdus predikaatarvutuses jätkub: termiteisendussüsteemid

26. märts.


Kursuse lõpu-tegevused

30. aprill loeng: Tanel jätkab verifitseerimisega.

7. mai: eelviimane prax.

7. mai loeng: Tanel räägib mitte-verifitseerimisrakendustest.

14. mai: Juhan räägib SMT-solveritest

21. mai: eksamiülevaade jms.

21. mai: viimane prax, hiljemalt selleks ajaks vaja esitada oma tööd!!! Kes on

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:

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