Důkazy pomocí konečných automatů
| Název práce v češtině: | Důkazy pomocí konečných automatů |
|---|---|
| Název v anglickém jazyce: | Proving by finite automata |
| Klíčová slova: | Walnut, automatická posloupnost, automatické dokazování vět |
| Klíčová slova anglicky: | Walnut, automatic sequence, automated theorem proving |
| Akademický rok vypsání: | 2016/2017 |
| Typ práce: | diplomová práce |
| Jazyk práce: | čeština |
| Ústav: | Katedra algebry (32-KA) |
| Vedoucí / školitel: | doc. Mgr. Štěpán Holub, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 03.11.2016 |
| Datum zadání: | 29.06.2017 |
| Datum potvrzení stud. oddělením: | 10.07.2017 |
| Datum a čas obhajoby: | 13.09.2017 00:00 |
| Datum odevzdání elektronické podoby: | 21.07.2017 |
| Datum odevzdání tištěné podoby: | 21.07.2017 |
| Datum proběhlé obhajoby: | 13.09.2017 |
| Oponenti: | Mgr. Karel Chvalovský, Ph.D. |
| Zásady pro vypracování |
| Student se seznámí s nedávno vyvinutou metodou důkazu vlastností slov pomocí konečných automatů. Metodu vyloží, ilustruje na příkladech a podle zájmu a postupu práce se ji pokusí aplikovat na nová tvrzení. |
| Seznam odborné literatury |
| V. Bruyère, G. Hansel, C. Michaux, R. Villemaire: Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc., 1 (1994), pp. 191-238
Dane Henshall, Jeffrey Shallit: Automatic Theorem-Proving in Combinatorics on Words. arXiv:1203.3758 [cs.FL] Hamoon Mousavi: Automatic Theorem Proving in Walnut. arXiv:1603.06017 [cs.FL] |
| Předběžná náplň práce |
| Zajímavá metoda založená na praktické aplikaci vztahu mezi logickými výroky určitého typu a příslušnou třídou jazyků, v tomto případě regulárních. Jedná se tedy o práci na hranici výpočetní složitosti, logiky a kombinatoriky.
S bonusem, že to "opravdu chodí". Viz baliček Walnut na stránce https://cs.uwaterloo.ca/~shallit/papers.html |
| Předběžná náplň práce v anglickém jazyce |
| An interesting method based on a practical application of the relation between logical expressions of a given type and a corresponding class of languages, in this case regular ones. It is a topic bordering computational complexity, logics and combinatorics.
The bonus is that "it really works": see Wlanut package on https://cs.uwaterloo.ca/~shallit/papers.html |