|
|
Recognition of picture languages
Barták, Jakub ; Mráz, František (advisor) ; Plátek, Martin (referee)
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.
|
|
|
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...
|
|
|
Compiler generator based on restarting automata
Procházka, Jan ; Mráz, František (advisor) ; Plátek, Martin (referee)
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.
|
|
|
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.
|
|
|
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.
|
|
|
Lexicalized Syntactic Analysis by Restarting Automata
Mráz, F. ; Otto, F. ; Pardubská, D. ; Plátek, Martin
We study h-lexicalized two-way restarting automata that can rewrite at most i times per cycle for some i ≥ 1 (hRLWW(i)-automata). This model is considered useful for the study of lexical (syntactic) disambiguation, which is a concept from linguistics. It is based on certain reduction patterns. We study lexical disambiguation through the formal notion of h-lexicalized syntactic analysis (hLSA). The hLSA is composed of a basic language and the corresponding h-proper language, which is obtained from the basic language by mapping all basic symbols to input symbols. We stress the sensitivity of hLSA by hRLWW(i)-automata to the size of their windows, the number of possible rewrites per cycle, and the degree of (non-)monotonicity. We introduce the concepts of contextually transparent languages (CTL) and contextually transparent lexicalized analyses based on very special reduction patterns, and we present two-dimensional hierarchies of their subclasses based on the size of windows and on the degree of synchronization. The bottoms of these hierarchies correspond to the context-free languages. CTL creates a proper subclass of context-sensitive languages with syntactically natural properties.
|
|
|
Hierarchical Modeling of Planning Problems
Dvořák, Tomáš ; Barták, Roman (advisor) ; Plátek, Martin (referee)
Automated planning is a task to find a sequence of actions leading from an initial state to a desired goal state. There is a lot of formal models for planning problems modeling. The class of hierarchical formal models is one of them. In this thesis we will propose a hierarchical model, called GramPlan, based on attribute grammars. We will present some methods to reduce classical STRIPS formalism to GramPlan and we will prove the correctness of this reduction. Also we will present reduction of the FlowOpt workflow model to GramPlan and we will prove it's correctness. We will desing a couple of verification methods for attribute grammars and we will show these methods are equivalent. Powered by TCPDF (www.tcpdf.org)
|
|
|
Reducing Automata and Syntactic Errors
Procházka, Martin ; Plátek, Martin (advisor) ; Pardubská, Dana (referee) ; Průša, Daniel (referee)
This thesis deals with reducing automata, their normalization, and their application for a (robust) reduction analysis and localization of syntactic errors for deterministic context-free languages (DCFL). A reducing automaton is similar to a restarting automaton with two subtle differences: an explicit marking of reduced symbols (which makes it possible to determine a position of an error accurately), and moving a lookahead window inside a control unit (which brings reducing automata closer to devices of classical automata and formal language theory). In case of reducing automata, it is easier to adopt and reuse notions and approaches developed within classical theory, e.g., prefix correctness or automata minimization. For any nonempty deterministic context-free language specified by a monotone reducing automaton, both prefix correct and minimal, we propose a method of robust analysis by reduction which ensures localization of formally defined types of (real) errors, correct subwords, and subwords causing reduction conflicts (i.e., subwords with ambiguous syntactic structure that can be reduced in different words in different ways). We implement the proposed method by a new type of device (called postprefix robust analyzer) and we briefly show how to implement this method by a deterministic pushdown...
|
|
|
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.
|
guest ::
RSS feed.