Fred: An approach to generating real, correct, reusable programs from proofs

In this paper we describe our system for automatically extracting "correct" programs from proofs using a development of the Curry-Howard process. Although program extraction has been developed by many authors, our system has a number of novel features designed to make it very easy to use and as close as possible to ordinary mathematical terminology and practice. These features include 1. the use of Henkin's technique to reduce higher-order logic to many-sorted (first-order) logic; 2. the free use of new rules for induction subject to certain conditions; 3. the extensive use of previously programmed (total, recursive) functions; 4. the use of templates to make the reasoning much closer to normal mathematical proofs and 5. a conceptual distinction between the computational type theory (for representing programs)and the logical type theory (for reasoning about programs). As an example of our system we give a constructive proof of the well known theorem that every graph of even parity, which is non-trivial in the sense that it does not consist of isolated vertices, has a cycle. Given such a graph as input, the extracted program produces a cycle as promised.

Quantified Analysis of the Leakage of Confidential Data

Basic information theory is used to analyse the amount of confidential information which may be leaked by programs written in a very simple imperative language. In particular, a detailed analysis is given of the possible leakage due to equality tests and if statements. The analysis is presented as a set of syntax-directed inference rules and can readily be automated.

The Requirements of Using Provenance in e-Science Experiments

In e-Science experiments, it is vital to record the experimental process for later use such as in interpreting results, verifying that the correct process took place or tracing where data came from. The process that led to some data is called the provenance of that data, and a provenance architecture is the software architecture for a system that will provide the necessary functionality to record, store and use process documentation. However, there has been little principled analysis of what is actually required of a provenance architecture, so it is impossible to determine the functionality they would ideally support. In this paper, we present use cases for a provenance architecture from current experiments in biology, chemistry, physics and computer science, and analyse the use cases to determine the technical requirements of a generic, technology and application-independent architecture. We propose an architecture that meets these requirements and evaluate a preliminary implementation by attempting to realise two of the use cases.

Terapia ocupacional em ação interdisciplinar: jogos educativo-nutricionais na prevenção da obesidade infantil

The inter-subjectivity is the answer in the search for the solution of complex problems, which concerns interfaces of knowledge, respecting their borders. This paradigm is essential in the author's work. So, the search on screen is based on this perspective, by using inter-subject groups of work conduced by professionals of Computer Science, Social Communication, Architecture and Urbanism, Pedagogy, Psicopegagogy, Nutritional Science, Endocrinology, Occupational Therapy and Nursing, it was also part of this group an 8 year old child, daughter of one of the professional who took part of the group. This thesis aims to present the course of investigation developed, analyzing the action of inter-subject Occupational Therapy and Nutrition on the promotion of learning nutritional concepts through educative-nutritional games in order to prevent child's obesity in an educative context. The research was analytic, interventionist and almost experimental. It took place in a public school in Fortaleza, Ceará, Brazil, between August and December 2004. It was selected a sample non-probabilistic, by convenience, of 200 children, born from 1994 to 1996. It was selected almost nonprobabilistically, by convenience, 200 children born between 1994 and 1996. To analyze the results it was used a triangulation, associated by quantitative and qualitative approaches. The basis collect happened through games specially manufactured to these research- video-games, board games, memory games, puzzles, scramble, searching words and iterative basics. There were semi-structured interviews, direct and structured observations and focus in-groups. It was noticed the efficiency of educativenutritional games in the learning process, which lead to a changing of attitude towards the eating choices. These games gave similar results in relation to the compared variations preferences, experience and attitudes, theses attitudes were observed through the game; and the categories to compare the possibility of learning by playing, the fantasy in the learning process, learning concepts of nutritional education and the need of help in the learning process (mediation). It was proved that educativenutritional games could be used to teach nutritional concepts, in an inter-subjective action of Occupational Therapy and Nutrition in schools. The simultaneous application of these games lead to the optimization of child s learning process. It should be emphasized the need of studies about the adaptation of tools used in a child s Nutritional Education, with the help of inter-subjective action. Because just one subject, in a fractionated way can give an answer to complex problems and help to a change of the reality with effectiveness and resolution

