|
|
Recognition of picture languages
Barták, Jakub ; Plátek, Martin (referee) ; Mráz, František (advisor)
We present a transformation of one-dimensional shrinking restarting automaton concept into two-dimensions. The resulting automaton (called Two-dimensional Restarting Automaton - 2RA) proved to have an interesting closure properties as well as close relation to the class or recognizable languages (REC) which qualify it as a notable member of two-dimensional language hierarchy.
|
|
|
Machine learning of formal languages
Klonfar, Matěj ; Mráz, František (advisor) ; Plátek, Martin (referee)
In the present work I study the task of machine learning of formal languages. The task of the work is to design and implement the program with anyone will be able to study the progress and results of algorithms for learning languages. With this program is possible to run algorithms for learning from examples. Examples could be sets of positive and negative examples of the result languages or sets expressed by teacher who knows the result language. The main task is to design easily extensible application with a view to inserting add-ins without no limits of used representation of learned languages or language complexity.
|
|
|
Learning Restricted Restarting Automata using Genetic Algorithm
Basovník, Stanislav ; Plátek, Martin (referee) ; Mráz, František (advisor)
Restarting automata are linguistically motivated models for language representation. The main goal of this work is to propose a suitable version of restarting automaton for learning from positive and negative samples using genetic algorithms. We also characterize the class of languages accepted by limited context restarting automata with respect to the Chomsky hierarchy. The proposed learning algorithm is compared to two well-known methods for learning languages from positive and negative samples - RPNI and LARS. A tool for learning the restricted version of restarting automaton is developed as a part of this work. Examples of usage and user guide are included in this work.
|
|
|
Compiler generator based on restarting automata
Procházka, Jan ; Plátek, Martin (referee) ; Mráz, František (advisor)
Restarting automata, in their most general form, represent a very strong theoretical model recognizing much wider class of languages than the class of context-free ones. Hence, our goal was to design a tool which for a given restarting automaton (in human-readable format) generates a program computing the meaning of an input text. In order to enable that, this thesis extends the model of restarting automata by adding semantics to its meta-instruction. The resulting program is a compiler-compiler (CCRA) inspired by the tools such as flex or bison. However, the CCRA uses restarting automaton instead of a context-free grammar. The implementation as well as the output are realized in C++ which ensures the compatibility with both Windows and Linux systems.
|
|
|
Verefication of Mathematical Proofs
Pudlák, Petr ; Štěpánek, Petr (advisor) ; Haniková, Zuzana (referee) ; Plátek, Martin (referee)
In this thesis we deal with the problem of automatic proving (or disproving) mathematical conjectures using computer programs (usually called automated theorem provers). We address several issues that are important for a successful utilization of such programs. In Chapter 3 we examine how to store and reuse important pieces of mathematical knowledge in the form of lemmas. We investigate how this process can be automatized, i.e. how a computer can construct and use lemmas without human guidance. The program we develop tries to shorten or to speed up the proofs of several conjectures from a common theory. It repeatedly extracts lemmas from the proofs it has already completed and uses the lemmas to improve the sets of premisses to produce more efficient proofs of the conjectures. In Chapter 4 we develop a new algorithm that tries to construct the optimal sets of premisses for proving and disproving mathematical conjectures. The algorithm semantically analyzes the conjectures and the set of premisses of the given theory to find the optimal subsets of the premisses. The algorithm uses an automated model finder to construct models that serve as counterexamples that guide the algorithm to find the optimal set of premisses. In Chapter 5 we use the algorithm to decide formulae in a wide range of modal systems. We...
|
|
|
Natural Language Processing of Textual Use Cases
Dražan, Jaroslav ; Mencl, Vladimír (advisor) ; Plátek, Martin (referee)
Use cases written in a natural language are usually employed for specifying of functional requirements. The format of a use case is not standardized but use case sentences traditionally adhere to a simple structure and describe actions which are either communication actions (among actors and a designed system), or internal actions. The natural language is used because it is comprehensible for stakeholders and is universal enough to capture most of the requirements but it is difficult to analyze it in an automated way. Vladimír Mencl employed state-of-the-art linguistic tools to extract a behavior of a system under design from textual use cases. The behavior specification is described in form of pro-cases. His work shows that this is possible but he met several issues. In this thesis, we solve some of the issues. We propose an algorithm based on the Mencl's algorithm which allows to process more use cases than the Mencl's one and we describe a metric which evaluate a quality of parse tree. The metric helps to select the best parse tree of a use case step from parse trees generated by different linguistic parsers. It addresses the issue of eliminating an incorrect parse tree returned by a single parser.
|
guest ::
RSS feed.