[pt] Neste trabalho propomos um framework lógico para sistemas de Dedução Natural rotulados. Sua meta-linguagem é baseada numa generalização dos esquemas de regras propostos por Prawitz, e o uso de rótulos permite a definição de lógicas intencionais como lógicas modais e de descrição, bem como a definição uniforme de quantificadores como o para um número não-renumerável de indivíduos vale a propriedade P (lógica de Keisler), ou para quase todos os indivíduos vale P (lógica de ultra-filtros), sem mencionar os quantificadores padrões de lógica de primeira-ordem. Mostramos também a implementação deste framework em um assistente de prova virtual disponível livremente na web, e comparamos a definição de sistemas lógicos nele com o mesmo feito em outros assistentes — Agda, Isabelle, Lean, Metamath. Como subproduto deste experimento comparativo, também contribuímos uma prova formal em Lean do postulado de Zolt em três dimensões usando o sistema Zp proposto por Giovaninni et al. / [en] We propose a Logical Framework for labelled Natural Deduction systems. Its meta-language is based on a generalization of the rule schemas proposed by Prawitz, and the use of labels allows the definition of intentional logics, such as Modal Logic and Description Logic, as well as some quantifiers, such as Keisler s for non-denumerable-many individuals property P, or for almost all individuals P holds, or generally P holds, not to mention standard first-order logic quantifiers, all in a uniform way. We also show an implementation of this framework as a freely-available web-based proof assistant. We then compare the definition of logical systems in our implementation and in other proof assistants — Agda, Isabelle, Lean, Metamath. As a sub-product of this comparison experiment, we contribute a formal proof (in Lean) of De Zolt s postulate for three dimensions, using the Zp system proposed by Giovaninni et al.

