Prova automática de satisfatibilidade módulo teoria aplicada ao método B

Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B

Uma investigação de algoritmos exatos e metaheurísticos aplicados ao nonograma

Nonogram is a logical puzzle whose associated decision problem is NP-complete. It has applications in pattern recognition problems and data compression, among others. The puzzle consists in determining an assignment of colors to pixels distributed in a N  M matrix that satisfies line and column constraints. A Nonogram is encoded by a vector whose elements specify the number of pixels in each row and column of a figure without specifying their coordinates. This work presents exact and heuristic approaches to solve Nonograms. The depth first search was one of the chosen exact approaches because it is a typical example of brute search algorithm that is easy to implement. Another implemented exact approach was based on the Las Vegas algorithm, so that we intend to investigate whether the randomness introduce by the Las Vegas-based algorithm would be an advantage over the depth first search. The Nonogram is also transformed into a Constraint Satisfaction Problem. Three heuristics approaches are proposed: a Tabu Search and two memetic algorithms. A new function to calculate the objective function is proposed. The approaches are applied on 234 instances, the size of the instances ranging from 5 x 5 to 100 x 100 size, and including logical and random Nonograms

On Fuzzy Implication Classes - Towards Extensions of Fuzzy Rule-Based Systems

Atualmente, há diferentes definições de implicações fuzzy aceitas na literatura. Do ponto de vista teórico, esta falta de consenso demonstra que há discordâncias sobre o real significado de "implicação lógica" nos contextos Booleano e fuzzy. Do ponto de vista prático, isso gera dúvidas a respeito de quais "operadores de implicação" os engenheiros de software devem considerar para implementar um Sistema Baseado em Regras Fuzzy (SBRF). Uma escolha ruim destes operadores pode implicar em SBRF's com menor acurácia e menos apropriados aos seus domínios de aplicação. Uma forma de contornar esta situação e conhecer melhor os conectivos lógicos fuzzy. Para isso se faz necessário saber quais propriedades tais conectivos podem satisfazer. Portanto, a m de corroborar com o significado de implicação fuzzy e corroborar com a implementação de SBRF's mais apropriados, várias leis Booleanas têm sido generalizadas e estudadas como equações ou inequações nas lógicas fuzzy. Tais generalizações são chamadas de leis Boolean-like e elas não são comumente válidas em qualquer semântica fuzzy. Neste cenário, esta dissertação apresenta uma investigação sobre as condições suficientes e necessárias nas quais três leis Booleanlike like — y ≤ I(x, y), I(x, I(y, x)) = 1 e I(x, I(y, z)) = I(I(x, y), I(x, z)) — se mantém válidas no contexto fuzzy, considerando seis classes de implicações fuzzy e implicações geradas por automorfismos. Além disso, ainda no intuito de implementar SBRF's mais apropriados, propomos uma extensão para os mesmos

A integração do tutorial interativo TryLogic via IMS Learning Tools Interoperability: construindo uma infraestrutura para o ensino de Lógica através de estratégias de demonstração e refutação

Logic courses represent a pedagogical challenge and the recorded number of cases of failures and of discontinuity in them is often high. Amont other difficulties, students face a cognitive overload to understand logical concepts in a relevant way. On that track, computational tools for learning are resources that help both in alleviating the cognitive overload scenarios and in allowing for the practical experimenting with theoretical concepts. The present study proposes an interactive tutorial, namely the TryLogic, aimed at teaching to solve logical conjectures either by proofs or refutations. The tool was developed from the architecture of the tool TryOcaml, through support of the communication of the web interface ProofWeb in accessing the proof assistant Coq. The goals of TryLogic are: (1) presenting a set of lessons for applying heuristic strategies in solving problems set in Propositional Logic; (2) stepwise organizing the exposition of concepts related to Natural Deduction and to Propositional Semantics in sequential steps; (3) providing interactive tasks to the students. The present study also aims at: presenting our implementation of a formal system for refutation; describing the integration of our infrastructure with the Virtual Learning Environment Moodle through the IMS Learning Tools Interoperability specification; presenting the Conjecture Generator that works for the tasks involving proving and refuting; and, finally to evaluate the learning experience of Logic students through the application of the conjecture solving task associated to the use of the TryLogic

Papel do município e relações federativas: atuação de municípios cearenses nas políticas de formação continuada de alfabetizadores

The investigation analyze s the role of the municipalities in the ongoing development of literacy teachers, having as a field of study the municipalities of Jaguaruana and Palhano, both in the State of Ceará. The political - educational space adopted as a sample of the study is the p eriod between the years 2003 and 2006, when the emphasis on cooperative action among the federated entities is observed in the Government’s guidelines and Brazilian educational policies, showing the municipal presence in the implementation and execution of these policies. T he historical - dialectical materialistic perspective, understood as an analysis of the social reality as historical elaboration and product of the human praxis, is expressed as the required theoretical - methodological path. The investigatio n is operationalized through interconnected stages: one that involves bibliographical and documental analysis, in which the theoretical input of the research is added, as well as the Federal, State and M unicipal documents accessed ; and another, regarding t he field work, studying the specific character of the object and its mutual rela tionships in the municipalities . The research brings the notion of intergovernmental relationships and cooperative mechanisms as central theoretical tools and, dialoguing with them, ideas such as decentralization, municipalization and municipal autonomy are inserted into a theoretical/practical body, through which the historical and logical aspects of the object are detailed. The study describes and interprets the policies of on going development of literacy teachers with focus on the national guidelines formulated since the 1990’s and on the govern mental incorporation in the national and subnational spaces. In this sense, the analysis is based on the comprehension of the interrel ationship between the municipal policies and the p olicies created by the S tate or Federal G overnments in order to offer ongoing development of literacy teachers. Considering the investigated sample, it shows how the municipal role and the relationships bet ween the State and municipalities of Ceará have emerged, as well as their characteristics regarding the education management policies, taking into account the practices of municipalization and cooperation between the State and municipalities in their histo rical composition. It shows the practices which aim at the ongoing development of literacy teachers observed in the researched municipalities, pointing out the realities and specific marks left by municipal presence in the area, demonstrating the assigned role and the role played. Based on the points of view of the managers interviewed in the municipalities of Jaguaruana e Palhano, it is possible to note the meaning and effectiveness of the policies carried out. With such elements, it discusses the municipa l asymmetries in their homogeneities and heterogeneities rega rding the execution of their federative role. The analysis shows that th e role of the municipalities vary according to the historical, political and social interventions in each municipality. In the fields of formulation and execution of educational policies, the actions of the municipal governments, situated and with expressive interferences, reveal asymmetries in the sense that some municipalities have bigger autonomy and participate more effect ively in the production and distribution of policies than others. In terms of the researched realities, the study shows that taking care of the policies of ongoing development of literacy teachers is not a task that should be assigned exclusively to the mu nicipalities, nonetheless it is a role that they play with varying degrees of success. This role is in fact a joint competence of the federated entities, in the scope the Brazilian cooperative federalism.

