O contato em um click: ser-com em um mundo supervirtualizado

O presente estudo tem como objetivo compreender os sentidos da experiência de jovens e adultos com a interação social virtual, partindo de suas narrativas. Inspiradas nas ideias de Martin Heidegger, especialmente em seu seminário A Questão da Técnica , refletiremos sobre os modos de ser-com, em tempos de tecnologia, internet, consumo e hipermodernidade, contexto deste estudo, onde as coisas são vivenciadas em seu extremo (hiperconsumo, hipercorpo, hipermercado, hipercartões). Neste cenário, a Internet e as Tecnologias de Informação e Comunicação estão mediando, cada vez mais o contato do homem com o mundo, reconfigurando a vida em sociedade. Diante disso, apresentamos A Era do Click , em que são possibilitados novos meios de estar com os outros. Este é um estudo qualitativo, baseado na fenomenologia de Heidegger, por ser favorecedora da compreensão dos sentidos da experiência em relação à questão problematizada. Como estratégias de pesquisa foram utilizadas sondagem de campo e entrevistas individuais, inspiradas nas narrativas de Walter Benjamin. Cinco colaboradores relataram suas experiências de ser-com no mundo virtual. A partir de seus relatos foi possível compreender que o espaço virtual se revela como mais um lócus, dentre tantos, no cotidiano do ser do homem, em que emergem diferentes modos de ser-com. Dependendo de sua abertura, a proximidade ou o distanciamento tornam-se relativos, do mesmo modo que o pessoal e o impessoal, o próprio e o impróprio. Além disso, tornou-se claro que, a virtualidade pode ajudar a lidar com a solidão e a angústia temporariamente, da mesma forma que pode tornar-se uma barreira para um contato mais aprofundado e autêntico com os outros. Os colaboradores demonstraram uma atitude de serenidade, um poder dizer sim e não simultaneamente à técnica moderna, além de uma postura de meditar sobre os modos como se conectam. Questionamos as implicações em longo prazo da virtualização do contato, estimulando novos estudos, sob a luz da fenomenologia heideggeriana

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