Mercurial > dylan

comparison proof.org @ 2:b4de894a1e2e

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