Teek predikaatarvutuse väljendamisülesannete lahenduste kontrollimiseks
Nimi
Siiri Saar
Kokkuvõte
Käesoleva bakalaureusetöö eesmärk on implementeerida teek predikaatarvutuse väljendamisülesannete lahenduste kontrollimiseks.
Teeki kuuluvad meetodid, mis võimaldavad kontrollida, kas sisend, s.t aritmeetika signatuuris σ = <0, 1; +, *; => kujutatud predikaatarvutuse valem, on korrektsel kujul ja kas valem väljendab etteantud predikaati. Valemi süntaktilise korrektsuse hindamiseks kontrollitakse muuhulgas järgnevat: valem sisaldab vaid etteantud signatuuri kuuluvaid konstant-, funktsionaal- ja predikaatsümboleid, valemis esinevad sulud on tasakaalus, lõppvalemis kasutatavad abipredikaadid on eelnevalt defineeritud, abipredikaadi defineerimisel ei kasutata predikaadi tähises vabu muutujaid, mida abipredikaadi valemis ei esine ja vastupidi – abipredikaadi valemis ei esine vabu muutujaid, mida tähises ei ole välja toodud.
Selleks, et kontrollida, kas valem väljendab etteantud predikaati, kasutatakse käesolevas töös kahte meetodit. Tõesuspuu meetodiga üritatakse kindlaks teha, kas sisestatud valem ja õige valem on samaväärsed, teisisõnu, kas nende kahe valemi ekvivalents on samaselt tõene. Kui tõesuspuu meetod ei anna määratud aja jooksul kindlat tulemust, võetakse kasutusele meetod, mis kontrollib, kas kahe valemi tõeväärtused langevad kokku suurel lõplikul hulgal.
Kuigi valemite samaväärsuse kontroll on algoritmiliselt mittelahenduv, võimaldavad arendatud teegi meetodid anda kindla vastuse laia alamhulga ülesannete korral, tõhustades seega praegust predikaatarvutuse väljendamisülesannete lahenduste kontrollimise töökorraldust Tartu Ülikooli matemaatilise loogika kursustel.
Teeki kuuluvad meetodid, mis võimaldavad kontrollida, kas sisend, s.t aritmeetika signatuuris σ = <0, 1; +, *; => kujutatud predikaatarvutuse valem, on korrektsel kujul ja kas valem väljendab etteantud predikaati. Valemi süntaktilise korrektsuse hindamiseks kontrollitakse muuhulgas järgnevat: valem sisaldab vaid etteantud signatuuri kuuluvaid konstant-, funktsionaal- ja predikaatsümboleid, valemis esinevad sulud on tasakaalus, lõppvalemis kasutatavad abipredikaadid on eelnevalt defineeritud, abipredikaadi defineerimisel ei kasutata predikaadi tähises vabu muutujaid, mida abipredikaadi valemis ei esine ja vastupidi – abipredikaadi valemis ei esine vabu muutujaid, mida tähises ei ole välja toodud.
Selleks, et kontrollida, kas valem väljendab etteantud predikaati, kasutatakse käesolevas töös kahte meetodit. Tõesuspuu meetodiga üritatakse kindlaks teha, kas sisestatud valem ja õige valem on samaväärsed, teisisõnu, kas nende kahe valemi ekvivalents on samaselt tõene. Kui tõesuspuu meetod ei anna määratud aja jooksul kindlat tulemust, võetakse kasutusele meetod, mis kontrollib, kas kahe valemi tõeväärtused langevad kokku suurel lõplikul hulgal.
Kuigi valemite samaväärsuse kontroll on algoritmiliselt mittelahenduv, võimaldavad arendatud teegi meetodid anda kindla vastuse laia alamhulga ülesannete korral, tõhustades seega praegust predikaatarvutuse väljendamisülesannete lahenduste kontrollimise töökorraldust Tartu Ülikooli matemaatilise loogika kursustel.
Lõputöö keel
eesti
Lõputöö tüüp
Bakalaureus - Informaatika
Juhendaja(d)
Reimo Palm
Kaitsmise aasta
2017