This thesis deals with the addition of flood protection measures in the Salašský potok basin. Working closely related to the previous bachelor thesis on Flood protection in the Salašský potok basin. Detail deal with left tributary Salašky - Modranský potok -which runs through the town Modrá, to be occupied by 6 small cascade of water reservoirs. The work is divided into two parts. The first part describes the actual parameters of the tanks and their assessment of the possible spill-over and is solved their overall transformational effect in the basin. In the second part of the thesis dealt with the tank as a semi tank in response to N-leté water and searched their design parameters.

This thesis deals with the river basin flood protection Loučka. The goal of the thesis is to assess the need of flood control measures supplement in the watershed. The first part deals with exploration of river basin, acquiring geographic factors and obtaining information about the topic, establishment and application of rainfall model used for solving the problem. The second part deals with improving of flood protection at critical selected places by using design of reservoir system with retention effect and by increasing river basin capacity. For basin schematisation was used ArcGIS program and the simulation of rainfall-runoff process was made by Hydrog program.

This thesis deals with the flood control. In particular, the design of a set of small water reservoirs with retention effect (polders) and their effect on flood flows. The work is divided into two parts, the first part refers to the bachelor thesis. In this thesis is description of the catchment, rainfall-runoff process and the evaluation of the ratio. That was got the necessary information for the design of polders. This is an abbreviated repetition of the contents of the thesis, which is a continuation of this work. The second part deals with the specific design of two reservoirs, including hydro calculations and drawings. For this work were used ArcGIS - ArcMap, Hydrog and to create drawings AutoCAD 2010.

Les schématisations de termes permettent de représenter des ensembles infinis de termes ayant une structure similaire de manière finie et compacte. Dans ce travail, nous étudions certains aspects liés à l'utilisation des schématisations de termes en déduction automatique, plus particulièrement dans les méthodes de démonstration de théorèmes du premier ordre par saturation. Après une brève étude comparée des formalismes de schématisation existants, nous nous concentrons plus particulièrement sur les termes avec exposants entiers (ou I-termes). Dans un premier temps, nous proposons une nouvelle approche permettant de détecter automatiquement des régularités dans les espaces de recherche. Cette détection des régularités peut avoir plusieurs applications, notamment la découverte de lemmes nécessaires à la terminaison dans certaines preuves inductives. Nous présentons DS3, un outil qui implémente ces idées. Nous comparons notre approche avec d'autres techniques de généralisation de termes. Notre approche diffère complètement des techniques existantes car d'une part, elle est complètement indépendante de la procédure de preuve utilisée et d'autre part, elle utilise des techniques de généralisation inductive et non déductives. Nous discutons également les avantages et les inconvénients liés à l'utilisation de notre méthode et donnons des éléments informels de comparaison avec les approches existantes. Nous nous intéressons ensuite aux aspects théoriques de l'utilisation des I-termes en démonstration automatique. Nous démontrons que l'extension aux I-termes du calcul de résolution ordonnée est réfutationnellement complète, que l'extension du calcul de superposition n'est pas réfutationnellement complète et nous proposons une nouvelle règle d'inférence pour restaurer la complétude réfutationnelle. Nous proposons ensuite un algorithme d'indexation (pour une sous-classe) des I-termes, utile pour le traitement des règles de simplification et d'élimination de la redondance. Finalement nous présentons DEI, un démonstrateur automatique de théorèmes capable de gérer directement des formules contenant des I-termes. Nous évaluons les performances de ce logiciel sur un ensemble de benchmarks. / Term schematisations allow one to represent infinite sets of terms having a similar structure by a finite and compact form. In this work we study some issues related to the use of term schematisation in automated deduction, in particular in saturation-based first-order theorem proving. After a brief comparative study of existing schematisation formalisms, we focus on terms with integer exponents (or I-terms). We first propose a new approach allowing to automatically detect regularities (obviously not always) on search spaces. This is motivated by our aim at extending current theorem provers with qualitative improvements. For instance, detecting regularities permits to discover lemmata which is mandatory for terminating in some kinds of inductive proofs. We present DS3, a tool which implements these ideas. Our approach departs from existing techniques since on one hand it is completely independent of the proof procedure used and on the other hand it uses inductive generalization techniques instead of deductive ones. We discuss advantages and disadvantages of our method and we give some informal elements of comparison with similar approaches. Next we tackle some theoretical aspects of the use of I-terms in automated deduction. We prove that the direct extension of the ordered resolution calculus is refutationally complete. We provide an example showing that a direct extension of the superposition calculus is not refutationally complete and we propose a new inference rule to restore refutational completeness. We then propose an indexing algorithm for (a subclass of) I-terms. This algorithm is an extension of the perfect discrimination trees that are are employed by many efficient theorem provers to implement redundancy elimination rules. Finally we present DEI, a theorem prover with built-in capabilities to handle formulae containing I-terms. This theorem-prover is an extension of the E-prover developed by S. Schulz. We evaluate the performances of this software on a set of benchmarks.