Rakendusliku loogika süvakursus: erinevus redaktsioonide vahel

Allikas: Lambda
Mine navigeerimisribale Mine otsikasti
← Vanem muudatusUuem muudatus →
27. rida: 27. rida:
* [[Prax3: tõestajatega eksperimenteerimine 2015]]
* [[Prax3: tõestajatega eksperimenteerimine 2015]]
* Vabatahtlik [[Prax4: induktiivne tõestus 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 <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.
Vaata kindlasti ka
* [[soovitusi Otteri otsingu suunamiseks]].
* [http://www.cs.miami.edu/~tptp/ TPTP] ja sealt [http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems Problems] ja selle alt leiad ülesannete tõestused ja saad online katsetada hulga eri tõestajatega: eriti head on Vampire ja E.
* [https://www.cs.unm.edu/~mccune/mace2/ 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
<pre>
All x All y Exists z All u ((m(u,x) & m(u,y)) <=> m(u,z))
</pre>
eeldades, et on defineeritud member funktsioon
<pre>
-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)).
</pre>
Ja Otteri jaoks ära unusta ka lisada aksioomi
<pre>
X=X
</pre>
Tõestuse jaoks on vaja kasutada induktsiooni, st tõestada nii
induktsiooni baas
<pre>
All y Exists z All u ((m(u,n) & m(u,y)) <=> m(u,z))
</pre>
kui induktsiooni samm
<pre>
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)))
</pre>


== Loenguteemad ja materjalid  ==
== Loenguteemad ja materjalid  ==

Redaktsioon: 5. veebruar 2015, kell 15:56

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:


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.

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:

  • 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=12212"