Název:
Konstrukce modelů v polynomiální reprezentaci
Překlad názvu:
Konstrukce modelů v polynomiální reprezentaci
Autoři:
Blicha, Martin ; Stanovský, David (vedoucí práce) ; Surynek, Pavel (oponent) Typ dokumentu: Bakalářské práce
Rok:
2015
Jazyk:
eng
Abstrakt: [eng][cze] Finite model finding is a problem defined as follows: given a theory in first-order logic, find a finite model of this theory. We present a new ap- proach to finite model finding based on a translation of axioms to a system of multivariate polynomial equation. Existence of a model of given size is then equivalent to an existence of a solution of the system. We prove the correctness of this approach, implement it and compare its performance with current state-of-the-art model finders. 1Hledání konečných modelů je problém definovaný takto: k dané teorii prvořádové logiky najít její konečný model. V této práci předkládáme nový způsob řešení tohoto problému, který je založen na překladu axiomů na sous- tavu polynomiálních rovnic. Existence modelu dané velikosti je pak ekviva- lentní existenci řešení této soustavy. Ukážeme korektnost tohoto přístupu, implementujeme algoritmus založen na tomto přístupu a porovnáme jeho výkon s aktuálně nejlepšími systémy na hledání modelů. 1