Thesis (Selection of subject)Thesis (Selection of subject)(version: 368)
Thesis details
   Login via CAS
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
 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html