Regular Derivations in Basic Superposition-Based Calculi

We prove the completeness of the regular strategy of derivations for superposition-based calculi. The regular strategy was pioneered by Kanger in [Kan63], who proposed that all equality inferences take place before all other steps in the proof. We show that the strategy is complete with the elimination of tautologies. The implication of our result is the completeness of non-standard selection functions by which in non-relational clauses only equality literals (and all of them) are selected.

Quantitative Information Flow, Relations and Polymorphic Types

This paper uses Shannon's information theory to give a quantitative definition of information flow in systems that transform inputs to outputs. For deterministic systems, the definition is shown to specialise to a simpler form when the information source and the known inputs jointly determine the inputs. For this special case, the definition is related to the classical security condition of non-interference and an equivalence is established between non-interference and independence of random variables. Quantitative information flow for deterministic systems is then presented in relational form. With this presentation, it is shown how relational parametricity can be used to derive upper and lower bounds on information flows through families of functions defined in the second order lambda calculus.

Model Configuration And Data Management In The Short-Term Water Information Forecasting Tools

The Short-term Water Information and Forecasting Tools (SWIFT) is a suite of tools for flood and short-term streamflow forecasting, consisting of a collection of hydrologic model components and utilities. Catchments are modeled using conceptual subareas and a node-link structure for channel routing. The tools comprise modules for calibration, model state updating, output error correction, ensemble runs and data assimilation. Given the combinatorial nature of the modelling experiments and the sub-daily time steps typically used for simulations, the volume of model configurations and time series data is substantial and its management is not trivial. SWIFT is currently used mostly for research purposes but has also been used operationally, with intersecting but significantly different requirements. Early versions of SWIFT used mostly ad-hoc text files handled via Fortran code, with limited use of netCDF for time series data. The configuration and data handling modules have since been redesigned. The model configuration now follows a design where the data model is decoupled from the on-disk persistence mechanism. For research purposes the preferred on-disk format is JSON, to leverage numerous software libraries in a variety of languages, while retaining the legacy option of custom tab-separated text formats when it is a preferred access arrangement for the researcher. By decoupling data model and data persistence, it is much easier to interchangeably use for instance relational databases to provide stricter provenance and audit trail capabilities in an operational flood forecasting context. For the time series data, given the volume and required throughput, text based formats are usually inadequate. A schema derived from CF conventions has been designed to efficiently handle time series for SWIFT.

An assessment of criteria to evaluate the graduate education program in Brazil

This study sought to identify criteria adequate for the evaluation of graduate programs in Brazil. A survey was the means for collecting the ratings and rankings given by faculty members at selected Brazilian graduate programs. A questionnaire using Likerttype and ranking items asked the importance attributed by each respondent to each of the 109 items listed. The data analysis reported in this dissertation indicates that the most highly rated criteria and indicators were: (1) Library: current periodicals; (2) Facilities: classrooms and laboratories; (3) Library: books and monographs; (4) Academic Environment: discussion, investigation, and expression; and (5) Facilities: research space and equipment. The study presents the means and standard deviations obtained for each indicator and also includes some figures obtained for a relational analysis. This dissertation was developed to provide useful information to educational planners, policy makers, administrators, and evaluators involved in Brazilian higher education or comparative studies. It is suggested that additional investigations concentrate on more specific and in-depth analysis and interpretation of the policymaking processes, i.e., on the study of social facts or organizational and academic variables in their relationships with aspects of the educational system. The appendices section includes a facsimile of the questionnaire and additional data.

Implementação de bancos de dados temporais com versionamento de esquemas: um estudo comparativo

Nas aplicações do mundo real, os dados mudam com o passar do tempo. Devido à característica dinâmica das aplicações, o esquema conceitual também pode mudar para se adaptar às mudanças que freqüentemente ocorrem na realidade. Para representar esta evolução, uma nova versão do esquema é definida e os dados armazenados são adaptados à nova versão. Entretanto, existem aplicações que precisam acessar também o esquema sob os diversos aspectos de suas mudanças, requerendo o uso de versionamento de esquemas. Durante a evolução do esquema, o versionamento preserva todas as versões deste esquema e seus dados associados, possibilitando a recuperação dos dados através da versão com a qual foram definidos. Ultimamente muitas pesquisas têm sido realizadas envolvendo as áreas de versionamento de esquemas e bancos de dados temporais. Estes bancos de dados provêm suporte ao versionamento de esquemas, pois permitem armazenar e recuperar todos os estados dos dados, registrando sua evolução ao longo do tempo. Apesar de muitos esforços, ainda não existem SGBDs temporais comercialmente disponíveis. A utilização de um modelo de dados temporal para a especificação de uma aplicação não implica, necessariamente, na utilização de um SGBD específico para o modelo. Bancos de dados convencionais podem ser utilizados desde que exista um mapeamento adequado entre o modelo temporal e o SGBD utilizado. Este trabalho apresenta uma abordagem para a implementação de um banco de dados temporal permitindo o versionamento de esquemas, usando um banco de dados relacional, tendo como base o modelo temporal TRM (Temporal Relational Model). Como forma de ilustrar apresenta-se um exemplo de implementação utilizando o SGBD DB2. O principal objetivo é avaliar diferentes técnicas de implementar e gerenciar o versionamento de esquemas em bancos de dados temporais. Para atingir esse objetivo, um protótipo foi desenvolvido para automatizar os mapeamentos do TRM para o DB2 e gerenciar o versionamento de esquemas e dados. Duas experiências de implementação foram realizadas utilizando formas diferentes de armazenar os dados - um repositório e vários repositórios - com o objetivo de comparar os resultados obtidos, considerando um determinado volume de dados e alterações. Um estudo de caso também é apresentado para validar as implementações realizadas.

Redes sociais e empresas II

Este relatório apresenta uma análise da bibliografia brasileira e da bibliografia internacional (anglo-saxã) sobre redes e empresas com o objetivo de contribuir para o debate teórico e orientar futuras pesquisas empíricas sobre o tema no Brasil, especialmente no campo da teoria das organizações e sociologia econômica. Para tanto, analisamos a bibliografia publicada nos últimos 10 anos (1990 a 2003) que trabalham com a abordagem de redes em três campos específicos: 1) a formação de redes entre empresas e o local onde estão inseridas; 2) o papel das redes na promoção de mudanças organizacionais e inovação; 3) o desenvolvimento de relações de confiança entre empresas e seu impacto na definição de estratégias empresariais.

Planejando o país do futuro à luz da cidadania: planejamento participativo no setor elétrico brasileiro

Este trabalho investiga o planejamento participativo como resultado da confluência de valores contemporâneos ligados aos conceitos de democracia e cidadania, que, ao mesmo tempo, atendem a exigências de sobrevivência e competitividade empresarial em um setor essencial de alto impacto ambiental, como o setor elétrico. Partindo de uma leitura relacional de poder na sociedade, o texto busca tecer o cenário que condicionou a aparente unanimidade do discurso participativo. Descreve o setor elétrico brasileiro e seus primeiros passos no sentido de se adequar às demandas democráticas e ambientais pela via do planejamento.