Mercurial > dylan

annotate 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
rev   line source
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