[pt] Em ambientes aquáticos, o uso tradicional de mergulhadores ou veiculos subaquáticos tripulados foi substituído por veículos subaquáticos não tripulados (como ROVs ou AUVs). Com vantagens em termos de redução de riscos de segurança, como exposição à pressão, temperatura ou falta de ar. Além disso, conseguem acessar áreas de extrema profundidade que até então não eram possiveis para o ser humano. Esses veiculos não tripulados são amplamente utilizados para inspeções como as necessárias para o descomissionamento de plataformas de petróleo Neste tipo de fiscalização é necessário analisar as condições do solo, da tu- bulação e, principalmente, se foi criado um ecossistema próximo à tubulação. Grande parte dos trabalhos realizados para a automação desses veículos utilizam diferentes tipos de sensores e GPS para realizar a percepção do ambiente. Devido à complexidade do ambiente de navegação, diferentes algoritmos de controle e automação têm sido testados nesta área, O interesse deste trabalho é fazer com que o autômato tome decisões através da análise de eventos visuais. Este método de pesquisa traz a vantagem de redução de custos para o projeto, visto que as câmeras possuem um preço inferior em relação aos sensores ou dispositivos GPS. A tarefa de inspeção autônoma tem vários desafios: detectar os eventos, processar as imagens e tomar a decisão de alterar a rota em tempo real. É uma tarefa altamente complexa e precisa de vários algoritmos trabalhando juntos para ter um bom desempenho. A inteligência artificial apresenta diversos algoritmos para automatizar, como os baseados em aprendizagem por reforço entre outros na área de detecção e classificação de imagens Esta tese de doutorado consiste em um estudo para criação de um sistema avançado de inspeção autônoma. Este sistema é capaz de realizar inspeções apenas analisando imagens da câmera AUV, usando aprendizagem de reforço profundo profundo para otimizar o planejamento do ponto de vista e técnicas de detecção de novidades. Contudo, este quadro pode ser adaptado a muitas outras tarefas de inspecção. Neste estudo foram utilizados ambientes realistas complexos, nos quais o agente tem o desafio de chegar da melhor forma possível ao objeto de interesse para que possa classificar o objeto. Vale ressaltar, entretanto, que os ambientes de simulação utilizados neste contexto apresentam certo grau de simplicidade carecendo de recursos como correntes marítimas on dinâmica de colisão em seus cenários simulados Ao final deste projeto, o Visual Inspection of Pipelines (VIP) framework foi desenvolvido e testado, apresentando excelentes resultados e ilustrando a viabilidade de redução do tempo de inspeção através da otimização do planejamento do ponto de vista. Esse tipo de abordagem, além de agregar conhecimento ao robô autônomo, faz com que as inspeções subaquáticas exijam pouca presença de ser humano (human-in-the-loop), justificando o uso das técnicas empregadas. / [en] In aquatic environments, the traditional use of divers or manned underwater vehicles has been replaced by unmanned underwater vehicles (such as ROVs or AUVs). With advantages in terms of reducing safety risks, such as exposure to pressure, temperature or shortness of breath. In addition, they are able to access areas of extreme depth that were not possible for humans until then. These unmanned vehicles are widely used for inspections, such as those required for the decommissioning of oil platforms. In this type of inspection, it is necessary to analyze the conditions of the soil, the pipeline and, especially, if an ecosystem was created close to the pipeline. Most of the works carried out for the automation of these vehicles use different types of sensors and GPS to perform the perception of the environment. Due to the complexity of the navigation environment, different control and automation algorithms have been tested in this area. The interest of this work is to make the automaton take decisions through the analysis of visual events. This research method provides the advantage of cost reduction for the project, given that cameras have a lower price compared to sensors or GPS devices. The autonomous inspection task has several challenges: detecting the events, processing the images and making the decision to change the route in real time. It is a highly complex task and needs multiple algorithms working together to perform well. Artificial intelligence presents many algorithms to automate, such as those based on reinforcement learning, among others in the area of image detection and classification. This doctoral thesis consists of a study to create an advanced autonomous inspection system. This system is capable of performing inspections only by analyzing images from the AUV camera, using deep reinforcement learning, and novelty detection techniques. However, this framework can be adapted to many other inspection tasks. In this study, complex realistic environments were used, in which the agent has the challenge of reaching the object of interest in the best possible way so that it can classify the object. It is noteworthy, however, that the simulation environments utilized in this context exhibit a certain degree of simplicity, lacking features like marine currents or collision dynamics in their simulated scenarios. At the conclusion of this project, a Visual Inspection of Pipelines (VIP) framework was developed and tested, showcasing excellent results and illustrating the feasibility of reducing inspection time through the optimization of viewpoint planning. This type of approach, in addition to adding knowledge to the autonomous robot, means that underwater inspections require little pres- ence of a human being (human-in-the-loop), justifying the use of the techniques employed.

