#+TITLE: WFF 'n Proof

 #+AUTHOR: Dylan Holmes

 #+MATHJAX: align:"left" mathml:t path:"../MathJax/MathJax.js"

 #+STYLE: <link rel="stylesheet" type="text/css" href="../css/aurellem.css" />

 #+OPTIONS:   H:3 num:t toc:t \n:nil @:t ::t |:t ^:t -:t f:t *:t <:t

 #+SETUPFILE: ../templates/level-0.org

 #+INCLUDE: ../templates/level-0.org

 #+BABEL: :noweb yes :results verbatim :cache yes

 

 

 * Introduction

 WFF 'n Proof is a competitive dice game designed to teach logic. The

 game is played with several dice whose faces are marked with logical

 symbols; the goal is to arrange the dice into /well-formed formulas/ (WFFs) \mdash{}

 expressions that are syntactically correct\mdash{}then to manipulate

 these formulas to form valid proofs.

 

 ** About the dice

 WFF and Proof has small cubes and large cubes which you use like

 dice. The small cubes have lower-case letters =p=, =q=, =r=, =s=, =i=,

 and =o= inscribed on their faces, whereas the big cubes have

 upper-case letters =C=, =A=, =K=, =E=, =N= and =R= on their faces. The

 lower-case letters stand for /propositions/ that can be either true or

 false, whereas the

 upper-case letters stand for certain logical connectives:

 

 

 | Symbol | Meaning |

 |--------+---------|

 | =C=    | Implies |

 | =A=    | Or      |

 | =K=    | And     |

 | =E=    | Equals  |

 |--------+---------|

 | =N=    | Not     |

 

 ** Well-formed formulas

 An expression is a row of dice arranged left-to-right. An expression

 is a well-formed formula (WFF) if and only if

 - It is a =p=, =q=, =r=, or =s=; or

 - It is an =N= followed by a WFF; or

 - It is a =C=, =A=, =K=, or =E= followed by two WFFs.

 

 (Both the lower-case letters =i= and =o= and the upper-case letter =R=

 are special, and are not used in forming WFFs)

 

 * Games you can play with WFF 'n Proof

 ** Shake a WFF

 Shake a WFF is the simplest game; it teaches you to build and to

 recognize well-formed formulas, skills that are fundamental to more advanced games. 

 

 #This game is for two or three players. 

 Each player starts the game with two small cubes and one big cube;

 these cubes constitute each player's hand. Divide the remaining cubes

 evenly among the players so that each player has a pile of unused

 cubes. Also allow space for completed WFFs.

 

 At the start of each turn, all of the players toss their dice

 simultaneously; each player races to build the longest WFF possible

 out of his own dice. As soon as a player is finished\mdash{}either he

 has constructed the longest WFF possible or has found that it is impossible to make a WFF\mdash{}he

 calls out \ldquo{}WFF!\rdquo{} or \ldquo{}No WFF!\rdquo{}. 

 

 When a player calls out \ldquo{}WFF!\rdquo{} or \ldquo{}No

 WFF!\rdquo{}, the other players must stop to validate the caller's

 claim. When a player confirms that the claim is correct, that player

 calls out \ldquo{}Check!\rdquo{}. Now, either all the players believe

 that the claim is correct, or they do not.

 

 

 - If all the players confirm that the claim is correct, the caller

   puts his WFF in the area for completed WFFs, then replenishes his

   supply of cubes by replacing each of the cubes in his WFF with a

   cube from his unused-cubes pile (each big cube must be replaced with

   a big cube, and each small cube must be replaced with a small cube),

   then takes an additional cube from his pile and receives one

   point. The turn then ends.

 

 - If, when checking the caller's claim, a player believes that the

   claim was made in error, the player calls out

   \ldquo{}Challenge!\rdquo{}, then points out the mistake: 

   - If the caller has presented an expression that is not a WFF, the

     challenger shows that it is not a WFF.

   - If the caller has presented a WFF that is not the longest possible,

     the challenger shows how to make a longer WFF from the caller's

     cubes.

   - If it is possible to make a WFF from the caller's cubes but the

     caller claims it is impossible, the challenger shows how to make a

     WFF from the caller's cubes.

   The other players verify this challenge. If the challenge was made

   correctly, the challenging player wins a point and gains an extra

   cube from his pile whereas the calling player must return a cube to his

   pile. If the challenge was made wrongly, the challenger must return a

   cube to his pile. In either case, the turn ends.

 

 After the turn ends, the player can play another turn. The game ends

 when a certain number of cubes are in the area for completed WFFs;

 this number can be decided before the game begins.

 

 One final note is the rule for cubes:

 #+begin_quote

 *Cube Rule:* A player's hand must have either the same number of big

  cubes and small cubes, or one more small cube than big cube. When

  taking cubes from or returning cubes to your unusued cubes pile, you

  must make sure to follow this rule.

 #+end_quote

 

 

 

 

 

 

 * Misc

 

 #+srcname: proof

 #+begin_src clojure

 (ns wff.proof)

 

 (defn arity[x]

   (first

    (keep-indexed

     (fn[i f](if (nil? (f x)) nil i))

     [#{'p 'q 'r 's}

      #{'N}

      #{'C 'A 'K 'E}])))

 

 (defn wff?

   [& symbols]

   ((fn[stack symbols]

      ;;(println stack symbols)

      (if (or(empty? symbols)(empty? stack))

        (and(empty? symbols)(empty? stack))

        (let [n (arity (first symbols))]

 	 (if (nil? n)

 	   false

 	   (recur (concat (rest stack) (repeat n '*)) (rest symbols))))))

    '(*) symbols))

 

 #+end_src

 

 

 

 

 

 

 * COMMENT tangle

 

 #+begin_src clojure :tangle ./proof.clj

 <<proof>>

 <<other-proof>>

 #+end_src