Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.

Text in English with abstracts in English, Afrikaans and isiZulu / The formalisation of first-order logic and axiomatic set theory in the first half of the 20th century—along with the advent of the digital computer—paved the way for the development of automated theorem proving. In the 1950s, the automation of proof developed from proving elementary geometric problems and finding direct proofs for problems in Principia Mathematica by means of simple, human-oriented rules of inference. A major advance in the field of automated theorem proving occurred in 1965, with the formulation of the resolution inference mechanism. Today, powerful Satisfiability Modulo Theories (SMT) provers combine SAT solvers with sophisticated knowledge from various problem domains to prove increasingly complex theorems. The combinatorial explosion of the search space is viewed as one of the major challenges to progress in the field of automated theorem proving. Pioneers from the 1950s and 1960s have already identified the need for heuristics to guide the proof search effort. Despite theoretical advances in automated reasoning and technological advances in computing, the size of the search space remains problematic when increasingly complex proofs are attempted. Today, heuristics are still useful and necessary to discharge complex proof obligations. In 2000, a number of heuristics was developed to aid the resolution-based prover OTTER in finding proofs for set-theoretic problems. The applicability of these heuristics to next-generation theorem provers were evaluated in 2009. The provers Vampire and Gandalf required respectively 90% and 80% of the applicable OTTER heuristics. This dissertation investigates the applicability of the OTTER heuristics to theorem proving in the hybrid theorem proving environment Rodin—a system modelling tool suite for the Event-B formal method. We show that only 2 of the 10 applicable OTTER heuristics were useful when discharging proof obligations in Rodin. Even though we argue that the OTTER heuristics were largely ineffective when applied to Rodin proofs, heuristics were still needed when proof obligations could not be discharged automatically. Therefore, we propose a number of our own heuristics targeted at theorem proving in the Rodin tool suite. / Die formalisering van eerste-orde-logika en aksiomatiese versamelingsteorie in die eerste helfte van die 20ste eeu, tesame met die koms van die digitale rekenaar, het die weg vir die ontwikkeling van geoutomatiseerde bewysvoering gebaan. Die outomatisering van bewysvoering het in die 1950’s ontwikkel vanuit die bewys van elementêre meetkundige probleme en die opspoor van direkte bewyse vir probleme in Principia Mathematica deur middel van eenvoudige, mensgerigte inferensiereëls. Vooruitgang is in 1965 op die gebied van geoutomatiseerde bewysvoering gemaak toe die resolusie-inferensie-meganisme geformuleer is. Deesdae kombineer kragtige Satisfiability Modulo Theories (SMT) bewysvoerders SAT-oplossers met gesofistikeerde kennis vanuit verskeie probleemdomeine om steeds meer komplekse stellings te bewys. Die kombinatoriese ontploffing van die soekruimte kan beskou word as een van die grootste uitdagings vir verdere vooruitgang in die veld van geoutomatiseerde bewysvoering. Baanbrekers uit die 1950’s en 1960’s het reeds bepaal dat daar ’n behoefte is aan heuristieke om die soektog na bewyse te rig. Ten spyte van die teoretiese vooruitgang in outomatiese bewysvoering en die tegnologiese vooruitgang in die rekenaarbedryf, is die grootte van die soekruimte steeds problematies wanneer toenemend komplekse bewyse aangepak word. Teenswoordig is heuristieke steeds nuttig en noodsaaklik om komplekse bewysverpligtinge uit te voer. In 2000 is ’n aantal heuristieke ontwikkel om die resolusie-gebaseerde bewysvoerder OTTER te help om bewyse vir versamelingsteoretiese probleme te vind. Die toepaslikheid van hierdie heuristieke vir die volgende generasie bewysvoerders is in 2009 geëvalueer. Die bewysvoerders Vampire en Gandalf het onderskeidelik 90% en 80% van die toepaslike OTTER-heuristieke nodig gehad. Hierdie verhandeling ondersoek die toepaslikheid van die OTTER-heuristieke op bewysvoering in die hibriede bewysvoeringsomgewing Rodin—’n stelselmodelleringsuite vir die formele Event-B-metode. Ons toon dat slegs 2 van die 10 toepaslike OTTER-heuristieke van nut was vir die uitvoering van bewysverpligtinge in Rodin. Ons voer aan dat die OTTER-heuristieke grotendeels ondoeltreffend was toe dit op Rodin-bewyse toegepas is. Desnieteenstaande is heuristieke steeds nodig as bewysverpligtinge nie outomaties uitgevoer kon word nie. Daarom stel ons ’n aantal van ons eie heuristieke voor wat in die Rodin-suite aangewend kan word. / Ukwenziwa semthethweni kwe-first-order logic kanye ne-axiomatic set theory ngesigamu sokuqala sekhulunyaka lama-20—kanye nokufika kwekhompyutha esebenza ngobuxhakaxhaka bedijithali—kwavula indlela ebheke ekuthuthukisweni kwenqubo-kusebenza yokufakazela amathiyoremu ngekhomyutha. Ngeminyaka yawo-1950, ukuqinisekiswa kobufakazi kwasuselwa ekufakazelweni kwezinkinga zejiyomethri eziyisisekelo kanye nasekutholakaleni kobufakazi-ngqo bezinkinga eziphathelene ne-Principia Mathematica ngokuthi kusetshenziswe imithetho yokuqagula-sakucabangela elula, egxile kubantu. Impumelelo enkulu emkhakheni wokufakazela amathiyoremu ngekhompyutha yenzeka ngowe-1965, ngokwenziwa semthethweni kwe-resolution inference mechanism. Namuhla, abafakazeli abanohlonze bamathiyori abizwa nge-Satisfiability Modulo Theories (SMT) bahlanganisa ama-SAT solvers nolwazi lobungcweti oluvela kwizizinda zezinkinga ezihlukahlukene ukuze bakwazi ukufakazela amathiyoremu okungelula neze ukuwafakazela. Ukukhula ngesivinini kobunzima nobunkimbinkimbi benkinga esizindeni esithile kubonwa njengenye yezinselelo ezinkulu okudingeka ukuthi zixazululwe ukuze kube nenqubekela phambili ekufakazelweni kwamathiyoremu ngekhompyutha. Amavulandlela eminyaka yawo-1950 nawo-1960 asesihlonzile kakade isidingo sokuthi amahuristikhi (heuristics) kube yiwona ahola umzamo wokuthola ubufakazi. Nakuba ikhona impumelelo esiyenziwe kumathiyori ezokucabangela okujulile kusetshenziswa amakhompyutha kanye nempumelelo yobuchwepheshe bamakhompyutha, usayizi wesizinda usalokhu uyinkinga uma kwenziwa imizamo yokuthola ubufakazi obuyinkimbinkimbi futhi obunobunzima obukhudlwana. Namuhla imbala, amahuristikhi asewuziso futhi ayadingeka ekufezekiseni izibopho zobufakazi obuyinkimbinkimbi. Ngowezi-2000, kwathuthukiswa amahuristikhi amaningana impela ukuze kulekelelwe uhlelo-kusebenza olungumfakazeli osekelwe phezu kwesixazululo, olubizwa nge-OTTER, ekutholeni ubufakazi bama-set-theoretic problems. Ukusebenziseka kwalawa mahuristikhi kwizinhlelo-kusebenza ezingabafakazeli bamathiyoremu besimanjemanje kwahlolwa ngowezi-2009. Uhlelo-kusebenza olungumfakazeli, olubizwa nge-Vampire kanye nalolo olubizwa nge-Gandalf zadinga ama-90% kanye nama-80%, ngokulandelana kwazo, maqondana nama-OTTER heuristics afanelekile. Lolu cwaningo luphenya futhi lucubungule ukusebenziseka kwama-OTTER heuristics ekufakazelweni kwamathiyoremu esimweni esiyinhlanganisela sokufakazela amathiyoremu esibizwa nge-Rodin—okuyi-system modelling tool suite eqondene ne-Event-B formal method. Kulolu cwaningo siyabonisa ukuthi mabili kuphela kwayi-10 ama-OTTER heuristics aba wusizo ngenkathi kufezekiswa isibopho sobufakazi ku-Rodin. Nakuba sibeka umbono wokuthi esikhathini esiningi ama-OTTER heuristics awazange abe wusizo uma esetshenziswa kuma-Rodin proofs, amahuristikhi asadingeka ezimweni lapho izibopho zobufakazi zingazenzekelanga ngokwazo ngokulawulwa yizinhlelo-kusebenza zekhompyutha. Ngakho-ke, siphakamisa amahuristikhi ethu amaningana angasetshenziswa ekufakazeleni amathiyoremu ku-Rodin tool suite. / School of Computing / M. Sc. (Computer Science)

