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.

Using Multi-Objective Optimization To Maximize Multiple Benefits For Sustainable Drainage Design

For many years, drainage design was mainly about providing sufficient network capacity. This traditional approach had been successful with the aid of computer software and technical guidance. However, the drainage design criteria had been evolving due to rapid population growth, urbanisation, climate change and increasing sustainability awareness. Sustainable drainage systems that bring benefits in addition to water management have been recommended as better alternatives to conventional pipes and storages. Although the concepts and good practice guidance had already been communicated to decision makers and public for years, network capacity still remains a key design focus in many circumstances while the additional benefits are generally considered secondary only. Yet, the picture is changing. The industry begins to realise that delivering multiple benefits should be given the top priority while the drainage service can be considered a secondary benefit instead. The shift in focus means the industry has to adapt to new design challenges. New guidance and computer software are needed to assist decision makers. For this purpose, we developed a new decision support system. The system consists of two main components – a multi-criteria evaluation framework for drainage systems and a multi-objective optimisation tool. Users can systematically quantify the performance, life-cycle costs and benefits of different drainage systems using the evaluation framework. The optimisation tool can assist users to determine combinations of design parameters such as the sizes, order and type of drainage components that maximise multiple benefits. In this paper, we will focus on the optimisation component of the decision support framework. The optimisation problem formation, parameters and general configuration will be discussed. We will also look at the sensitivity of individual variables and the benchmark results obtained using common multi-objective optimisation algorithms. The work described here is the output of an EngD project funded by EPSRC and XP Solutions.

Desenvolvimento de uma abordagem para a inserção da simulação no setor hospitalar de Porto Alegre

Esta dissertação apresenta uma abordagem para inserção e aplicação da técnica de Simulação Computacional como ferramenta de apoio a análise de decisão no setor hospitalar. Um grupo de onze hospitais foi contemplado diretamente no estudo. O processo de inserção da ferramenta foi implementado em quatro macro etapas. As duas primeiras etapas envolveram a totalidade do grupo de hospitais e objetivaram a divulgação da ferramenta; foram elas: (i) Pesquisa para diagnosticar o conhecimento e interesse do grupo na técnica, e (ii) realização de seminários para divulgação da técnica. As duas macro etapas finais caracterizam um estudo de caso, tendo sido desenvolvidas em um hospital; foram elas: (iii) Estudo-Piloto com desenvolvimento de um modelo computacional utilizando um software dedicado, no qual o grupo do hospital foi treinado, e (iv) utilização do modelo na definição das características de um novo serviço de atendimento. Durante todo o processo onze hospitais participaram da pesquisa realizada, aproximadamente cem pessoas assistiram a pelo menos um dos seminários e um hospital desenvolveu um estudo aplicado de simulação. Neste estudo a simulação foi utilizada para analisar alternativas para uma situação específica no hospital e um novo serviço alternativo foi criado a partir da análise realizada e do modelo desenvolvido. O resultado decorrente da simulação foi implementado na prática. Pode-se constatar neste trabalho o grande interesse dos hospitais em técnicas que auxiliem a tomada de decisão.

Fábricas de software e a academia: análise da formação acadêmica em informática no município do Rio de Janeiro

As Brazil wants to be perceived as a competitor in providing computer applications and system development services in the global market, the concept of Software Factory gains importance. The metaphor for the 'Factory', when applied to the activity of software development, is used to describe organizations which produce software with a minimum quality standard and at competitive costs. However, the term 'Factory' recalls Fordist concepts, which have been challenged for a few decades in the manufacturing industry. This study analyzed university curricula and how students and teachers perceive the concept of Software Factory and assessed them in relation to the Fordism ------------ post-Fordism /continuum/. It was observed that some of the teachers who have influence over curricula define Software Factories according to Fordist concepts. It was also observed that, despite opportunities for improvements, curricula are adequately structured with regards to the skills a professional at these organizations must possess. We conclude that education provided at the programs being analyzed is adequate, but that it must be supplemented by companies or by the professionals themselves so that the knowledge acquired in the programs may be put in practice.

Aprendizagem de escrita de língua de sinais pelo sistema SignWriting : língua de sinais no papel e no computador

Esta tese trata de como o sistema SignWriting pode servir de suporte a uma nova proposta pedagógica ao ensino da escrita de língua de sinais e letramento para crianças surdas usuárias da Língua Brasileira de Sinais - Libras e da Língua de Sinais Francesa - LSF. Escrever deve ser uma atividade significativa para a criança. No caso da criança surda, a escrita fundamenta-se em sua competência na língua de sinais, sem precisar da intermediação da língua oral. A criança surda, quando em um ambiente onde ela e seus colegas se comunicam em língua de sinais, efetivamente tenta escrever sinais, quando é incentivada a fazê-lo. Em nossos experimentos, usamos o sistema SignWriting para mostrar ás crianças surdas (e a seus pais e professores) como escrever textos em línguas de sinais de ambas as formas: manuscrita e impressa, usando o programa Sign Writer para editar textos em línguas de sinais. A base teórica que apóia a tese é a abordagem bilíngüe para a educação de surdos, a língua de sinais, a teoria de Piaget, e de Ferreiro quando trata das etapas da alfabetização em língua oral. Esta investigação possui um caráter exploratório, em que o delineamento metodológico é dado pela pesquisa-ação. O primeiro estudo apresenta um levantamento do processo de aquisição da escrita de sinais, em sua forma manuscrita, pela criança e jovem surdo no Brasil e na França. O segundo estudo trata da ajuda que a informática pode dar a essa aquisição e de como utilizamos os softwares de escrita de língua de sinais em aulas de introdução ao uso do computador e em transcrições da LSF de corpus vídeo para a escrita de língua de sinais. Os resultados sugerem que as crianças evoluem em sua escrita, pois muitos signos que elas escreveram não foram sugeridos pela experimentadora, nem por outro meio, mas surgiram espontaneamente. A introdução de um software como o Sign Writer ou o SW-Edit nas classes para introduzir as TI traz a essas aulas muito maior interesse do que quando usamos um editor de textos na língua oral. Também as produções das crianças são mais sofisticadas. As conclusões indicam que a escrita de língua de sinais incorporada à educação das crianças surdas pode significar um avanço significativo na consolidação de uma educação realmente bilíngüe, na evolução das línguas de sinais e aponta para a possibilidade de novas abordagens ao ensino da língua oral como segunda língua.

