Rakendusliku loogika süvakursus: erinevus redaktsioonide vahel

Allikas: Lambda
Mine navigeerimisribale Mine otsikasti
← Vanem muudatus
 
(ei näidata sama kasutaja 60 vahepealset redaktsiooni)
1. rida: 1. rida:
Ainekood: ITV0081<br>
Ainekood: ITV0081<br>
Lektor: Tanel Tammet<br>
Lektor: Tanel Tammet<br>
Kontakt: tanel.tammet@ttu.ee, 6203457, TTÜ AK223<br>
Kontakt: tanel.tammet@ttu.ee, 6203457, TTÜ IT-426<br>
Arhiiv: [[ITV0081 arhiiv 2012]]
Arhiiv: [[ITV0081 arhiiv 2014|2013]], [[ITV0081 arhiiv 2012|2012]]




== Eksam ==


== Muutused loengukohas ==
Aeg ja koht (kaks eraldi aega):


Loengud toimuvad nüüd ja edaspidi uues IT majas Akadeemia 15, 4 korrus arvutiteaduse seminariruumis 411.
* 4. juuni, neljapäev, kell 10:00 ruumis <font color="red"><b>ICT-A1</b></font>, ü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 <b>ICT-A2</b> (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 ==
== Koht ja aeg ==


Semester: kevad<br>
Semester: kevad<br>
Hindamine: eksam + praktikumid<br>
Hindamine: 60% eksam + 40% praktikumid<br>. Kolm kohustuslikku praktikumi, üks valikuline.
Loengud: iga esmaspäev kell  17:45-19:15 ruumis IT-140<br>
Loengud: iga neljapäev kell  12:00-13:30 ruumis IT-A2<br>
Praktikumid: neljapäeviti paarisnädalatel kell 16:00-17:30 ruumis IT-213D, IT-213H.<br>
Praktikumid: neljapäeviti paarisnädalatel kell 10:00-11:30 ruumis IT-637<br>


== Soovitatav kirjandus:==


==Soovitatav kirjandus:==
* T.Tamme, T.Tammet, R.Prank.  [http://dspace.utlib.ee/dspace/bitstream/handle/10062/24397/9985562313.pdf Loogika: mõtlemisest tõestamiseni. TÜ Kirjastus, 2002]
* T.Tamme, T.Tammet, R.Prank.  [http://dspace.utlib.ee/dspace/bitstream/handle/10062/24397/9985562313.pdf Loogika: mõtlemisest tõestamiseni. TÜ Kirjastus, 2002]
* [[Media:Geoffreasoningnotes.pdf|Geoff reasoning course notes]]
* [[Media:Geoffreasoningnotes.pdf|Geoff reasoning course notes]]


== Lahendajad testimiseks ==
Test and compare simple propositional solver algorithms:
Latest:
* [http://logictools.org Proper logictools site]
Old versions:
* [http://dijkstra.cs.ttu.ee/~tammet/logictools/proplogic.html Uuem, arenduses versioon]
* [http://dijkstra.cs.ttu.ee/~tammet/proplogic.html Vana versioon]
== 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]].
* 12 või 26 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
[[Media:RakLoogika_1_tz_tt-1.ppt|Loengukonspekt (ppt)]] <br>
=== 2. Resolutsioonimeetod ja DPLL lausearvutuses ===
12. veebruar.
NB! Praktikum kell 10.
[[Media:RakLoogika_2_tz_tt-1.ppt|Loengukonspekt (ppt)]]
Täiendavalt väga detailne kolmeosaline loengukomplekt  Eugene Goldbergilt: [http://eigold.tripod.com/presentations/Lecture1.zip loeng1], [http://eigold.tripod.com/presentations/Lecture2.zip loeng2],[http://eigold.tripod.com/presentations/Lecture3.zip loeng3]


== 2013 aasta kodused ülesanded ==
=== 3. DPLL optimeeringud ja algus: resolutsioonimeetod predikaatarvutuses: põhialgoritm ===


Praktikumide kuupäevad: 14., 28. veebruar, 14., 28. märts, 11., 25. aprill, 9., ja 23. mai.
19. veebruar.


Ülesanded jagunevad kaheks:  
=== 4. Resolutsioonimeetod predikaatarvutuses: põhialgoritm jätkub ===
* käsitsi väikeste ülesannete lahendamine
* tõestajatega eksperimenteerimine mittetriviaalsete ülesannete automaatseks lahendamiseks


=== 1. prax ===
26. veebruar.


14. veebruar: [[lausearvutuse ja lihtsamate predikaatarvutuse ülesannete lahendamine]].
NB! Praktikum kell 10. Esimese ülesannetekomplekti vastuste tähtaeg.


=== 2. prax ===
Vaata kindlasti ka: [http://dijkstra.cs.ttu.ee/~tammet/proplogic.html Test and compare simple propositional solver algorithms]


14. märts: lausearvutuse tõestajatega eksperimenteerimine.
=== 4. Resolutsioonimeetod predikaatarvutuses: põhialgoritm jätkub ===


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


Lihtsam: [[Prax 2: lausearvutuse lahendajatega eksperimenteerimine]]
=== 5. Resolutsioonimeetod predikaatarvutuses: strateegiad ===


Keerulisem: [[Prax 2: lihtsa DPLL lahendaja realiseerimine]]
12. märts


=== 3. prax ===
=== 6. Võrdus predikaatarvutuses ===


9. mai: predikaatarvutuse tõestajatega eksperimenteerimine.
19. märts.


Kaks osa: soendus ja põhiosa.
=== 6. Võrdus predikaatarvutuses jätkub: termiteisendussüsteemid ===


A) Soendus:
26. märts.


1. osa: lihtsad katsed tõestajaga


Geoff:
== <font color="red">Kursuse lõpu-tegevused</font> ==


* lk 36 ülesanded 1,3,4,5,6,8
30. aprill loeng: Tanel jätkab verifitseerimisega.
* lk 43 ülesanne 7: joonista puu
* lk 47 ülesanne 2


Eesti õpik:
7. mai: eelviimane prax.


* lk 319 ülesanne 3
7. mai loeng: Tanel räägib mitte-verifitseerimisrakendustest.


B) Põhiosa: katsed tõestajaga, kus Otter automaatrezhiim ei leia mõistliku
14. mai: Juhan räägib SMT-solveritest
aja jooksul lahendust, vaja on ise proovida eri strateegiaid. Kokku tuleb kaks blokki ülesandeid.
* Esimene blokk ülesandeid: [[Media:Problems.tar.gz‎]]
* 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 <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)
aga lõpuks pead leidma ise fikseeritud strateegia ja piirangud, millega Otter lahenduse leiab.
Vaata kindlasti ka [[soovitusi Otteri otsingu suunamiseks]].


== 2013 aasta loengute materjalid (jooksvalt täiendatakse) ==
21. mai: eksamiülevaade jms.


# [[Media:RakLoogika_1_tz_tt.ppt|Sissejuhatus, süntaks, semantika (ppt)]] <br>
21. mai: viimane prax, hiljemalt selleks ajaks vaja esitada oma tööd!!! Kes on
# [[Media:RakLoogika_2_tz_tt.ppt|Resolutsioonimeetod ja DPLL lausearvutuses (ppt)]] <br>
# DPLL tehnoloogia: hea väga detailne kolmeosaline loengukomplekt  Eugene Goldbergilt: [http://eigold.tripod.com/presentations/Lecture1.zip loeng1], [http://eigold.tripod.com/presentations/Lecture1.zip loeng2],[http://eigold.tripod.com/presentations/Lecture1.zip loeng3]


== Vanad 2012 aasta loengute materjalid ==
== Vanad 2012 aasta loengute materjalid ==
96. rida: 148. rida:




== Eelmise aasta kodused ülesanded tutvumiseks: 2012 aasta arhiiv ==
== Eksam ==
 
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
 
[[Media:RLSKodu2.pdf|Kodused ülesanded 2]]: tähtaeg 23.märts 2012
 
[[Media:RLSülesanded3.pdf|Kodused ülesanded 3]]: tähtaeg 4.mai 201
 
[[Media:Vastused.pdf|Lahendused]]


[[Kodutööde punktid]]
<b>NB! see on näitekirjeldus 2013 eksamist: 2015 eksam tuleb veidi teistsugune</b>


Eksamil on küsimusi kolmest teemast:


[[Kohustuslik kodune ülesanne 1]] : tähtaeg 20.aprill 2012
* 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:
*** [http://dspace.utlib.ee/dspace/bitstream/handle/10062/24397/9985562313.pdf Loogika: mõtlemisest tõestamiseni. TÜ Kirjastus, 2002], semantika ehk mudelite osa & teor tõestamise osa.
*** [[Media:Geoffreasoningnotes.pdf|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.


[[Kohustuslik kodune ülesanne 2]] : tähtaeg 18.mai 2012
* Indekseerimine:
** McCune klassikalise artikli tasemel: [[Media: Mccuneindexing.pdf]]
** Oskus ehitada väikesi discrimination tree indeksipuid (trie termi jaoks).

Viimane redaktsioon: 3. juuni 2015, kell 17:15

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).
Pärit leheküljelt "http://www.lambda.ee/w/index.php?title=Rakendusliku_loogika_süvakursus&oldid=12423"