Prax3: tõestajatega eksperimenteerimine 2015

NB! 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