Constructing a Game Modelled After Logic and Proofs - Tenjin: A Smartphone Game

Abstract

Logical reasoning plays an important role in human behaviour and is widely used in everyday life. It is incorporated in contexts such as natural languages, mathematics and programming. However, the general knowledge in today’s society with regards to formal logic is lacking and does not reflect the important role it plays. This lack of knowledge may not be an issue in simple situations. However, in more complex situations, not having a formal understanding may lead to erroneous reasoning. One explanation for this knowledge gap may be the lack of formal education of logic in school, with the bulk being taught as late as in university. Tenjin, a smartphone game modelled after classical propositional logic in the style of sequent calculus, tries to mitigate this problem. Tenjin aims to make learning formal logic accessible to people in the age range of 13–25 by replacing the formal syntactic notation with an intuitive space-themed user interface. As a proof of concept for Tenjin, this paper describes a development- and design process which results in both an accurate software representation for a subset of classical propositional logic and its proof rules, and a tested and intuitive visualisation for users to interact with. Designing the visualisation was done through incremental testing. First, each designcandidate went through benchmark-tests using proofs of different difficulty. If a candidate passed the benchmark-tests, it then went through paper prototype-tests with real-life users. Development of the software was executed using well-founded software principles and tools, e.g. the S.O.L.I.D principles and different design patterns. After performing a thorough modelling process of the problem domain, the code-base was written in the programming language C# and the frameworks .NET and Unity.