rlm@2: #+TITLE: WFF 'n Proof
rlm@2: #+AUTHOR: Dylan Holmes
rlm@2: #+MATHJAX: align:"left" mathml:t path:"../MathJax/MathJax.js"
rlm@2: #+STYLE: <link rel="stylesheet" type="text/css" href="../css/aurellem.css" />
rlm@2: #+OPTIONS:   H:3 num:t toc:t \n:nil @:t ::t |:t ^:t -:t f:t *:t <:t
rlm@2: #+SETUPFILE: ../templates/level-0.org
rlm@2: #+INCLUDE: ../templates/level-0.org
rlm@2: #+BABEL: :noweb yes :results verbatim :cache yes
rlm@2: 
rlm@2: 
rlm@2: * Introduction
rlm@2: WFF 'n Proof is a competitive dice game designed to teach logic. The
rlm@2: game is played with several dice whose faces are marked with logical
rlm@2: symbols; the goal is to arrange the dice into /well-formed formulas/ (WFFs) \mdash{}
rlm@2: expressions that are syntactically correct\mdash{}then to manipulate
rlm@2: these formulas to form valid proofs.
rlm@2: 
rlm@2: ** About the dice
rlm@2: WFF and Proof has small cubes and large cubes which you use like
rlm@2: dice. The small cubes have lower-case letters =p=, =q=, =r=, =s=, =i=,
rlm@2: and =o= inscribed on their faces, whereas the big cubes have
rlm@2: upper-case letters =C=, =A=, =K=, =E=, =N= and =R= on their faces. The
rlm@2: lower-case letters stand for /propositions/ that can be either true or
rlm@2: false, whereas the
rlm@2: upper-case letters stand for certain logical connectives:
rlm@2: 
rlm@2: 
rlm@2: | Symbol | Meaning |
rlm@2: |--------+---------|
rlm@2: | =C=    | Implies |
rlm@2: | =A=    | Or      |
rlm@2: | =K=    | And     |
rlm@2: | =E=    | Equals  |
rlm@2: |--------+---------|
rlm@2: | =N=    | Not     |
rlm@2: 
rlm@2: ** Well-formed formulas
rlm@2: An expression is a row of dice arranged left-to-right. An expression
rlm@2: is a well-formed formula (WFF) if and only if
rlm@2: - It is a =p=, =q=, =r=, or =s=; or
rlm@2: - It is an =N= followed by a WFF; or
rlm@2: - It is a =C=, =A=, =K=, or =E= followed by two WFFs.
rlm@2: 
rlm@2: (Both the lower-case letters =i= and =o= and the upper-case letter =R=
rlm@2: are special, and are not used in forming WFFs)
rlm@2: 
rlm@2: * Games you can play with WFF 'n Proof
rlm@2: ** Shake a WFF
rlm@2: Shake a WFF is the simplest game; it teaches you to build and to
rlm@2: recognize well-formed formulas, skills that are fundamental to more advanced games. 
rlm@2: 
rlm@2: #This game is for two or three players. 
rlm@2: Each player starts the game with two small cubes and one big cube;
rlm@2: these cubes constitute each player's hand. Divide the remaining cubes
rlm@2: evenly among the players so that each player has a pile of unused
rlm@2: cubes. Also allow space for completed WFFs.
rlm@2: 
rlm@2: At the start of each turn, all of the players toss their dice
rlm@2: simultaneously; each player races to build the longest WFF possible
rlm@2: out of his own dice. As soon as a player is finished\mdash{}either he
rlm@2: has constructed the longest WFF possible or has found that it is impossible to make a WFF\mdash{}he
rlm@2: calls out \ldquo{}WFF!\rdquo{} or \ldquo{}No WFF!\rdquo{}. 
rlm@2: 
rlm@2: When a player calls out \ldquo{}WFF!\rdquo{} or \ldquo{}No
rlm@2: WFF!\rdquo{}, the other players must stop to validate the caller's
rlm@2: claim. When a player confirms that the claim is correct, that player
rlm@2: calls out \ldquo{}Check!\rdquo{}. Now, either all the players believe
rlm@2: that the claim is correct, or they do not.
rlm@2: 
rlm@2: 
rlm@2: - If all the players confirm that the claim is correct, the caller
rlm@2:   puts his WFF in the area for completed WFFs, then replenishes his
rlm@2:   supply of cubes by replacing each of the cubes in his WFF with a
rlm@2:   cube from his unused-cubes pile (each big cube must be replaced with
rlm@2:   a big cube, and each small cube must be replaced with a small cube),
rlm@2:   then takes an additional cube from his pile and receives one
rlm@2:   point. The turn then ends.
rlm@2: 
rlm@2: - If, when checking the caller's claim, a player believes that the
rlm@2:   claim was made in error, the player calls out
rlm@2:   \ldquo{}Challenge!\rdquo{}, then points out the mistake: 
rlm@2:   - If the caller has presented an expression that is not a WFF, the
rlm@2:     challenger shows that it is not a WFF.
rlm@2:   - If the caller has presented a WFF that is not the longest possible,
rlm@2:     the challenger shows how to make a longer WFF from the caller's
rlm@2:     cubes.
rlm@2:   - If it is possible to make a WFF from the caller's cubes but the
rlm@2:     caller claims it is impossible, the challenger shows how to make a
rlm@2:     WFF from the caller's cubes.
rlm@2:   The other players verify this challenge. If the challenge was made
rlm@2:   correctly, the challenging player wins a point and gains an extra
rlm@2:   cube from his pile whereas the calling player must return a cube to his
rlm@2:   pile. If the challenge was made wrongly, the challenger must return a
rlm@2:   cube to his pile. In either case, the turn ends.
rlm@2: 
rlm@2: After the turn ends, the player can play another turn. The game ends
rlm@2: when a certain number of cubes are in the area for completed WFFs;
rlm@2: this number can be decided before the game begins.
rlm@2: 
rlm@2: One final note is the rule for cubes:
rlm@2: #+begin_quote
rlm@2: *Cube Rule:* A player's hand must have either the same number of big
rlm@2:  cubes and small cubes, or one more small cube than big cube. When
rlm@2:  taking cubes from or returning cubes to your unusued cubes pile, you
rlm@2:  must make sure to follow this rule.
rlm@2: #+end_quote
rlm@2: 
rlm@2: 
rlm@2: 
rlm@2: 
rlm@2: 
rlm@2: 
rlm@2: * Misc
rlm@2: 
rlm@2: #+srcname: proof
rlm@2: #+begin_src clojure
rlm@2: (ns wff.proof)
rlm@2: 
rlm@2: (defn arity[x]
rlm@2:   (first
rlm@2:    (keep-indexed
rlm@2:     (fn[i f](if (nil? (f x)) nil i))
rlm@2:     [#{'p 'q 'r 's}
rlm@2:      #{'N}
rlm@2:      #{'C 'A 'K 'E}])))
rlm@2: 
rlm@2: (defn wff?
rlm@2:   [& symbols]
rlm@2:   ((fn[stack symbols]
rlm@2:      ;;(println stack symbols)
rlm@2:      (if (or(empty? symbols)(empty? stack))
rlm@2:        (and(empty? symbols)(empty? stack))
rlm@2:        (let [n (arity (first symbols))]
rlm@2: 	 (if (nil? n)
rlm@2: 	   false
rlm@2: 	   (recur (concat (rest stack) (repeat n '*)) (rest symbols))))))
rlm@2:    '(*) symbols))
rlm@2: 
rlm@2: #+end_src
rlm@2: 
rlm@2: 
rlm@2: 
rlm@2: 
rlm@2: 
rlm@2: 
rlm@2: * COMMENT tangle
rlm@2: 
rlm@2: #+begin_src clojure :tangle ./proof.clj
rlm@2: <<proof>>
rlm@2: <<other-proof>>
rlm@2: #+end_src