A representação social de disciplinas didático-pedagógicas no contexto da formação inicial docente: um entremear de saberes

We seek, through this study, to analyze about social representation that the students of licentiate degree course of the Federal Institute of Education, Science and Technology of Rio Grande do Norte - IFRN - have about didactic-pedagogical subjects. We utilize the Social Representations Theory (MOSCOVICI, 2009; 2012; JODELET, 2001) as a theoretical and methodological contribution and as aim, we identify this social representation and understand how it is influenced by the formation of these undergraduates. So we developed the research under the seven undergraduate classroom courses offered by IFRN, namely: Biology, Spanish, Physics, Geography, Computer Science, Mathematics and Chemistry, covering units located both in the capital and in the countryside. While methodological approach we used the Procedure of Multiple Classification (PMC) - (ROAZZI, 1995), whose realization requires a set of words achieved through of Free Technique of Words Association - FTWA - (ABRIC, 1998). For this realization we have a total of one hundred twenty (120) participants, with thirty (30) in FTWA and other stage in the realization of free classification and directed that correspond to the MPR. Achieved the empirical data, we use the analysis of content (BARDIN, 2011; FRANCO, 2007) and multidimensional (ROAZZI, 1995) for the course of his interpretation. Finally, we identify the social representation of didactic and pedagogical subjects centered around the idea that it is through these subjects that can achieve the profile of "good professional" as one who gathers knowledge and attributes required for the full development of teaching involving capabilities it and characteristics that mark the sense of professionalism. Furthermore, we found that the anchoring social representation on the understanding that these disciplines "teach the teacher to be" in the image and its objectification of the "good teacher", ie, one that reaches through the training process and experiences, qualities that make it unique and able to carry full professional. Still see that the actions of the teacher trainer affects the way students perceive, assume and engage in the study of teaching and pedagogical subjects and it reflects significantly the social representation then created

Improving accuracy and speed of optimum-path forest classifier using combination of disjoint training subsets

The Optimum-Path Forest (OPF) classifier is a recent and promising method for pattern recognition, with a fast training algorithm and good accuracy results. Therefore, the investigation of a combining method for this kind of classifier can be important for many applications. In this paper we report a fast method to combine OPF-based classifiers trained with disjoint training subsets. Given a fixed number of subsets, the algorithm chooses random samples, without replacement, from the original training set. Each subset accuracy is improved by a learning procedure. The final decision is given by majority vote. Experiments with simulated and real data sets showed that the proposed combining method is more efficient and effective than naive approach provided some conditions. It was also showed that OPF training step runs faster for a series of small subsets than for the whole training set. The combining scheme was also designed to support parallel or distributed processing, speeding up the procedure even more. © 2011 Springer-Verlag.

A proposed neural control for the trajectory tracking of a nonholonomic mobile robot with disturbances

In this paper, a trajectory tracking control problem for a nonholonomic mobile robot by the integration of a kinematic neural controller (KNC) and a torque neural controller (TNC) is proposed, where both the kinematic and dynamic models contains disturbances. The KNC is a variable structure controller (VSC) based on the sliding mode control theory (SMC), and applied to compensate the kinematic disturbances. The TNC is a inertia-based controller constituted of a dynamic neural controller (DNC) and a robust neural compensator (RNC), and applied to compensate the mobile robot dynamics, and bounded unknown disturbances. Stability analysis with basis on Lyapunov method and simulations results are provided to show the effectiveness of the proposed approach. © 2012 Springer-Verlag.

Teoria da ressonância adaptativa através da linguagem Java para detecção e classificação de e-mails indesejados

Pós-graduação em Engenharia Elétrica - FEIS

Ensaio sobre o fluxo de Ricci e os buracos negros: fundamentação e estudo computacional

Pós-graduação em Ciência da Computação - IBILCE

Role playing game eletrônico: uma tecnologia lúdica para aprender e ensinar matemática

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Estabilidade global e bifurcação de Hopf em um modelo de HIV baseado em sistemas do tipo Lotka-Volterra

Pós-graduação em Matematica Aplicada e Computacional - FCT