The master’s thesis deals with Balanced Scorecard implementation within a company environment. The object of the thesis is to increase the effectiveness of strategic management which can be achieved through proper implementation of the method. The theoretical section explains the basic concepts of strategic management, followed by the description of method BSC, its implementation and risks. The practical part is focused on creating a business strategy and the model BSC implementation in particular company. As an auxiliary tool for management decision making a fuzzy model was developed and then a dialogue is held with fuzzy expert system.

Control theory of complex systems by utilization of artificial intelligent algorithms is relatively new science field and it can be used in many areas of technical practise. Best known algorithms to solved similar tasks are genetic algorithm, differential evolution, HC12 Nelder-Mead method, fuzzy logic and grammatical evolution. Complex solution is presented at selected examples from mathematical nonlinear systems to examples of anthems design and stabilization of deterministic chaos. The goal of this thesis is present examples of implementation and utilization of artificial algorithms by multi-objective optimization. To achieve optimal results is used designed software solution by multi-platform application, which used Matlab and Java interfaces. The software solution integrate every algorithms of this thesis to complex solution and it extends possible application of those approaches to real systems and practical world.

It is no secret that 'managerial' solutions are not, on average, nearly as reliable as 'technical' solutions. The focus of this work is to clarify the reasons why this is so, and to seek ways to increase the reliability of managerial solutions. The causes of this situation are both subjective (human factor failure), which can be influenced, and objective (complexity of the problem, the specifics of human behaviour, etc.) that can be only minimally influenced. Significant subjective causes at work were identified as: a. cognitive distortions at the mental level of thinking of the problem solvers; b. deficiencies in making inference and drawing conclusions; c. incorrect argumentation. There are two ways to reduce these causes: 1. cultivation of managerial thinking of the problem solvers; 2. the use of reserves in the implementation of approaches and tools of theoretical disciplines that already operate successfully elsewhere and are beneficial for managerial solutions. The first way deals with procedures for managerial solutions formulated in the language of the relevant discipline (the language of management), expressed by natural language and the chain of formulas (calculations) and visual (graphic) tools in the form of managerial decision trees, diagrams and charts with the rules of 'managerial logic'. This is generally defined as a set of approaches, tools, methods and skills needed for credible justification when solving managerial problems. Specifically it deals with: - the 'case-based reasoning' approach, which aims at finding the best point of view on a given problem and analysing all considered aspects within its context step-by-step in detail; - translating the tools and methods of modern logic (especially its intuitionistic version) from the language of logic into the language of management taking into account the factual content of expressive means of the language of management including the ability of their effective application; - respecting the principles of rational and ethical argumentation within managerial solutions. The second way circumvents managerial solution procedures by recasting the managerial task to the task of a scientific discipline (logic, game theory, etc.) and derives the correct result therein. In this context we talk about the use of knowledge of theoretical disciplines in management. Both of these ways are demonstrated in the work in a number of illustrative examples and the annexed case studies addressing the specific tasks of managerial practice.

