|
|
Simulation of Car Traffic
Gregor, Ivan ; Pudlák, Petr (advisor) ; Hladík, Milan (referee)
This bachelor's thesis describes the main components of the program that simulates the car traffic. It describes the representation of road system, agents, simulation in progress and its output. It also describes several results reached during the simulation of concrete traffic situations. Moreover, the comparison between this program and multiagent systems is included in the end of this thesis. The road system consists of roads and crossroads which are controlled by traffic lights. The user of this program can observe different agent's behaviour. The only condition is that the class that represents an agent implements a uniform interface. The term agent means the car and its driver together. It is autonomous object that moves inside the road system respecting given limits of the simulation. Consequently, behaviour of agents is limited by the simulation rules. Agents are possibly controlled by simulation in order to avoid collisions and not to break traffic rules. The output of the simulation is used to compare the successfulness of individual strategies of agents in terms of length of the drive or fuel usage.
|
|
|
Typed Functional Genetic Programming
Křen, Tomáš ; Pudlák, Petr (advisor) ; Kubalík, Jiří (referee)
In this thesis is presented design and implementation of a system performing genetic programming in simply typed lambda calculus. Population initialization method based on term generating technique producing typed lambda terms in long normal form is introduced. This method is parameterized by simple search strategy. Several search strategies are presented, such as strategy for systematic generation or strategy corresponding to standard ramped half-and-half method. Another such a strategies called \textit{geometric} strategy is further examined in experiments and shown to have various desirable effects such as improved success rate, lesser time consumption and smaller average term size in comparison with standard ramped half-and-half generating method. Other performance enhancements are proposed and supported by experiments such as eta-normalization of generated individuals and @-tree representation of individuals. Abstraction elimination is utilized to enable use of simple tree- swapping crossover. Powered by TCPDF (www.tcpdf.org)
|
|
|
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...
|
|
|
Mariáš Trainer
Caithaml, Tomáš ; Pudlák, Petr (advisor) ; Majerech, Vladan (referee)
In the present thesis we deal with designing a program to play training games of mariáš (traditional czech card game) against computer. Two three-player versions of this game are considered - volený mariáš and licitovaný mariáš. The program enables to play games in tournament mode simulating the real game as well as in training mode where player can look into opponent's hand, undo moves, replay different variations, get advice from computer and so analyse the game situation. It is possible to extend the program by artificial players and to set up tournament between them. The thesis introduces several implementations of artificial player based on enchanced alfa-beta prunning.
|
|
|
Maintainable type classes for Haskell
Farka, František ; Pudlák, Petr (advisor) ; Křen, Tomáš (referee)
In this thesis we address a long-term maintainability problem in Haskell type class system. In particular we study a possibility of backward-compatible changes in existing class hierarchies. In the first part of the thesis we give a brief overview of the language. The following part summarizes current proposed solutions to the problem and analyzes their properties. Based on this analysis we derive our own language extension proposal. In the penultimate chapter we present several possible applications of the language extension and compare the extension to other solutions. As a part of the thesis we also give a proof-of-concept implementation of the extension for the GHC compiler, which is briefly described in the last part of this thesis. Powered by TCPDF (www.tcpdf.org)
|
|
|
Functional reactive programming for web applications
Smrž, Roman ; Pudlák, Petr (advisor) ; Hric, Jan (referee)
Functional reactive programming provides mechanisms of describing dynamic systems in a declarative and type-safe manner, which is traditional domain of functional languages in general and Haskell, which we use here, in particular. We explore ways, in which it may be applied to programming web applications, specifically, we design a domain specific language intended for writing web pages as a part of a Haskell program, which would generate the actual code served to the client, and enriching them with dynamic content; and also find out to what extent we may broaden the expressive power of such library given certain inherent constraints of the chosen method. In doing so, we utilize the tree-like structure of the HTML page, which is quite suitable to be written as a source code in a programming language and to which we embed additional entities providing the dynamics and interactivity.
|
|
|
Automatic lifting of expressions for typed functional languages
Smrž, Roman ; Pudlák, Petr (advisor) ; Hric, Jan (referee)
In typed functional programming there is often the need for combining pure and monadic (or other effectful) computations, but the required lifting must be done manually by the programmer and may result in cluttered code. This thesis explores ways to allow the compiler to perform this task automat- ically. Several possible approaches are described, where the final one reduces the task to solving a system of linear diophantine equations. Apart from monads, the described method is also considered for the case of applicative functors as another abstraction to represent effectful operations. 1
|
|
|
Maintainable type classes for Haskell
Farka, František ; Pudlák, Petr (advisor) ; Křen, Tomáš (referee)
In this thesis we address a long-term maintainability problem in Haskell type class system. In particular we study a possibility of backward-compatible changes in existing class hierarchies. In the first part of the thesis we give a brief overview of the language. The following part summarizes current proposed solutions to the problem and analyzes their properties. Based on this analysis we derive our own language extension proposal. In the penultimate chapter we present several possible applications of the language extension and compare the extension to other solutions. As a part of the thesis we also give a proof-of-concept implementation of the extension for the GHC compiler, which is briefly described in the last part of this thesis. Powered by TCPDF (www.tcpdf.org)
|
|
|
Typed Functional Genetic Programming
Křen, Tomáš ; Pudlák, Petr (advisor) ; Kubalík, Jiří (referee)
In this thesis is presented design and implementation of a system performing genetic programming in simply typed lambda calculus. Population initialization method based on term generating technique producing typed lambda terms in long normal form is introduced. This method is parameterized by simple search strategy. Several search strategies are presented, such as strategy for systematic generation or strategy corresponding to standard ramped half-and-half method. Another such a strategies called \textit{geometric} strategy is further examined in experiments and shown to have various desirable effects such as improved success rate, lesser time consumption and smaller average term size in comparison with standard ramped half-and-half generating method. Other performance enhancements are proposed and supported by experiments such as eta-normalization of generated individuals and @-tree representation of individuals. Abstraction elimination is utilized to enable use of simple tree- swapping crossover. Powered by TCPDF (www.tcpdf.org)
|
|
|
Functional reactive programming for web applications
Smrž, Roman ; Pudlák, Petr (advisor) ; Hric, Jan (referee)
Functional reactive programming provides mechanisms of describing dynamic systems in a declarative and type-safe manner, which is traditional domain of functional languages in general and Haskell, which we use here, in particular. We explore ways, in which it may be applied to programming web applications, specifically, we design a domain specific language intended for writing web pages as a part of a Haskell program, which would generate the actual code served to the client, and enriching them with dynamic content; and also find out to what extent we may broaden the expressive power of such library given certain inherent constraints of the chosen method. In doing so, we utilize the tree-like structure of the HTML page, which is quite suitable to be written as a source code in a programming language and to which we embed additional entities providing the dynamics and interactivity.
|
guest ::
RSS feed.