Název: Vizualizace rezoluční metody
Překlad názvu: Resolution Method Visualisation
Autoři: Kasem, Jakub ; Zbořil, František (oponent) ; Rozman, Jaroslav (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2023
Jazyk: slo
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [slo] [eng]
Táto bakalárska práca je zameraná na problematiku automatizovaného dokazovania pomocou rezolučnej metódy. Teoretická časť práce je zameraná na predikátovú logiku, jej operácie a zákony, rezolučnú metódu a jej procesy, prehľadávanie stavového priestoru neinformovanými algoritmami a nástroje pre programovanie automatického dokazovania. Práca ďalej popisuje implementáciu výučbovej aplikácie vizualizujúcej rezolučnú metódu. Aplikácia automaticky dokazuje pravdivosť daného výroku hľadaním sporu medzi negáciou výroku a množinou predpokladov a odkrýva postup riešenia. V závere práce je zhodnotená implementácia riešenia i obsah práce a sú navrhnuté možné vylepšenia. This bachelor thesis is focused on the topic of automated reasoning using the resolution method. The theoretical part of the thesis focuses on predicate logic, its operations and laws, the resolution method and its processes, state space search by uninformed algorithms, and tools for automated reasoning programming. The thesis further describes the implementation of a educational application visualizing the resolution method. The application automatically proves the truth value of a given statement by finding a contradiction between the negation of the statement and the set of premises and reveals the solution procedure. In the conclusion of the thesis, the implementation of the solution and the content of the work are evaluated and possible improvements are suggested.
Klíčová slova: Automated reasoning; breadth-first search strategy; clausal form; clause; depth-first search strategy; educational application.; formula; predicate logic; resolution inference rule; resolution method; state space

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: http://hdl.handle.net/11012/211044

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-529321


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Bakalářské práce