Modelo comportamental do capacitor ferroelétrico como unidade básica de neurônios artificiais e sua implementação em FPGA

This work proposes the use of the behavioral model of the hysteresis loop of the ferroelectrics capacitor as a new alternative to the usually costly techniques in the computation of nonlinear functions in artificial neurons implemented on reconfigurable hardware platform, in this case, a FPGA device. Initially the proposal has been validated by the implementation of the boolean logic through the digital models of two artificial neurons: the Perceptron and a variation of the model Integrate and Fire Spiking Neuron, both using the model also digital of the hysteresis loop of the ferroelectric capacitor as it’s basic nonlinear unit for the calculations of the neurons outputs. Finally, it has been used the analog model of the ferroelectric capacitor with the goal of verifying it’s effectiveness and possibly the reduction of the number of necessary logic elements in the case of implementing the artificial neurons on integrated circuit. The implementations has been carried out by Simulink models and the synthesizing has been done through the DSP Builder software from Altera Corporation.

Of madness and many-valuedness: an investigation into Suszko's Thesis

Suszko’s Thesis is a philosophical claim regarding the nature of many-valuedness. It was formulated by the Polish logician Roman Suszko during the middle 70s and states the existence of “only but two truth values”. The thesis is a reaction against the notion of many-valuedness conceived by Jan Łukasiewicz. Reputed as one of the modern founders of many-valued logics, Łukasiewicz considered a third undetermined value in addition to the traditional Fregean values of Truth and Falsehood. For Łukasiewicz, his third value could be seen as a step beyond the Aristotelian dichotomy of Being and non-Being. According to Suszko, Łukasiewicz’s ideas rested on a confusion between algebraic values (what sentences describe/denote) and logical values (truth and falsity). Thus, Łukasiewicz’s third undetermined value is no more than an algebraic value, a possible denotation for a sentence, but not a genuine logical value. Suszko’s Thesis is endorsed by a formal result baptized as Suszko’s Reduction, a theorem that states every Tarskian logic may be characterized by a two-valued semantics. The present study is intended as a thorough investigation of Suszko’s thesis and its implications. The first part is devoted to the historical roots of many-valuedness and introduce Suszko’s main motivations in formulating the double character of truth-values by drawing the distinction in between algebraic and logical values. The second part explores Suszko’s Reduction and presents the developments achieved from it; the properties of two-valued semantics in comparison to many-valued semantics are also explored and discussed. Last but not least, the third part investigates the notion of logical values in the context of non-Tarskian notions of entailment; the meaning of Suszko’s thesis within such frameworks is also discussed. Moreover, the philosophical foundations for non-Tarskian notions of entailment are explored in the light of recent debates concerning logical pluralism.

Ambiente para avaliação de controladores fuzzy aplicados ao método de elevação artificial por bombeio centrífugo submerso

From their early days, Electrical Submergible Pumping (ESP) units have excelled in lifting much greater liquid rates than most of the other types of artificial lift and developed by good performance in wells with high BSW, in onshore and offshore environments. For all artificial lift system, the lifetime and frequency of interventions are of paramount importance, given the high costs of rigs and equipment, plus the losses coming from a halt in production. In search of a better life of the system comes the need to work with the same efficiency and security within the limits of their equipment, this implies the need for periodic adjustments, monitoring and control. How is increasing the prospect of minimizing direct human actions, these adjustments should be made increasingly via automation. The automated system not only provides a longer life, but also greater control over the production of the well. The controller is the brain of most automation systems, it is inserted the logic and strategies in the work process in order to get you to work efficiently. So great is the importance of controlling for any automation system is expected that, with better understanding of ESP system and the development of research, many controllers will be proposed for this method of artificial lift. Once a controller is proposed, it must be tested and validated before they take it as efficient and functional. The use of a producing well or a test well could favor the completion of testing, but with the serious risk that flaws in the design of the controller were to cause damage to oil well equipment, many of them expensive. Given this reality, the main objective of the present work is to present an environment for evaluation of fuzzy controllers for wells equipped with ESP system, using a computer simulator representing a virtual oil well, a software design fuzzy controllers and a PLC. The use of the proposed environment will enable a reduction in time required for testing and adjustments to the controller and evaluated a rapid diagnosis of their efficiency and effectiveness. The control algorithms are implemented in both high-level language, through the controller design software, such as specific language for programming PLCs, Ladder Diagram language.