Důkazy pomocí konečných automatů
Thesis title in Czech: | Důkazy pomocí konečných automatů |
---|---|
Thesis title in English: | Proving by finite automata |
Key words: | Walnut, automatická posloupnost, automatické dokazování vět |
English key words: | Walnut, automatic sequence, automated theorem proving |
Academic year of topic announcement: | 2016/2017 |
Thesis type: | diploma thesis |
Thesis language: | čeština |
Department: | Department of Algebra (32-KA) |
Supervisor: | doc. Mgr. Štěpán Holub, Ph.D. |
Author: | hidden - assigned and confirmed by the Study Dept. |
Date of registration: | 03.11.2016 |
Date of assignment: | 29.06.2017 |
Confirmed by Study dept. on: | 10.07.2017 |
Date and time of defence: | 13.09.2017 00:00 |
Date of electronic submission: | 21.07.2017 |
Date of submission of printed version: | 21.07.2017 |
Date of proceeded defence: | 13.09.2017 |
Opponents: | Mgr. Karel Chvalovský, Ph.D. |
Guidelines |
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í. |
References |
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] |
Preliminary scope of work |
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 |
Preliminary scope of work in English |
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 |