Název: Vizualizace rezoluční metody
Překlad názvu: Resolution Method Visualisation
Autoři: Smetka, Tomáš ; Orság, Filip (oponent) ; Rozman, Jaroslav (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2013
Jazyk: cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [cze] [eng]
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í. This bachelor’s thesis deals with problems in the area of automated reasoning in propositional and predicate logic. In the theoretical part the propositional and predicate logic is described in connection with the system of its automatic proving with help of resolution method. Further there is described draft and implementation of a program which consists of a terminal and server part. The program looks for a proof if the given formula is impossible to be solved and visualizes every single step which leads to finding of the solution. In conclusion the implementation of solution and the thesis as a whole is evaluated and there are also described additional possibilities of extension.
Klíčová slova: automatické dokazování; lexikální analýza; predikátová logika; prohledávání stavového prostoru; rezoluční metoda; Robinsonův rezoluční princip; syntaktická analýza; Výroková logika; automated reasoning; lexical analysis; predicate logic; Propositional logic; resolution method; Robinson's resolution principle; state space searching; syntactic analysis

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/54795

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


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