|
rlm@2
|
1 #+TITLE: WFF 'n Proof
|
|
rlm@2
|
2 #+AUTHOR: Dylan Holmes
|
|
rlm@2
|
3 #+MATHJAX: align:"left" mathml:t path:"../MathJax/MathJax.js"
|
|
rlm@2
|
4 #+STYLE: <link rel="stylesheet" type="text/css" href="../css/aurellem.css" />
|
|
rlm@2
|
5 #+OPTIONS: H:3 num:t toc:t \n:nil @:t ::t |:t ^:t -:t f:t *:t <:t
|
|
rlm@2
|
6 #+SETUPFILE: ../templates/level-0.org
|
|
rlm@2
|
7 #+INCLUDE: ../templates/level-0.org
|
|
rlm@2
|
8 #+BABEL: :noweb yes :results verbatim :cache yes
|
|
rlm@2
|
9
|
|
rlm@2
|
10
|
|
rlm@2
|
11 * Introduction
|
|
rlm@2
|
12 WFF 'n Proof is a competitive dice game designed to teach logic. The
|
|
rlm@2
|
13 game is played with several dice whose faces are marked with logical
|
|
rlm@2
|
14 symbols; the goal is to arrange the dice into /well-formed formulas/ (WFFs) \mdash{}
|
|
rlm@2
|
15 expressions that are syntactically correct\mdash{}then to manipulate
|
|
rlm@2
|
16 these formulas to form valid proofs.
|
|
rlm@2
|
17
|
|
rlm@2
|
18 ** About the dice
|
|
rlm@2
|
19 WFF and Proof has small cubes and large cubes which you use like
|
|
rlm@2
|
20 dice. The small cubes have lower-case letters =p=, =q=, =r=, =s=, =i=,
|
|
rlm@2
|
21 and =o= inscribed on their faces, whereas the big cubes have
|
|
rlm@2
|
22 upper-case letters =C=, =A=, =K=, =E=, =N= and =R= on their faces. The
|
|
rlm@2
|
23 lower-case letters stand for /propositions/ that can be either true or
|
|
rlm@2
|
24 false, whereas the
|
|
rlm@2
|
25 upper-case letters stand for certain logical connectives:
|
|
rlm@2
|
26
|
|
rlm@2
|
27
|
|
rlm@2
|
28 | Symbol | Meaning |
|
|
rlm@2
|
29 |--------+---------|
|
|
rlm@2
|
30 | =C= | Implies |
|
|
rlm@2
|
31 | =A= | Or |
|
|
rlm@2
|
32 | =K= | And |
|
|
rlm@2
|
33 | =E= | Equals |
|
|
rlm@2
|
34 |--------+---------|
|
|
rlm@2
|
35 | =N= | Not |
|
|
rlm@2
|
36
|
|
rlm@2
|
37 ** Well-formed formulas
|
|
rlm@2
|
38 An expression is a row of dice arranged left-to-right. An expression
|
|
rlm@2
|
39 is a well-formed formula (WFF) if and only if
|
|
rlm@2
|
40 - It is a =p=, =q=, =r=, or =s=; or
|
|
rlm@2
|
41 - It is an =N= followed by a WFF; or
|
|
rlm@2
|
42 - It is a =C=, =A=, =K=, or =E= followed by two WFFs.
|
|
rlm@2
|
43
|
|
rlm@2
|
44 (Both the lower-case letters =i= and =o= and the upper-case letter =R=
|
|
rlm@2
|
45 are special, and are not used in forming WFFs)
|
|
rlm@2
|
46
|
|
rlm@2
|
47 * Games you can play with WFF 'n Proof
|
|
rlm@2
|
48 ** Shake a WFF
|
|
rlm@2
|
49 Shake a WFF is the simplest game; it teaches you to build and to
|
|
rlm@2
|
50 recognize well-formed formulas, skills that are fundamental to more advanced games.
|
|
rlm@2
|
51
|
|
rlm@2
|
52 #This game is for two or three players.
|
|
rlm@2
|
53 Each player starts the game with two small cubes and one big cube;
|
|
rlm@2
|
54 these cubes constitute each player's hand. Divide the remaining cubes
|
|
rlm@2
|
55 evenly among the players so that each player has a pile of unused
|
|
rlm@2
|
56 cubes. Also allow space for completed WFFs.
|
|
rlm@2
|
57
|
|
rlm@2
|
58 At the start of each turn, all of the players toss their dice
|
|
rlm@2
|
59 simultaneously; each player races to build the longest WFF possible
|
|
rlm@2
|
60 out of his own dice. As soon as a player is finished\mdash{}either he
|
|
rlm@2
|
61 has constructed the longest WFF possible or has found that it is impossible to make a WFF\mdash{}he
|
|
rlm@2
|
62 calls out \ldquo{}WFF!\rdquo{} or \ldquo{}No WFF!\rdquo{}.
|
|
rlm@2
|
63
|
|
rlm@2
|
64 When a player calls out \ldquo{}WFF!\rdquo{} or \ldquo{}No
|
|
rlm@2
|
65 WFF!\rdquo{}, the other players must stop to validate the caller's
|
|
rlm@2
|
66 claim. When a player confirms that the claim is correct, that player
|
|
rlm@2
|
67 calls out \ldquo{}Check!\rdquo{}. Now, either all the players believe
|
|
rlm@2
|
68 that the claim is correct, or they do not.
|
|
rlm@2
|
69
|
|
rlm@2
|
70
|
|
rlm@2
|
71 - If all the players confirm that the claim is correct, the caller
|
|
rlm@2
|
72 puts his WFF in the area for completed WFFs, then replenishes his
|
|
rlm@2
|
73 supply of cubes by replacing each of the cubes in his WFF with a
|
|
rlm@2
|
74 cube from his unused-cubes pile (each big cube must be replaced with
|
|
rlm@2
|
75 a big cube, and each small cube must be replaced with a small cube),
|
|
rlm@2
|
76 then takes an additional cube from his pile and receives one
|
|
rlm@2
|
77 point. The turn then ends.
|
|
rlm@2
|
78
|
|
rlm@2
|
79 - If, when checking the caller's claim, a player believes that the
|
|
rlm@2
|
80 claim was made in error, the player calls out
|
|
rlm@2
|
81 \ldquo{}Challenge!\rdquo{}, then points out the mistake:
|
|
rlm@2
|
82 - If the caller has presented an expression that is not a WFF, the
|
|
rlm@2
|
83 challenger shows that it is not a WFF.
|
|
rlm@2
|
84 - If the caller has presented a WFF that is not the longest possible,
|
|
rlm@2
|
85 the challenger shows how to make a longer WFF from the caller's
|
|
rlm@2
|
86 cubes.
|
|
rlm@2
|
87 - If it is possible to make a WFF from the caller's cubes but the
|
|
rlm@2
|
88 caller claims it is impossible, the challenger shows how to make a
|
|
rlm@2
|
89 WFF from the caller's cubes.
|
|
rlm@2
|
90 The other players verify this challenge. If the challenge was made
|
|
rlm@2
|
91 correctly, the challenging player wins a point and gains an extra
|
|
rlm@2
|
92 cube from his pile whereas the calling player must return a cube to his
|
|
rlm@2
|
93 pile. If the challenge was made wrongly, the challenger must return a
|
|
rlm@2
|
94 cube to his pile. In either case, the turn ends.
|
|
rlm@2
|
95
|
|
rlm@2
|
96 After the turn ends, the player can play another turn. The game ends
|
|
rlm@2
|
97 when a certain number of cubes are in the area for completed WFFs;
|
|
rlm@2
|
98 this number can be decided before the game begins.
|
|
rlm@2
|
99
|
|
rlm@2
|
100 One final note is the rule for cubes:
|
|
rlm@2
|
101 #+begin_quote
|
|
rlm@2
|
102 *Cube Rule:* A player's hand must have either the same number of big
|
|
rlm@2
|
103 cubes and small cubes, or one more small cube than big cube. When
|
|
rlm@2
|
104 taking cubes from or returning cubes to your unusued cubes pile, you
|
|
rlm@2
|
105 must make sure to follow this rule.
|
|
rlm@2
|
106 #+end_quote
|
|
rlm@2
|
107
|
|
rlm@2
|
108
|
|
rlm@2
|
109
|
|
rlm@2
|
110
|
|
rlm@2
|
111
|
|
rlm@2
|
112
|
|
rlm@2
|
113 * Misc
|
|
rlm@2
|
114
|
|
rlm@2
|
115 #+srcname: proof
|
|
rlm@2
|
116 #+begin_src clojure
|
|
rlm@2
|
117 (ns wff.proof)
|
|
rlm@2
|
118
|
|
rlm@2
|
119 (defn arity[x]
|
|
rlm@2
|
120 (first
|
|
rlm@2
|
121 (keep-indexed
|
|
rlm@2
|
122 (fn[i f](if (nil? (f x)) nil i))
|
|
rlm@2
|
123 [#{'p 'q 'r 's}
|
|
rlm@2
|
124 #{'N}
|
|
rlm@2
|
125 #{'C 'A 'K 'E}])))
|
|
rlm@2
|
126
|
|
rlm@2
|
127 (defn wff?
|
|
rlm@2
|
128 [& symbols]
|
|
rlm@2
|
129 ((fn[stack symbols]
|
|
rlm@2
|
130 ;;(println stack symbols)
|
|
rlm@2
|
131 (if (or(empty? symbols)(empty? stack))
|
|
rlm@2
|
132 (and(empty? symbols)(empty? stack))
|
|
rlm@2
|
133 (let [n (arity (first symbols))]
|
|
rlm@2
|
134 (if (nil? n)
|
|
rlm@2
|
135 false
|
|
rlm@2
|
136 (recur (concat (rest stack) (repeat n '*)) (rest symbols))))))
|
|
rlm@2
|
137 '(*) symbols))
|
|
rlm@2
|
138
|
|
rlm@2
|
139 #+end_src
|
|
rlm@2
|
140
|
|
rlm@2
|
141
|
|
rlm@2
|
142
|
|
rlm@2
|
143
|
|
rlm@2
|
144
|
|
rlm@2
|
145
|
|
rlm@2
|
146 * COMMENT tangle
|
|
rlm@2
|
147
|
|
rlm@2
|
148 #+begin_src clojure :tangle ./proof.clj
|
|
rlm@2
|
149 <<proof>>
|
|
rlm@2
|
150 <<other-proof>>
|
|
rlm@2
|
151 #+end_src
|