[pt] No Brasil, há uma falta de investimento em tratamentos psicossociais para demência. A Terapia de Estimulação Cognitiva (CST) é uma intervenção psicossocial baseada em evidências para pessoas que vivem com demência (PvcD) que foi adaptada e validada para vários países. Desenvolvida no Reino Unido, a CST envolve 14 sessões que acontecem ao longo de sete semanas. Seu objetivo é melhorar a função cognitiva por meio de atividades em grupo temáticas, que estimulam implicitamente as habilidades, incluindo memória, função executiva e linguagem. As sessões seguem um conjunto de princípios básicos que incluem estimulação mental, novas ideias, pensamentos e associações e opiniões em vez de fatos. Estudos sugerem que a CST pode melhorar a cognição, o humor, a qualidade de vida e as atividades de vida diária em PvcD leve a moderada. No Brasil, um ensaio controlado randomizado (RCT) buscou investigar a viabilidade da CST no país. Os resultados sugerem que aqueles que participaram dos grupos da CST apresentaram melhora significativa nas medidas relativas ao humor e às atividades de vida diária. Devido à pandemia COVID-19, foram feitas adaptações para que a CST pudesse ser oferecida virtualmente (vCST). O primeiro estudo foi realizado juntamente com o RCT para acessar a perspectiva dos participantes do grupo e explorar os efeitos da CST. Foram realizadas entrevistas individuais semiestruturadas com as PvcD que participaram dos grupos e seus cuidadores (n = 23). As transcrições das entrevistas foram analisadas por meio da Framework Analysis. A partir da análise, dois temas gerais, Benefícios pessoais de fazer parte do grupo e Mudanças na vida diária e sete subtemas, Benefícios para cuidadores, Benefícios para pessoas com demência, Memória, Sociabilidade, Linguagem, Humor, Orientação, Atividades cotidianas e Sintomas comportamentais e psicológicos. Os resultados indicam que a CST traz benefícios pessoais percebidos às PvcD e aos cuidadores, e há muitas melhorias percebidas, que são consistentes com achados qualitativos anteriores e apoiadas por achados empíricos de ensaios da CST. O segundo estudo teve como objetivo acessar a experiência e as perspectivas das PvcD que participaram de grupos da vCST e seus cuidadores (n =25), durante a pandemia do COVID-19. As informações qualitativas que surgiram da análise serão comparadas com dados quantitativos para entender a eficácia e a viabilidade do vCST. As transcrições das entrevistas foram analisadas por meio daFramework Analysis. A partir da análise, dois temas gerais, Benefícios pessoais defazer parte do grupo e Design da vCST e 12 subtemas, Prazer, Estimulação mental, Estimulação contínua, Ocupação, Cognição, Humor, Sociabilidade, On-line, Duração, Estrutura de sessões, Centrada na pessoa e Baseada em evidências. Os achados indicam que a VCST levou a melhorias percebidas para a PvcD e trouxe benefícios pessoais para aqueles que participaram dos grupos. Resultados semelhantes são encontrados em estudos da CST, que sugerem que a vCST é viável, como a intervenção presencial. / [en] In Brazil, there is a lack of investment in psychosocial treatments for dementia. Cognitive Stimulation Therapy (CST) is an evidence-based psychosocial intervention for people living with dementia (PlwD) that has been adapted and validated to several countries. Developed in the UK, it involves 14 sessions over seven weeks. It aims to improve cognitive function through themed group activities, which implicitly stimulate skills including memory, executive function and language. Sessions follow a set of guiding principles which include mental stimulation, new ideas, thoughts and associations and opinions rather than facts. Studies suggest that CST can improve cognition, mood, quality of life and activities of daily living in mild to moderate dementia. In Brazil, a randomized controlled trial (RCT) sought to investigate the feasibility of CST in the country. The results suggest that those who took part in the CST groups had a significant improvement in measures relative to mood and activities of daily living. Due to the COVID-19 pandemic, adaptations were made for virtual delivery, and virtual CST (vCST) groups are being conducted. The first study was conducted alongside the randomized RCT to explore the real-life effectiveness of CST and to access the perspective of group participants. Individual semi-structured interviews were applied to PlwD who took part in the groups and their care partners (n = 23). The transcripts of interviews were analysed using Framework Analysis. From the analysis, two general themes, Personal benefits of being part of the group and Changes to daily living and 7 subthemes, Benefits for caregivers, Benefits por people with dementia, Memory, Sociability, Language, Mood, Orientation, Everyday activities and Behavioural and psychological symptoms have emerged. Results indicate that CST brings perceived personal benefits to PlwD and caregivers, and there are many perceived improvements, which are consistent with previous qualitative findings and supported by empirical findings from CST trials. The second study aimed to access the experience and perspectives of Plwd who have participated in vCST groups and their care partners (n = 25), during the COVID-19 pandemic. Qualitative information that has emerged from the analysis will be compared with quantitative data to understand the effectiveness and feasibility of vCST. The transcripts of interviews were analysed using Framework Analysis. From the analysis, two general themes, Personal benefits of being part of the group and Design of vCST and 12 subthemes, Enjoyment, Mental stimulation, Continued stimulation, Occupation, Cognition, Mood, Sociability, Online, Duration, Structure of sessions, Person-centred and Evidence-based have emerged. The findings indicate that vCST led to perceived improvements for PlwD and personal benefits for those who took part in the groups. Similar results are found in CST studies, which suggest that vCST is viable as studies have suggested with the face-to-face intervention.