|
|
Vizualizace rezoluční metody
Smetka, Tomáš ; Orság, Filip (oponent) ; Rozman, Jaroslav (vedoucí práce)
Tato bakalářská práce se zabývá problematikou automatického dokazování ve výrokové a predikátové logice. V teoretické části je popsána výroková a predikátová logika v návaznosti na systém jejich automatického dokazování pomocí rezoluční metody. V práci je dále popsán návrh a implementace programu, který se skládá z terminálu a serverové části. Program hledá důkaz nesplnitelnosti zadané formule a vizualizuje jednotlivé kroky vedoucí k nalezení řešení. V závěru je vyhodnocena implementace řešení a práce jako celek a také jsou popsány další možnosti rozšíření.
|
|
|
Generátor a řešitel hry sudoku
Polínková, Eliška ; Čermák, Martin (oponent) ; Goldefus, Filip (vedoucí práce)
Tato práce pojednává o způsobech generovaní a řešení hry Sudoku. Popisuje možné přístupy k problému řešení, a to: využití logických metod a využití metod prohledávání stavového prostoru. Praktickou část této práce tvoří návrh a implementace aplikace umožňující generování, řešení, ověřování vlastností, vytváření vlastních zadání a export her do formátu XML.
|
|
|
Generátor a řešitel hry sudoku
Polínková, Eliška ; Čermák, Martin (oponent) ; Goldefus, Filip (vedoucí práce)
Tato práce pojednává o způsobech generovaní a řešení hry Sudoku. Popisuje možné přístupy k problému řešení, a to: využití logických metod a využití metod prohledávání stavového prostoru. Praktickou část této práce tvoří návrh a implementace aplikace umožňující generování, řešení, ověřování vlastností, vytváření vlastních zadání a export her do formátu XML.
|
|
|
Vizualizace rezoluční metody
Smetka, Tomáš ; Orság, Filip (oponent) ; Rozman, Jaroslav (vedoucí práce)
Tato bakalářská práce se zabývá problematikou automatického dokazování ve výrokové a predikátové logice. V teoretické části je popsána výroková a predikátová logika v návaznosti na systém jejich automatického dokazování pomocí rezoluční metody. V práci je dále popsán návrh a implementace programu, který se skládá z terminálu a serverové části. Program hledá důkaz nesplnitelnosti zadané formule a vizualizuje jednotlivé kroky vedoucí k nalezení řešení. V závěru je vyhodnocena implementace řešení a práce jako celek a také jsou popsány další možnosti rozšíření.
|
host ::
RSS.