Original title:
Konstrukce modelů v polynomiální reprezentaci
Translated title:
Konstrukce modelů v polynomiální reprezentaci
Authors:
Blicha, Martin ; Stanovský, David (advisor) ; Surynek, Pavel (referee) Document type: Bachelor's theses
Year:
2015
Language:
eng Abstract:
[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
Institution: Charles University Faculties (theses)
(web)
Document availability information: Available in the Charles University Digital Repository. Original record: http://hdl.handle.net/20.500.11956/81972