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

Ülesanded jagunevad kaheks:

• käsitsi väikeste ülesannete lahendamine
• tõestajatega eksperimenteerimine mittetriviaalsete ülesannete automaatseks lahendamiseks

1. prax

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.

Prax 2: lausearvutuse lahendajatega eksperimenteerimine

Prax 2: lihtsa DPLL lahendaja realiseerimine

3. prax

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

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

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