Many enjoy solving logical puzzles as a form of recreation. In contrast, quite few do proofs in logic calculi for recreation; and often even computer science students have trouble doing formal proofs. However, doing a proof in a formal calculus can be seen as a game. You are supposed to prove a statement from some assumptions. The rules of the calculus allow you to simplify the goal statement, split the task into smaller subtask, or apply assumptions to make progress on a subgoal. Using a suitable visualization, doing a formal proof can be disguised as solving a puzzle. The visualization may also help thinking about the problem in more concrete, sensual terms, as opposed to the dry, abstract presentation encountered in mathematics.
A visualization scheme could be the following: an atomic proposition is presented as a playing card, each atom as a different one: ace of spades, ace of hearts, etc. The conjunction of two formulas can be a card with a bottom different from the top. For instance, a card labeled with both the ace of spades and the ace of hearts would be the conjunction of these two atoms. Ripping a conjunction card in two would give you both the conjuncts, and stitching two cards together would give you a conjunction card. A disjunction could be a card with a different label on the back than on the front. Moreover, the card is spinning, such that you see alternatively front and back. An implication would be a power card that allows you to trade a certain card for another. For instance, if you have a trading card labeled "A to B" and you have a card labeled "A" you can play both to get a card labeled "B". Falsity could be visualized as joker, it can fill for any card.
A proof (sub)goal is the task to produce a certain card (conclusion) given a hand of cards (assumptions). A goal could be visualized as a card outline which has to be filled with the matching real card. The conclusion can be modified according to the rules of logic. Say you have to prove "A or B", i.e., you see a spinning outline of a card with front A and back B, you can decide to go for A, and fix the card to the front side. If you have to prove "A and B", you can rip this card into two, giving you two goals: "A" and "B". If you have to prove "A implies B", you can obtain card "A" into your hand, but now have to prove "B".
The goal is to implement a smartphone game with a touch interface that mimics proving in formal logic. A suitable underlying proof calculus for this game is known under the name "Sequent Calculus". It allows transformations on both the hypothesis (playing a card) and the goal (breaking a goal into subgoals). As a first step, the model should be defined: the proof state, possible actions one can take according to the state, and how they transform the proof state. The model should be parameterized over the logic and the available proof rules. For instance, in usual propositional logic one can use assumptions any number of times (in the visualization: copy and discard cards), but in linear logic each assumption must be used exactly once. As a second step, this should be turned into a game with a suitable, intuitive visualization of the proof state and the actions. The visualization can be simple at first and become nicer in a third step (time permitting).
- Good programming skills.
- Some familiarity with smart phone programming (e.g. Android).
- Interest in logic and formal calculi.
D, DV F, IT and TM