Formal logic plays a fundamental role in computer science. Unfortunately, it is observed that the effectiveness of the learning process of formal logic has proved to be less than ideal. This work presents the ∃lementar system; a system that integrates a proof assistant in a gamified context, i.e., that uses game elements to promote student’s engagement and motivation. After introducing ∃lementar’s main features, this work presents preliminary data that point to an improvement in student’s performance indicators.

Formal logic plays a fundamental role in computer science. It is necessary to introduce the fundamentals of this discipline so that these students can achieve mastery across the range of its applications in computer science. Unfortunately, it is observed that the efficiency of the learning process the Bachelor in Information Systems program, has proved to be less than ideal. In this work, we propose that it is possible to increase the effectiveness of the learning process through the use of proof assistants as a teaching tool, but with the introduction of game-like elements. This approach has been known as gamification. We present an overview of the theoretical basis that supports the use of gamification, we then proceed to describe a proposal of a gamified system for learning formal logic, as well as a prototype implementation of this proposed system. We conclude this paper presenting some results of an experiment conducted by adopting our prototype as a learning tool during one academic semester. We then compare these results with the previous semester and analyze the possibilities of the use of gamification in an educational setting.

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.