Control theory of complex systems by utilization of artificial intelligent algorithms is relatively new science field and it can be used in many areas of technical practise. Best known algorithms to solved similar tasks are genetic algorithm, differential evolution, HC12 Nelder-Mead method, fuzzy logic and grammatical evolution. Complex solution is presented at selected examples from mathematical nonlinear systems to examples of anthems design and stabilization of deterministic chaos. The goal of this thesis is present examples of implementation and utilization of artificial algorithms by multi-objective optimization. To achieve optimal results is used designed software solution by multi-platform application, which used Matlab and Java interfaces. The software solution integrate every algorithms of this thesis to complex solution and it extends possible application of those approaches to real systems and practical world.

The subject of this diploma thesis is the simulation and digital commissioning of a robotic production system for welding elements such as studs on sheet metal parts. The basis of the work is search of information related to industrial robots, PLC control, tools used for welding, fixtures, manipulators, sensors, safety and protection elements commonly used in such production systems. The second part of the work deals with the given problem and it is a virtual commissioning of the given concept of a robotic production system. This means creating its simulation model in the Process Simulate environment, selecting robots, creating robotic trajectories, collision analysis, creating sensors, signals and optimization. Last part includes the connection of the simulation model with the software S-7PLCSIM Advanced and TIA Portal, the creation of control PLC logic in the form of a program, visualization and verification of their functionality using the above-mentioned connection with the simulation model.

The following diploma thesis focuses on processing of uncertain information in databases. Uncertain information represents vague customer requests during laptop choice in classic shop purchasing. Effort of the work is to develop a modern e-shop application selling laptops, which is based on expert fuzzy system helping customers to choose a laptop without knowledge of technical specifications and current trends.

This thesis focuses on fuzzy neural networks. The combination of the fuzzy logic and artificial neural networks leads to the development of more robust systems. These systems are used in various field of the research, such as artificial intelligence, machine learning and control theory. First, we provide a quick overview of underlying neural networks and fuzzy systems to explain fundamental ideas that form the basis of the fields, and follow with the introduction of the fuzzy neural network theory, classification and application. Then we describe a design and a realization of the fuzzy associative memory, as an example of these systems. Finally, we benchmark the realization using the pattern recognition and control tasks. The results are evaluated and compared against existing systems.

Cielom diplomovej prace je vytvorenie expertného systému založeného na modeloch fuzzy logiky v programoch Excel a MATLAB, pomocou ktorého je možné ohodnotiť rôzne dôchodkové fondy a ďalšie finančné produkty. Vzhľadom na prehlbujúcu sa demografickú krízu, práca ponúka návrhy optimálneho investičného mixu pre tri modelové situácie s cieľom dodatočného finančného zabezpečenia počas dôchodkového veku. Práca je spracovaná pre podmienky Slovenskej republiky, podľa súčasnej situácie a platnej legislatívy.