Konstrukce modelů v polynomiální reprezentaci
| Thesis title in Czech: | Konstrukce modelů v polynomiální reprezentaci |
|---|---|
| Thesis title in English: | Model building in polynomial representation |
| Academic year of topic announcement: | 2011/2012 |
| Thesis type: | Bachelor's thesis |
| Thesis language: | angličtina |
| Department: | Department of Algebra (32-KA) |
| Supervisor: | doc. RNDr. David Stanovský, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 30.09.2011 |
| Date of assignment: | 20.10.2011 |
| Confirmed by Study dept. on: | 06.12.2011 |
| Date and time of defence: | 07.09.2015 00:00 |
| Date of electronic submission: | 30.07.2015 |
| Date of submission of printed version: | 31.07.2015 |
| Date of proceeded defence: | 07.09.2015 |
| Opponents: | doc. RNDr. Pavel Surynek, Ph.D. |
| Guidelines |
| Problém zní, k dané sadě axiomů v predikátové logice najít (konečný) model.
Cílem práce je navrhnout a implementovat algoritmus, který by hledal modely, jejichž relace a operace jsou reprezentovány pomocí polynomů nad konečnými tělesy. Základní myšlenka je následující. Každé zobrazení na p-prvkové množině lze reprezentovat polynomem nad tělesem Z_p. Pokud symboly daného jazyka reprezentujeme jako polynomy s neznámými koeficienty, axiomy se přeloží na soustavu polynomiálních rovnic nad Z_p. Existence řešení této soustavy je ekvivalentní existenci modelu. Algoritmus bude implementován v nějakém systému, který obsahuje efektivní metody řešení soustav rovnic nad konečnými tělesy (např. Sage), a bude testován na úlohách z knihovny TPTP a porovnán s ostatními systémy na hledání modelů. |
| References |
| M. Kalkbrenner, Solving systems of algebraic equations by using Groebner bases, Proc. of Eurocal 1987, LNCS 378, 282-292.
G. Bard, Algorithms for solving systems of linear and polynomial equations, University of Maryland, 2007. G. Bard, Algebraic cryptanalysis, Springer, 2009. D. Stanovský, Počítačová algebra, Matfyzpress, 2011. K. Claessen, N.� Sörensson, New techniques that improve MACE-style finite model finding, CADE-19, 2003. knihovna TPTP, http://www.tptp.org Sage, http://www.sagemath.org |