Rakendusliku loogika süvakursus: erinevus redaktsioonide vahel
| 67. rida: | 67. rida: | ||
B) Põhiosa: katsed tõestajaga, kus Otter automaatrezhiim ei leia mõistliku | B) Põhiosa: katsed tõestajaga, kus Otter automaatrezhiim ei leia mõistliku | ||
aja jooksul lahendust, vaja on ise proovida eri strateegiaid. Kokku tuleb kaks blokki ülesandeid. | aja jooksul lahendust, vaja on ise proovida eri strateegiaid. Kokku tuleb kaks blokki ülesandeid. | ||
* Esimene blokk ülesandeid: [[Media:Problems.tar.gz]] | * Esimene blokk ülesandeid: [[Media:Problems.tar.gz]]. Mõned neist (ntx ex_1) on lihtsad, ja Otteri automaatrezhiim leiab kiirelt tõestuse. Alustagi lihtsatest. Osad ülesanded on keerulisemad: Otteri automaatrezhiim ei leia mõistliku aja jooksul tõestust. | ||
* Teine blokk: paar täiendavat analoogilist ülesannet aprilli jooksul. | * Teine blokk: paar täiendavat analoogilist ülesannet aprilli jooksul. | ||
Mida sa pead nende ülesannetega tegema? Leidma Otteriga lahenduse, kusjuures pead ise seadma sellised otsingustrateegiad ja piirangud, et Otter sinu masinas hakkama saaks. | Mida sa pead nende ülesannetega tegema? Leidma Otteriga lahenduse, kusjuures pead ise seadma sellised otsingustrateegiad ja piirangud, et Otter sinu masinas hakkama saaks. | ||
Seejuures <b>ei tohi</b> kasutada automaatrezhiimi ja GEO ülesannete juures ei tohi kasutada splittimist. Sa võid küll automaatrezhiimi ja splittimisega katsetada (see on soovitav) | Seejuures <b>ei tohi</b> 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. | aga lõpuks pead leidma ise fikseeritud strateegia ja piirangud, millega Otter lahenduse leiab. | ||
Vaata kindlasti ka | Vaata kindlasti ka | ||
Redaktsioon: 11. aprill 2013, kell 20:18
Ainekood: ITV0081
Lektor: Tanel Tammet
Kontakt: tanel.tammet@ttu.ee, 6203457, TTÜ AK223
Arhiiv: ITV0081 arhiiv 2012
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. Kokku tuleb kaks blokki ülesandeid.
- Esimene blokk ülesandeid: Media:Problems.tar.gz. Mõned neist (ntx ex_1) on lihtsad, ja Otteri automaatrezhiim leiab kiirelt tõestuse. Alustagi lihtsatest. Osad ülesanded on keerulisemad: Otteri automaatrezhiim ei leia mõistliku aja jooksul tõestust.
- Teine blokk: paar täiendavat analoogilist ülesannet aprilli jooksul.
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.
- Otter
2013 aasta loengute materjalid (jooksvalt täiendatakse)
- Sissejuhatus, süntaks, semantika (ppt)
- Resolutsioonimeetod ja DPLL lausearvutuses (ppt)
- DPLL tehnoloogia: hea väga detailne kolmeosaline loengukomplekt Eugene Goldbergilt: loeng1, loeng2,loeng3
Vanad 2012 aasta loengute materjalid
- Meeldetuletus lausearvutusest. (ppt)
- Meeldetuletus predikaatarvutusest. (ppt)
- Sekventsarvutus.
- Tõestuseotsingu strateegiad.
- Unifitseerimine. (ppt)
- Sissejuhatus automaattõestamisse.
- Davis-Putnami meetod. (ppt)
- Resolutsioonimeetod lausearvutuses. (ppt)
- Resolutsioonimeetod predikaatarvutuses. (ppt).
- Resolutsioonistrateegiad. (ppt)
- Võrdusega predikaatarvutus. (ppt)
- 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
Kohustuslik kodune ülesanne 1 : tähtaeg 20.aprill 2012
Kohustuslik kodune ülesanne 2 : tähtaeg 18.mai 2012