|
|
Deciding Logic with Automata
Hečko, Michal ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
Tato práce se zaměřuje na rozhodování kvantifikované lineární celočíselné aritmetiky pomocí konečných automatů. Představujeme novou implementaci klasické rozhodovací procedury založené na automatech, která podporuje vstupní formát SMT-LIB. Naše souhrnná prezentace vyvinutého nástroje se zaměřuje na různé aspekty a návrhová rozhodnutí, která hrají významnou roli při výkonu implementace. Za hlavní příčinu celkově slabého výkonu rozhodovací procedury označujeme nedostatek uvažování založeného na teorii a uvádíme řadu levných heuristik, které výrazně zvyšují její rychlost. Představujeme také novou reformulace klasické procedury pracující způsobem shora dolů, která umožňuje provádět uvažování založené na teorii již během konstrukce automatů. Náš nástroj také porovnáváme s nejmodernějšími SMT řešiči a ukazujeme, že naše prototypová implementace je srovnatelná a dokonce překonává současný stav techniky.
|
|
|
Resolution Method Visualisation
Smetka, Tomáš ; Orság, Filip (referee) ; Rozman, Jaroslav (advisor)
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.
|
|
|
Resolution Method Visualisation
Kasem, Jakub ; Zbořil, František (referee) ; Rozman, Jaroslav (advisor)
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.
|
|
|
Resolution Method Visualisation
Smetka, Tomáš ; Orság, Filip (referee) ; Rozman, Jaroslav (advisor)
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.
|
guest ::
