Prax3: tõestajatega eksperimenteerimine 2015

Tähtaeg: mai keskpaik.

Kaks varianti valikuks: predikaatarvutuse tõestajatega eksperimenteerimine või predikaatarvutuse tõestaja realiseerimine.

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

predikaatarvutuse tõestaja realiseerimine

Eesmärk ei ole mitte eriti efektiivse ja keerulise tõestaja tegemine, vaid võimalikult arusaadava tõestaja ehitamine, mida saaks kasutada resolutsioonimeetodi selgitamisel ja katsetamisel ning mis sobiks edasiarendamiseks. Konkreetselt oleks hea ehitada tõestada javascriptis saidi http://logictools.org jaoks, sarnaselt seal olevatele lausearvutuse tõestajatele.

Tõestaja realiseerimisel on kaks sobivat teed:

• Kirjutada n.ö. harilik resolutsioonimeetodit kasutav tõestaja.
• Kirjutada nn "saturation-based" tõestaja, mis genereerib predikaatarvutuse valemist suure lausearvutuse valemi, asendades muutujate sisse konstante kõikvõimalikel viisidel, ning siis kasutab lahendamiseks lausearvutuse lahendajat. See on täielik - ja suhteliselt praktiline - meetod juhul, kui sinu predikaatarvutuse valemis ei ole funktsioonisümboleid ja ei ole eksistentsikvantoreid. Näiteks

   p(X) -> r(X)
   p(a)
   p(b)
   -r(b)

genereerib lausearvutuse valemi

   p(a) -> r(a)
   p(b) -> r(b)
   p(a)
   p(b)
   -r(b)