Bakalárska práca
Eliminácia pravidla rezu v sekventovom kalkule LKh
Kód sa aktualizuje v prototype a bakalárska práca sa aktualizuje vo východiskách.
14.2 - 20.2. 2022
- Zobrazovanie a konvertovanie Henkinových konštánt do symbolických výrazov a naopak(funckie sexp->ht,ht->sexp)
- Zjednodušenie konvertovania zo symbolickeho vyrazu do dôkazu pre kvantifikačné pravidlá, tým že stačí zadať menej údajov (súbor mread.rkt)
- V bakalárskej práci v kapitole návrh riešenia v podkapitole eliminácia pravidla rezu doplnenie prípadov pre výrokovologické spojky
- Zefektvínenie výpočtu preorderu indexu formuly pri zobrazení (súbor display.rkt) pridaním počítadla
- Vyjadrenie atomických formúl výlučne pomocou štruktúry Af(môže obsahovať aj formuly ktoré nie su číste narozdiel od štruktúry P), zmena hlavne v súboroch
mread a mwrite, odstránenie hashovacej tabulky pre štruktúru P
21.2 - 27.2. 2022
- Opravenie prípadov redukcie rezu v kapitole návrh riešenia v sekcií redukcia rezu
- Pridanie nových sekcií v návrhu riešenia
- Pridanie funkcií deep replacement pre dôkaz,výraz
28.3 - 6.3
- Pridanie UML diagramu do kapitoly implementácia
- Písanie úvodu do problematiky v kapitole návrh riešenia
- Pridanie nových kapitol s názvami modulov v kapitole implementacia
- Oprava Úvodnej kapitoly
8.3 - 13.3
- Pridanie príkladov pre tablá v kapitole návrh v podkapitole eliminácia rezu
- Pridanie dalších testov pre elimináciu pravidla rezu
- spravenie eliminácie pravidla rezu s kvantifikačnými formulami, kde sú dôkazy regulárne
14.3 - 20.3
- Pridanie kódu do kapitoly implementácia
- Pridanie inverzie rezu do kódu, funkcia cut-inversion
- Otestovanie inverzie rezu
- Pridanie testov pre unarnu inverziu
- Rozpracovanie kváziregularizácie v kóde
- Pridanie odvodzovacích pravidiel pre tablá v kapitole návrh riešenia v podkapitole Eliminácia pravidla rezu
21.3 - 27.3
- Oprava formulacií v implementačnej kapitole pri vysvetľovaní jednotlivých funkcií
- Pridanie testov pre kváziregularizáciu
- Zmena dôkazu v kapitole návrh riešenia v podkapitole vzťah medzi sekventovým kalkulom a tablom
- Implementácia kváziregularizácie v kóde
28.3 - 3.4
- Pridanie vyzobrazenia dôkazu do kapitoly testovanie
- Pridanie možnosti nastavovania nazvov henkinovych konštánt na vstupe
- Otestovanie nastavovania nazvov Henkinovych konstant na vstupe
- Pridanie dalších testov na kváziregularizáciu
- Odstránenie nepotrebných príkladov v časti metóda tabiel
4.4 - 10.4
- Oprava štrukturálnej lemmy a zoslabenia, zosilenia a skrátenia v kapitole návrh riešenia
- Pridanie vysvetlenia k dôkazu v návrhu riešenia v podkapitole vzťah medzi sekventovým kalkulom a tablom
- Pridanie testov pre elimináciu rezu
- Pridanie kódu funkcie eliminate a eliminate/all do implementačnej kapitoly
11.4 - 17.4
- Refraktorovanie súboru debug.rkt
- Oprava vety o inverzii rezu
- Písanie vysvetlenia algoritmu v kapitole návrh riešenia
- Písanie algoritmu kváziregularizácie v návrhu riešnia
18.4 - 25.4
- pridanie nových funkcii do kapitoly implementácia
- začanie písania kapitoly záver
- písanie prípadu redukcie rezu keď je formula vseobecna, v kapitole navrh riesenia v podkapitole redukcia rezu