Mechanising first-order temporal resolution

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. Although a complete and correct resolution-style calculus has already been suggested for this specific fragment, this calculus involves constructions too complex to be of practical value. In this paper, we develop a machine-oriented clausal resolution method which features radically simplified proof search. We first define a normal form for monodic formulae and then introduce a novel resolution calculus that can be applied to formulae in this normal form. By careful encoding, parts of the calculus can be implemented using classical first-order resolution and can, thus, be efficiently implemented. We prove correctness and completeness results for the calculus and illustrate it on a comprehensive example. An implementation of the method is briefly discussed.

Monodic Temporal Resolution

First-order temporal logic is a coincise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics have identified important enumerable and even decidable fragments. In this paper we present the first resolution-based calculus for monodic first-order temporal logic. Although the main focus of the paper is on establishing completeness result, we also consider implementation issues and define a basic loop-search algorithm that may be used to guide the temporal resolution system.

Handling Equality in Monodic Temporal Resolution

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments including the guarded fragment with equality. In this paper, we specialise the monodic resolution method to the guarded monodic fragment with equality and first-order temporal logic over expanding domains. We introduce novel resolution calculi that can be applied to formulae in the normal form associated with the clausal resolution method, and state correctness and completeness results.

Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.

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.

Adaptive languages and a new programming style

A programming style can be seen as a particular model of shaping thought or a special way of codifying language to solve a problem. Adaptive languages have the basic feature of allowing the expression of programs which self-modifying through adaptive actions at runtime. The conception of such languages calls for a new programming style, since the application of adaptive technology in the field of programming languages suggests a new way of thinking. With the adaptive style, programming language codes can be structured in such a way that the codified program therein modifies or adapts itself towards the needs of the problem. The adaptive programming style may be a feasible alternate way to obtain self-modifying consistent codes, which allow its use in modern applications for self-modifying code.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

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

Conditional reasoning: A key to assessing computer-based knowledge-building communication processes

This article describes a methodological approach to conditional reasoning in online asynchronous learning environments such as Virtual-U VGroups, developed by SFU, BC, Canada, consistent with the notion of meaning implication: If part of a meaning C is embedded in B and a part of a meaning B is embedded in A, then A implies C in terms of meaning [Piaget 91]. A new transcript analysis technique was developed to assess the flows of conditional meaning implications and to identify the occurrence of hypotheses and connections among them in two human science graduate mixed-mode online courses offered in the summer/spring session of 1997 by SFU. Flows of conditional meaning implications were confronted with Virtual-U VGroups threads and results of the two courses were compared. Findings suggest that Virtual-U VGroups is a knowledge-building environment although the tree-like Virtual-U VGroups threads should be transformed into neuronal-like threads. Findings also suggest that formulating hypotheses together triggers a collaboratively problem-solving process that scaffolds knowledge-building in asynchronous learning environments: A pedagogical technique and an built-in tool for formulating hypotheses together are proposed. © Springer Pub. Co.

ARISupport - Interaction support for augmented reality systems

The communication between user and software is a basic stage in any Interaction System project. In interactive systems, this communication is established by the means of a graphical interface, whose objective is to supply a visual representation of the main entities and functions present in the Virtual Environment. New ways of interacting in computational systems have been minimizing the gap in the relationship between man and computer, and therefore enhancing its usability. The objective of this paper, therefore, is to present a proposal for a non-conventional user interface library called ARISupport, which supplies ARToolKit applications developers with an opportunity to create simple GUI interfaces, and provides some of the functionality used in Augmented Reality systems. © Springer-Verlag Berlin Heidelberg 2005.

The application of distributed virtual machines for enterprise computer management: A two-tier network file system for image provisioning and management

In order to simplify computer management, several system administrators are adopting advanced techniques to manage software configuration of enterprise computer networks, but the tight coupling between hardware and software makes every PC an individual managed entity, lowering the scalability and increasing the costs to manage hundreds or thousands of PCs. Virtualization is an established technology, however its use is been more focused on server consolidation and virtual desktop infrastructure, not for managing distributed computers over a network. This paper discusses the feasibility of the Distributed Virtual Machine Environment, a new approach for enterprise computer management that combines virtualization and distributed system architecture as the basis of the management architecture. © 2008 IEEE.

Towards a java bytecodes compiler for nios II soft-core processor

Reconfigurable computing is one of the most recent research topics in computer science. The Altera - Nios II soft-core processor can be included in a large set of reconfigurable architectures, especially because it is designed in software, allowing it to be configured according to the application. The recent growth in applications that demand reconfigurable computing made necessary the building of compilers that translate high level languages source codes into reconfigurable devices instruction sets. In this paper we present a compiler that takes as input the bytecodes generated by a Java front-end compiler and generates a set of instructions that attends to the Nios II processor instruction set rules. Our work shows how we process Java bytecodes to the intermediate code, in the Nios II instructions format, and build the control flow and the control dependence graphs. © 2009 IEEE.

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.