This diploma thesis examines applications of datamining methods to open data. It is realized by solving analytical questions using the LISp-Miner system. Analytical questions are examined in data from The Czech Trade Inspection Authority from the perspective of the data owner. Procedure used to solve analytical questions is 4ft-Miner. There are presented and resolved four analytical questions, which are the results of the work. Work includes a detailed description of the transformation of the relational database into a format suitable for data mining. A detailed description of the data is also included. The theoretical part deals with the GUHA method and CRISP-DM methodology.

This thesis applies the data mining method of decision rules on data from Consulting centre for Metabolism disorders from University hospital Pilsen. As a tool is used the system LISp-Miner, developed at University of Economics, Prague. Decision rules found are evaluated by a specialist. The main parts of this thesis are followings: an overview on main data mining methods and results evalutation methods, description of the data mining method application on data and description and evaluation of results.

In programming languages, record types give a universe of discourse (via so-called Σ-types); parameterised record types fix parts of that universe ahead of time (via Π-types), and algebraic datatypes give us first-class syntax (via W-types), which can then be used to program, e.g., evaluators and optimisers. A frequently-encountered issue in library design for statically-typed languages is that, for example, the algebraic datatype implementing the first-class view of the language induced by a record declaration cannot be defined by simple reference to the record type declaration, nor to any common “source”. This leads to unwelcome repetition, and to maintenance burdens. Similarly, the “unbundling problem” concerns similar repetition that arises for variants of record types where some fields are turned into parameters. The goal of this thesis is to show how, in dependently-typed languages (DTLs), algebraic datatypes and parameterised record types can be obtained from a single pragmatic declaration within the dependently-typed language itself, without using a separate “module language”. Besides this practical shared declaration interface, which is extensible in the language, we also find that common data structures correspond to simple theories. Put simply, the thesis is about making tedious and inexpressible patterns of programming in DTLs (dependently typed languages) become mechanical and expressible. The situations described above occur frequently when working in a dependently-typed language, and it is reasonable enough to have the computer handle them. We develop a notion of contexts that serve as common source for definitions of algebraic datatype and of parameterised record types, and demonstrate a “language” of “package operations” that enables us to avoid the above-mentioned replication that pervades current library developments. On the one hand, we demonstrate an implementation of that language as integrated editor functionality — this makes it possible to directly emulate the different solutions that are employed in current library developments, and refactor these into a shape that uses single declaration of contexts, thus avoiding the usual repetition that is otherwise required for provision of record types at different levels of parameterisation and of algebraic datatypes. On the other hand, we will demonstrate that the power of dependently-typed languages is sufficient to implement such package operations in a statically-typed manner within the language; using this approach will require adapting to the accordingly-changed library interfaces. Although our development uses the dependently-typed programming language Agda throughout, we emphasise that the idea is sufficiently generic to be implemented in other DTLs. / Thesis / Doctor of Philosophy (PhD) / There are things we want to use from various perspectives, our tools show that this is possible without any duplication and in a practical and efficient fashion.

Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check them with theorem-proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier? We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are "always true"). Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higher-level proofs can be written more concisely than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified. To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some phi, there exists a Level 1 proof of phi. We then mechanically translate the Level 11 proof for each Level n into a Level n - 1 proof---that is, we create a Level 1 proof of Level 2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs. In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1. / text

