Original title: Vizualizace rezoluční metody
Translated title: Resolution Method Visualisation
Authors: Kasem, Jakub ; Zbořil, František (referee) ; Rozman, Jaroslav (advisor)
Document type: Bachelor's theses
Year: 2023
Language: slo
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [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.
Keywords: 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

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/211044

Permalink: http://www.nusl.cz/ntk/nusl-529321


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses