|
|
Systémy pro formální matematiku
Kunčar, Ondřej ; Urban, Josef (advisor) ; Štěpánek, Petr (referee)
Title: Systems for formal mathematics Author: Ondrěj Kuncˇar Department: Dep. of Theoretical Computer Science and Mathematical Logic Supervisor: Mgr. Josef Urban, Ph.D. Supervisor's e-mail address: josef.urban@gmail.com Abstract: The Mizar type system is a relatively sophisticated system as it allows for many properties, such as independent types, attributes, overloading, subty- ping, structures and many others. All these properties make formalization of mathematics more intuitive in Mizar that in other systems. However, there is a need to verify mathematical results formalized in Mizar in other systems, so that belief in consistency of Mizar system is strengthened. Attempts at recon- struction of this type system in other mathematics formalization systems follow directly from this requisite. The present work seeks to reconstruct Mizar type system in HOL Light system. The basic idea here is to represent Mizar types as predicates in this system (HOL Light). The present work also aims at precise description of relevant parts of Mi- zar type system. The thesis concludes by reviewing some of the insights that were arrived at in the course of designing and implementing suggested reconstruction. Keywords: type system, Mizar, HOL Light 1
|
|
|
Systems for formal mathematics
Kunčar, Ondřej ; Štěpánek, Petr (referee) ; Urban, Josef (advisor)
The Mizar type system is a relatively sophisticated system as it allows for many properties, such as independent types, attributes, overloading, subtyping, structures and many others. All these properties make formalization of mathematics more intuitive in Mizar that in other systems. However, there is a need to verify mathematical results formalized in Mizar in other systems, so that belief in consistency of Mizar system is strengthened. Attempts at reconstruction of this type system in other mathematics formalization systems follow directly from this requisite. The present work seeks to reconstruct Mizar type system in HOL Light system. The basic idea here is to represent Mizar types as predicates in this system (HOL Light). The present work also aims at precise description of relevant parts of Mizar type system. The thesis concludes by reviewing some of the insights that were arrived at in the course of designing and implementing suggested reconstruction.
|
|
|
THE REDUCTION OF SIGNAL DYNAMIC IN ORTHOGONAL FREQUENCY DIVISION MULTIPLEX SYSTEMS
Urban, Josef ; Lúč, Andrej (referee) ; Galajda,, Pavol (referee) ; Maršálek, Roman (advisor)
This doctoral thesis is focused into the area of multicarrier radio communications systems. These systems are perspective for current and incoming mobile communications and wireless networks. Advantages of multicarrier systems like better multipath propagation resistivity are redeemed by some disadvantages. The high peak to average power ratio of transmitted signal belongs to these disadvantages, for its inconvenience for high efficient power amplification. The thesis concerns with peak to average power ratio reduction methods for OFDM systems, that belongs to the most used multicarrier systems. One of the main objectives is the modification of the existing methods with the intention of complexity reduction. Following subject of interest is the analysis of suitable methods combinations possibilities for more significant peak to average power ratio reduction. One part of this thesis is research of influence of these methods on the OFDM signals with different parameters.
|
|
|
Multicarrier modulator and demodulator for software defined radio
Klučka, Jaroslav ; Urban, Josef (referee) ; Maršálek, Roman (advisor)
This thesis deals with computer simulation of the communication chain using the OFDM modulation. In the beginning of my thesis there is a brief description of digital modulations, especially OFDM. The model of the transmitter, radio channel and receiver, including a simple timing and frequency synchronization and equalization is designed and simulated in the Matlab environment. There is a designed communication system implemented into USRP development board in the Simulink environment. The development board could not work simultaneously as a transmitter and as a receiver. Function of the transmitter was verified by measuring on spectrum analyzer. Testing OFDM signal using the arbitrary waveform generator CompuGen 4302 was generated for the verification of the function of the receiver. Testing signal was received and demodulated on the development board which works as a receiver.
|
|
|
OFDM demodulator implementation in FPGA
Solar, Pavel ; Urban, Josef (referee) ; Maršálek, Roman (advisor)
The master's thesis briefly analyses the principle of OFDM modulation, possibilities of the synchronization and channel estimation in OFDM. The simply model of OFDM system is made in MATLAB. Because of the implementation in FPGA is generated the behavioral description of the OFDM demodulator through the combination of the schematics description and the description in the VHDL language. The ISE development environment is used.
|
|
|
PAPR reduction in OFDM and simulation in Scilab
Maňák, David ; Maršálek, Roman (referee) ; Urban, Josef (advisor)
Main goal of this dissertation is read over principal and properties of the OFDM modulation. Onward we become acquainted with basic methods for PAPR dynamics reduction in OFDM such as Clipping or Interleaving. Simulation of reduction methods will be realized in Scilab environment, in which are made basic functions for OFDM modulator and demodulator. Furthermore there are created functions for PAPR reduction methods. All established functions are implemented in the GUI.
|
|
|
GSM alarm for motorcycles
Beníček, Martin ; Fedra, Zbyněk (referee) ; Urban, Josef (advisor)
The main target of this work is to design and to implement unfailable safety appliance for motocycles with use any GSM technology. In my masters’s thesis I applied to individaul fields which I had to knows for realization of this work. The introductory chapter tells the reader about evaluation of former semestral projects and about brief description of the realized mechanism. It is followed by descripctoin of principles of communication between PC and mobile phone. The main part of my work is dedicated to application itself. The applicaton is called motoalarm. The last chapter creates description service of localisation mobil phones which is called Kde je... The conclusion includes evaluation of this master´s project and general description of the realized mechanism.
|
|
| |
|
|
The response of selected potato varieties to plant density
URBAN, Josef
The aim of my diploma thesis was to evaluate four densities of growth by chosen varieties of potatoes. The thesis deals with the experiment on 4 different varieties of potatoes. I have chosen the standard technology of growing ware potatoes. The selected densities of growth were 35 000, 40 000, 45 000 and 50 000 young plants ha-1. Each variant was repeated four times. I have evaluated the yield of bulbs, the share and yield of ware bulbs, the average number of bulbs for one plant, the weight of bulbs for one plant, the average weight of a bulb and the average weight of ware bulbs. The research was done on a private farm like the field experiment. The farm is located in potato-growing area in Vysočina Region, 490 metres above the sea level. Potatoes are grown approximately over 7 hectares on the farm. The experiment started in 2010. The potato planter MARS 42 was used for the planting. The distance between drills was 0,75 metre. Parcels consisted of 4 drills, each drill equals one repetition, each parcel equals one density of growth. On purchase of samples was realized the kickoff of 10 plants from each repetition. What followed was division of bulbs according to their size in each sample. They were divided into bulbs smaller than 40 millimetres and bigger. After that the samples were weighed and bulbs were counted. The number of bulbs and the weight of bulbs are very important for subtotal. It was established the variety Mirage made the best results when the density was 45 000 plants ha-1. The variety Agria had two suitable densities of growth, namely 40 000 and 45 000 plants ha-1. There was no considerable difference between them. In contrast with previous, the varieties Victoria and Marabel made the best result when the density was 35 000 plants ha-1. I have realized the density 50 000 plants ha-1 is explicitly unsuitable for all varieties. This density of growth is loss-making especially because of lowering of all assessed indexes. Another disadvantage is higher costs (more bulbs are required) and then there is also bigger risk of diseases and pests.
|
|
| |
guest ::
RSS feed.