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.
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