arvutiteaduse instituudi lõputööderegister


Kahni algoritmi tõestamine Coq raamistikus
Nimi Raul Redpap
Kokkuvõte Coq on funktsionaalne programmeerimiskeel, mille abil saab kirjutada teoreemide tõestusi.
Töö eesmärk on uurida ja anda ülevaade Coqist ning tõestada Coqis omadus, et Kahni algoritm lõpetab töö iga sisendi puhul ja et tagastatud järjestus on tõepoolest topoloogiline järjestus. Peamiselt keskendutakse formaalse tõestuse loomisele ja tõestustes kasutatavate taktikate kirjeldamisele, kuid antakse ka lühiülevaade Kahni algoritmist ja topoloogilisest järjestusest.
Lõputöö keel eesti
Lõputöö tüüp Bakalaureus - Informaatika
Juhendaja(d) Kalmer Apinis
Kaitsmise aasta 2019
PDF lisad