Thesis (Ph.D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 1982. / MICROFICHE COPY AVAILABLE IN ARCHIVES AND ENGINEERING. / Bibliography: leaves 756-761. / by Brian Cantwell Smith. / Ph.D.

Thesis (Ph.D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 1982. / MICROFICHE COPY AVAILABLE IN ARCHIVES AND ENGINEERING. / Bibliography: leaves 439-451. / by Robert Cregar Berwick. / Ph.D.

On étudie l'abstraction et la généricité dans les langages de programmation. On décrit les principaux outils de la programmation générique. On traite ensuite de la spécification des types et des fonctions et on étudie les methodes de vérification de programmes spécifiés algébriquement.

Le but de cette these est de definir et developper un systeme de bases lexicales multilingues independant des applications et des theories linguistiques. Elle debute donc par une etude des dictionnaires (imprimes ou electroniques) et des outils de gestion de bases lexicales, avec, notamment, le projet ESPRIT MULTILEX, considere comme l'effort le plus avance, mais qui presente quelques faiblesses (architecture lexicale par transfert, structures linguistiques codees sous forme de structures de traits types.). La deuxieme partie de cette these est consacree a la definition de SUBLIM, un systeme de gestion de bases lexicales multilingues qui permet de specifier l'architecture lexicale (organisation des dictionnaires) et l'architecture linguistique (organisation des informations linguistiques des unites des dictionnaires), sans imposer de contraintes ni sur les types de dictionnaires choisis, ni sur les structures linguistiques utilisees. La troisieme et derniere partie de cette these presente une specialisation de ce systeme generique en un systeme dedie a la gestion de bases lexicales multilingues fondees sur les acceptions interlingues : NADIA. Cette approche generalise certaines methodes interlingues comme celle du projet de traduction multilingue ULTRA, et permet la definition de bases lexicales multilingues ne se basant pas sur une approche par connaissances.

.

Submitted by Izabel Franco (izabel-franco@ufscar.br) on 2016-09-23T12:33:24Z No. of bitstreams: 1 DissAJRC.pdf: 3333263 bytes, checksum: 705b9ce01810131eee4f42918ca5f807 (MD5) / Approved for entry into archive by Marina Freitas (marinapf@ufscar.br) on 2016-09-26T20:36:15Z (GMT) No. of bitstreams: 1 DissAJRC.pdf: 3333263 bytes, checksum: 705b9ce01810131eee4f42918ca5f807 (MD5) / Approved for entry into archive by Marina Freitas (marinapf@ufscar.br) on 2016-09-26T20:36:21Z (GMT) No. of bitstreams: 1 DissAJRC.pdf: 3333263 bytes, checksum: 705b9ce01810131eee4f42918ca5f807 (MD5) / Made available in DSpace on 2016-09-26T20:36:27Z (GMT). No. of bitstreams: 1 DissAJRC.pdf: 3333263 bytes, checksum: 705b9ce01810131eee4f42918ca5f807 (MD5) Previous issue date: 2015-05-05 / Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq) / It’s presented in this work a graphic program that allows the analysis (calculation of forces and displacements) of concrete slabs by the equivalent grid model. The surface is considered as monolithic without the traditional discretization of the structure, i.e., the separation of the various structural members (beams, columns and slabs). Only the pillars are considered as unmovable in the direction of its principal axis. The graphical environment designed for this is pioneering, developed by objectoriented programming and will be distributed freely and with listings available. The system allows the designing of the structure as a model, allowing an easier perception of its different structural components and the definition of the different stresses on it. The program establishes an interface adapted to the calculation module, that initially was developed by Igor Stayanov Cotta in 2006,.and thus allows the graphic view of the efforts, displacements and stresses acting over the model. / Apresenta-se neste trabalho um programa gráfico que permite a análise (cálculo de esforços e deslocamentos) de lajes de concreto pelo modelo da grelha equivalente. O pavimento é considerado como monolítico sem a tradicional discretização da estrutura, ou seja, a separação dos diversos elementos estruturais (vigas, lajes e pilares). Apenas os pilares são considerados como indeslocáveis na direção do seu eixo principal. O ambiente gráfico idealizado para tal é pioneiro, desenvolvido por meio da programação orientada a objetos e será livre (gratuito e com listagem disponível). No sistema é possível lançar a estrutura como se desenham as fôrmas de uma estrutura, permitindo assim, de forma fácil, a caracterização das diferentes propriedades dos materiais e a definição das ações atuantes na estrutura. O programa estabelece uma interface para o módulo de cálculo adaptado que, inicialmente, foi desenvolvido por Igor Stayanov Cotta em 2006.e assim permite a visualização dos esforços, dos deslocamentos e dos gráficos de tensões na tela do monitor.