Auditoria externa em empresas que utilizam computador eletrônico: um estudo de casos

o objetivo deste estudo foi explorar a relação existente entre a li teratura sobre procedimentos de auditoria de PED e os procedimentos efetivamente utilizados pelas seis empresas de auditoria contábil no Brasil. Bus cou-se identificar a diferença entre os procedimentos de auditoria de PED utilizados pelas empresas nacionais e os utilizados pelas empresas de ori gem estrangei ra (Capitulo I). Na revisão de literatura, apresentam-se os atuais conhecimentos so bre a auditoria externa em empresas que utilizam sistemas complexos de com putador e as perspectivas previsiveis para o futuro (Capltulo 11). A seguir, apresenta-se a metodologia utilizada, justificando-se as razões de seu emprego neste tipo de estudo exploratório (Capltulo lU). Entrevistas utilizando um questionário contendo,em sua maioria, que~ tões abertas, possibilitaram uma descrição dos procedimentos de auditoria externa empregados pelas empresas de auditoria em clientes que utilizam computador (Capitulo IV). Os resultados obtidos possibilitaram uma análise dos procedimentos de auditoria de PED utilizados pelas seis empresas de auditoria pesquis~ das (Capitulo V). Finalmente, relacionando-se os resultados ã literatura existente, sao apresentadas conclusões, formuladas recomendações e sugeridos novos es tudos (Capitulo VI).

Gestão verde de tecnologia da informação e comunicação: fatores que influenciam a sua adoção em grandes empresas usuárias no Brasil

A crescente utilização de recursos de informática e comunicação nas empresas, visando modernização, agilidade, redução de custos e outros, tem trazido diversos benefícios, mas tem também se tornado um enorme problema para o planeta. A quantidade de lixo eletrônico (e-waste) gerada pelos equipamentos de informática e comunicação tem dobrado a cada cinco anos, se tornando um dos principais focos de atenção nos últimos anos. O volume de lixo eletrônico gerado pelo descarte de equipamentos de informática e comunicação (TIC), já ultrapassa a marca de 50 milhões de toneladas por ano, o que equivale a oito vezes a produção total de resíduos da cidade de São Paulo. O mercado brasileiro total de eletrônicos é considerado o quinto do mundo, depois da China, Estados Unidos, Japão e Rússia. A produção total de lixo eletrônico no Brasil em 2011 foi de um milhão de toneladas e a parte referente a equipamentos de TIC foi estimada em 98 mil toneladas. Frente a este contexto este estudo visa contribuir para a expansão do conhecimento na gestão verde da cadeia de suprimentos (GSCM) aplicado à realidade empresarial brasileira de TIC. Especificamente pretende-se identificar quais fatores influenciam o processo de adoção e aplicação da gestão verde de TIC, em grandes empresas usuárias de TIC no Brasil, a partir dos modelos propostos por Molla (2008) e Molla e Coopers (2008). Desta forma buscou-se responder ao seguinte problema de pesquisa: quais fatores influenciam grandes empresas usuárias de tecnologia da informação e comunicação (TIC) no Brasil na adoção de conceitos de gestão de verde? Para isto, foi realizado estudo de caso em seis grandes empresas, todas lideres em seus setores, representando grandes áreas de serviços e manufatura. Como resultado final, foi proposto um novo modelo analítico, que pareceu mais adequado ao setor de serviços. O estudo também identificou que na gestão verde de TIC empresas manufatureiras tem prioridades diferentes das de serviço. Muitas vezes seus desafios operacionais são mais críticos em relação à sustentabilidade, que a gestão verde de TIC em si. Por outro lado, o estudo dos serviços prestados pelo setor público apesar dos grandes orçamentos anuais, apontou restrições quanto aos aspectos legais e deficiência de qualificação e capacitação de seus colaboradores como fatores limitantes para a implantação de programas de gestão verde mais abrangentes.

Wow!: objects

Nowadays computers have advanced beyond the desktop into many parts of everyday life and objects. To achieve this we have to make the computer invisible, and making a computer invisible is not a matter of size of the hardware, it’s all about how the human perceives the computer. To make this possible, the interaction with the computer has to be done in an alternative way, such that the user doesn’t notice the usual computer interfaces (mouse and keyboard) when using it. Therefore this thesis focuses on physical objects that are interactive to achieve various purposes like persuasive objects for stress relief, persuasive objects to help the process of teaching, persuasive objects for fun, persuasive objects to display internet information and persuasive objects to make people feel more in community (exchange virtual emotions), persuasive objects are going to be created and evaluated to see if they have the power to simplify and turn our lives better. The persuasive objects developed employ technology like sensors, actuators, microcontrollers, and computer/web services’ communication. This Master thesis starts by presenting a comprehensive introduction of what are persuasive objects and some general information about several areas that are related to our persuasive objects like stress relief, work experience, multimedia education and other major aspects. It continues by describing related work done in this area. Then we have a detailed view of each persuasive object and finally this thesis finishes with a general conclusion and notion of future work.