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: eksam + praktikumid
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

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

1. prax: ülesanded

See ülesanne kehtib 2015 aastal.

26. veebruar

2. prax: lausearvutuse tõestajatega eksperimenteerimine

See ülesanne on näide 2013 aastast, mida lähiajal uuendatakse 2015 aastaks.

Tähtaeg 14. märts:

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

Prax 2: lausearvutuse lahendajatega eksperimenteerimine

Prax 2: lihtsa DPLL lahendaja realiseerimine

3. prax: tõestajatega eksperimenteerimine

See ülesanne on näide 2013 aastast, mida lähiajal uuendatakse 2015 aastaks.

Tähtaeg: mai algus

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 ülesanne on näide 2013 aastast, mida lähiajal uuendatakse 2015 aastaks.

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

Loenguteemad ja materjalid

1. Sissejuhatus. Süntaks ja semantika.

5. veebruar

Loengukonspekt (ppt)

2. Resolutsioonimeetod ja DPLL lausearvutuses

12. veebruar.

Loengukonspekt (ppt)

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

3. Resolutsioonimeetod predikaatarvutuses: põhialgoritm

19. veebruar.

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

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