A lógica formal possui um papel fundamental na ciência da computação. Infelizmente, se observa que a eficácia do processo de ensino-aprendizagem da lógica formal tem se mostrado abaixo do ideal. Este trabalho apresenta o sistema ∃lementar, um sistema que incorpora um assistente de provas em um contexto de gamificação, i.e., que utiliza elementos de jogos para promover o engajamento e a motivação dos alunos. Após introduzir as caracterı́sticas gerais do sistema ∃lementar, este artigo apresenta dados preliminares que indicam melhoria nos indicadores de desempenho dos alunos.

A lógica formal desempenha um papel fundamental na ciência da computação. É necessário introduzir os fundamentos dessa disciplina para que esses alunos possam alcançar o domínio em todas as suas aplicações em ciência da computação. Infelizmente, observa-se que a eficiência do processo de aprendizagem do programa de Bacharelado em Sistemas de Informação se mostrou menos do que ideal. Neste trabalho, propomos que é possível aumentar a efetividade do processo de aprendizagem através do uso de assistentes de prova como ferramenta de ensino, mas com a introdução de elementos do tipo jogo. Essa abordagem é conhecida como gamificação. Apresentamos uma visão geral da base teórica que apóia o uso da gamificação. Em seguida, descrevemos a proposta de um sistema gamificado para o aprendizado da lógica formal, bem como a implementação de um protótipo desse sistema proposto. Concluímos este artigo apresentando alguns resultados de um experimento realizado adotando nosso protótipo como ferramenta de aprendizado durante um semestre acadêmico. Em seguida, comparamos esses resultados com o semestre anterior e analisamos as possibilidades do uso da gamificação em um ambiente educacional.

Multi-valued Model Checking extends classical, two-valued model checking to multi-valued logic such as Quasi-Boolean logic. The added expressivity is useful in dealing with such concepts as incompleteness and uncertainty in target systems, while it comes with the cost of time and space. Chechik and others proposed an efficient reduction from multi-valued model checking problems to two-valued ones, but to the authors' knowledge, no study was done for multi-valued bounded model checking. In this paper, we propose a novel, efficient algorithm for multi-valued bounded model checking. A notable feature of our algorithm is that it is not based on reduction of multi-values into two-values; instead, it generates a single formula which represents multi-valuedness by a suitable encoding, and asks a standard SAT solver to check its satisfiability. Our experimental results show a significant improvement in the number of variables and clauses and also in execution time compared with the reduction-based one.

Multi-valued Model Checking is an extension of classical, two-valued model checking with multi-valued logic. Multi-valuedness has been proved useful in expressing additional information such as incompleteness, uncertainty, and many others, but with the cost of time and space complexity. This paper addresses this problem, and proposes a new algorithm for Multi-valued Model Checking. While Chechik et al. have extended BDD-based Symbolic Model Checking algorithm to the multi-valued case, our algorithm extends Bounded Model Checking (BMC), which can generate a counterexample of minimum length efficiently (if any). A notable feature of our algorithm is that it directly generates conjunctive normal forms, and never reduces multi-valued formulas into many slices of two-valued formulas. To achieve this feature, we extend the BMC algorithm to the multi-valued case and also devise a new translation of multi-valued propositional formulas. Finally, we show experimental results and compare the performance of our algorithm with that of a reduction-based algorithm.