1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/proof.org	Fri Oct 28 00:03:05 2011 -0700
     1.3 @@ -0,0 +1,151 @@
     1.4 +#+TITLE: WFF 'n Proof
     1.5 +#+AUTHOR: Dylan Holmes
     1.6 +#+MATHJAX: align:"left" mathml:t path:"../MathJax/MathJax.js"
     1.7 +#+STYLE: <link rel="stylesheet" type="text/css" href="../css/aurellem.css" />
     1.8 +#+OPTIONS:   H:3 num:t toc:t \n:nil @:t ::t |:t ^:t -:t f:t *:t <:t
     1.9 +#+SETUPFILE: ../templates/level-0.org
    1.10 +#+INCLUDE: ../templates/level-0.org
    1.11 +#+BABEL: :noweb yes :results verbatim :cache yes
    1.12 +
    1.13 +
    1.14 +* Introduction
    1.15 +WFF 'n Proof is a competitive dice game designed to teach logic. The
    1.16 +game is played with several dice whose faces are marked with logical
    1.17 +symbols; the goal is to arrange the dice into /well-formed formulas/ (WFFs) \mdash{}
    1.18 +expressions that are syntactically correct\mdash{}then to manipulate
    1.19 +these formulas to form valid proofs.
    1.20 +
    1.21 +** About the dice
    1.22 +WFF and Proof has small cubes and large cubes which you use like
    1.23 +dice. The small cubes have lower-case letters =p=, =q=, =r=, =s=, =i=,
    1.24 +and =o= inscribed on their faces, whereas the big cubes have
    1.25 +upper-case letters =C=, =A=, =K=, =E=, =N= and =R= on their faces. The
    1.26 +lower-case letters stand for /propositions/ that can be either true or
    1.27 +false, whereas the
    1.28 +upper-case letters stand for certain logical connectives:
    1.29 +
    1.30 +
    1.31 +| Symbol | Meaning |
    1.32 +|--------+---------|
    1.33 +| =C=    | Implies |
    1.34 +| =A=    | Or      |
    1.35 +| =K=    | And     |
    1.36 +| =E=    | Equals  |
    1.37 +|--------+---------|
    1.38 +| =N=    | Not     |
    1.39 +
    1.40 +** Well-formed formulas
    1.41 +An expression is a row of dice arranged left-to-right. An expression
    1.42 +is a well-formed formula (WFF) if and only if
    1.43 +- It is a =p=, =q=, =r=, or =s=; or
    1.44 +- It is an =N= followed by a WFF; or
    1.45 +- It is a =C=, =A=, =K=, or =E= followed by two WFFs.
    1.46 +
    1.47 +(Both the lower-case letters =i= and =o= and the upper-case letter =R=
    1.48 +are special, and are not used in forming WFFs)
    1.49 +
    1.50 +* Games you can play with WFF 'n Proof
    1.51 +** Shake a WFF
    1.52 +Shake a WFF is the simplest game; it teaches you to build and to
    1.53 +recognize well-formed formulas, skills that are fundamental to more advanced games. 
    1.54 +
    1.55 +#This game is for two or three players. 
    1.56 +Each player starts the game with two small cubes and one big cube;
    1.57 +these cubes constitute each player's hand. Divide the remaining cubes
    1.58 +evenly among the players so that each player has a pile of unused
    1.59 +cubes. Also allow space for completed WFFs.
    1.60 +
    1.61 +At the start of each turn, all of the players toss their dice
    1.62 +simultaneously; each player races to build the longest WFF possible
    1.63 +out of his own dice. As soon as a player is finished\mdash{}either he
    1.64 +has constructed the longest WFF possible or has found that it is impossible to make a WFF\mdash{}he
    1.65 +calls out \ldquo{}WFF!\rdquo{} or \ldquo{}No WFF!\rdquo{}. 
    1.66 +
    1.67 +When a player calls out \ldquo{}WFF!\rdquo{} or \ldquo{}No
    1.68 +WFF!\rdquo{}, the other players must stop to validate the caller's
    1.69 +claim. When a player confirms that the claim is correct, that player
    1.70 +calls out \ldquo{}Check!\rdquo{}. Now, either all the players believe
    1.71 +that the claim is correct, or they do not.
    1.72 +
    1.73 +
    1.74 +- If all the players confirm that the claim is correct, the caller
    1.75 +  puts his WFF in the area for completed WFFs, then replenishes his
    1.76 +  supply of cubes by replacing each of the cubes in his WFF with a
    1.77 +  cube from his unused-cubes pile (each big cube must be replaced with
    1.78 +  a big cube, and each small cube must be replaced with a small cube),
    1.79 +  then takes an additional cube from his pile and receives one
    1.80 +  point. The turn then ends.
    1.81 +
    1.82 +- If, when checking the caller's claim, a player believes that the
    1.83 +  claim was made in error, the player calls out
    1.84 +  \ldquo{}Challenge!\rdquo{}, then points out the mistake: 
    1.85 +  - If the caller has presented an expression that is not a WFF, the
    1.86 +    challenger shows that it is not a WFF.
    1.87 +  - If the caller has presented a WFF that is not the longest possible,
    1.88 +    the challenger shows how to make a longer WFF from the caller's
    1.89 +    cubes.
    1.90 +  - If it is possible to make a WFF from the caller's cubes but the
    1.91 +    caller claims it is impossible, the challenger shows how to make a
    1.92 +    WFF from the caller's cubes.
    1.93 +  The other players verify this challenge. If the challenge was made
    1.94 +  correctly, the challenging player wins a point and gains an extra
    1.95 +  cube from his pile whereas the calling player must return a cube to his
    1.96 +  pile. If the challenge was made wrongly, the challenger must return a
    1.97 +  cube to his pile. In either case, the turn ends.
    1.98 +
    1.99 +After the turn ends, the player can play another turn. The game ends
   1.100 +when a certain number of cubes are in the area for completed WFFs;
   1.101 +this number can be decided before the game begins.
   1.102 +
   1.103 +One final note is the rule for cubes:
   1.104 +#+begin_quote
   1.105 +*Cube Rule:* A player's hand must have either the same number of big
   1.106 + cubes and small cubes, or one more small cube than big cube. When
   1.107 + taking cubes from or returning cubes to your unusued cubes pile, you
   1.108 + must make sure to follow this rule.
   1.109 +#+end_quote
   1.110 +
   1.111 +
   1.112 +
   1.113 +
   1.114 +
   1.115 +
   1.116 +* Misc
   1.117 +
   1.118 +#+srcname: proof
   1.119 +#+begin_src clojure
   1.120 +(ns wff.proof)
   1.121 +
   1.122 +(defn arity[x]
   1.123 +  (first
   1.124 +   (keep-indexed
   1.125 +    (fn[i f](if (nil? (f x)) nil i))
   1.126 +    [#{'p 'q 'r 's}
   1.127 +     #{'N}
   1.128 +     #{'C 'A 'K 'E}])))
   1.129 +
   1.130 +(defn wff?
   1.131 +  [& symbols]
   1.132 +  ((fn[stack symbols]
   1.133 +     ;;(println stack symbols)
   1.134 +     (if (or(empty? symbols)(empty? stack))
   1.135 +       (and(empty? symbols)(empty? stack))
   1.136 +       (let [n (arity (first symbols))]
   1.137 +	 (if (nil? n)
   1.138 +	   false
   1.139 +	   (recur (concat (rest stack) (repeat n '*)) (rest symbols))))))
   1.140 +   '(*) symbols))
   1.141 +
   1.142 +#+end_src
   1.143 +
   1.144 +
   1.145 +
   1.146 +
   1.147 +
   1.148 +
   1.149 +* COMMENT tangle
   1.150 +
   1.151 +#+begin_src clojure :tangle ./proof.clj
   1.152 +<<proof>>
   1.153 +<<other-proof>>
   1.154 +#+end_src