(************** Content-type: application/mathematica ************** CreatedBy='Mathematica 5.0' Mathematica-Compatible Notebook This notebook can be used with any Mathematica-compatible application, such as Mathematica, MathReader or Publicon. The data for the notebook starts with the line containing stars above. To get the notebook into a Mathematica-compatible application, do one of the following: * Save the data starting with the line of stars above into a file with a name ending in .nb, then open the file inside the application; * Copy the data starting with the line of stars above to the clipboard, then use the Paste menu command inside the application. Data for notebooks contains only printable 7-bit ASCII and can be sent directly in email or through ftp in text mode. Newlines can be CR, LF or CRLF (Unix, Macintosh or MS-DOS style). NOTE: If you modify the data for this notebook not in a Mathematica- compatible application, you must delete the line below containing the word CacheID, otherwise Mathematica-compatible applications may try to use invalid cache data. For more information on notebooks and Mathematica-compatible applications, contact Wolfram Research: web: http://www.wolfram.com email: info@wolfram.com phone: +1-217-398-0700 (U.S.) Notebook reader applications are available free of charge from Wolfram Research. *******************************************************************) (*CacheID: 232*) (*NotebookFileLineBreakTest NotebookFileLineBreakTest*) (*NotebookOptionsPosition[ 113510, 3790]*) (*NotebookOutlinePosition[ 128572, 4329]*) (* CellTagsIndexPosition[ 125447, 4206]*) (*WindowFrame->Normal*) Notebook[{ Cell["\[Copyright] K. Sutner 2004", "Text"], Cell[CellGroupData[{ Cell["Logic", "Title", CellTags->"c:1"], Cell[CellGroupData[{ Cell["Tautologies", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:2"], Cell[CellGroupData[{ Cell["Task:", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:3"], Cell[TextData[{ "Determine which of the following formulas are tautologies.\n\na) ", Cell[BoxData[ \(TraditionalForm\`Q\ \[And] \ \[Not] Q\ \[DoubleLongRightArrow]\ P\)]], "\nb) ", Cell[BoxData[ \(TraditionalForm\`P\ \[And] \ Q\ \[DoubleLongRightArrow]\ P\)]], "\nc) ", Cell[BoxData[ \(TraditionalForm\`P\ \ \[DoubleLongRightArrow]\ P\ \[Or] \ Q\)]], "\n\nMake sure your arguments are clear and simple." }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, FontFamily->"Times", FontSize->18, CellTags->"c:4"], Cell[TextData[{ "a) ", Cell[BoxData[ \(TraditionalForm\`Q\ \[And] \ \[Not] Q\ \[DoubleLongRightArrow]\ P\)]], "\n", Cell[BoxData[ \(TraditionalForm\`Q\ \[And] \ \[Not] \ Q\)]], " is a contradiction, hence the premise of the implication is always \ false. But then the implication is a tautology. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "b) ", Cell[BoxData[ \(TraditionalForm\`P\ \[And] \ Q\ \[DoubleLongRightArrow]\ P\)]], "\nIf ", Cell[BoxData[ \(TraditionalForm\`P\ \[And] \ Q\)]], " is true, ", Cell[BoxData[ \(TraditionalForm\`P\)]], " must be true, hence the implication is true. But if ", Cell[BoxData[ \(TraditionalForm\`P\ \[And] \ \ Q\)]], " is false, the implication is automatically true. Hence, the implication \ is a tautology. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "c) ", Cell[BoxData[ \(TraditionalForm\`P\ \ \[DoubleLongRightArrow]\ P\ \[Or] \ Q\)]], "\nIf ", Cell[BoxData[ \(TraditionalForm\`\(\(P\)\(\ \)\)\)]], " is true, ", Cell[BoxData[ \(TraditionalForm\`\(\(\(P\)\(\ \)\)\(\[Or]\)\(\ \)\(Q\)\(\ \)\)\)]], " is also true, hence the implication is true. But if ", Cell[BoxData[ \(TraditionalForm\`\(\(P\)\(\ \)\)\)]], " is false, the implication is automatically true. Hence, the implication \ is a tautology. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Normal Forms", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:5"], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:6"], Cell[TextData[{ "Convert the following formulae into CNF and DNF.\n\na) ", Cell[BoxData[ \(TraditionalForm\`p\ \[LongLeftRightArrow]\ q\)]], "\nb) ", Cell[BoxData[ \(TraditionalForm\`\[Not] \((\ p\ \[And] \ q \[And] \ \[Not] r)\)\ \[Rule] \ \((p \[Rule] \ q)\)\)]], "\n\nAgain, you can tackle this problem by hand, or by computer. You are \ probably better off just doing it by hand. " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", CellTags->"c:7"], Cell[CellGroupData[{ Cell["Part a", "Subsubsection", CellTags->"c:8"], Cell[TextData[{ "Our formula is ", Cell[BoxData[ \(TraditionalForm\`\((p \[Rule] q)\)\ \[And] \ \((q \[Rule] p)\)\)]], " and is clearly true if, and only if, the truth assignment for ", Cell[BoxData[ \(TraditionalForm\`p\)]], " is the same as for ", Cell[BoxData[ \(TraditionalForm\`q\)]], ". This is easy to write down in DNF:\n\n\t", Cell[BoxData[ \(TraditionalForm\`\((p\ \[And] \ q)\)\ \[Or] \ \((\[Not] p \[And] \ \[Not] q)\)\)]], ".\n\nBy distributing and cancellation we get CNF \n\n\t", Cell[BoxData[ \(TraditionalForm\`\((p\ \[Or] \ \[Not] q)\)\ \[And] \ \((\[Not] p\ \ \[And] \ q)\)\)]], ".\n" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part b", "Subsubsection", CellTags->"c:9"], Cell[TextData[{ "Our formula is\n\t\t ", Cell[BoxData[ \(TraditionalForm\`\[Not] \((p \[And] q\ \[And] \ \[Not] r)\)\ \ \[Rule] \ \((\[Not] p \[Or] q)\)\)]], ". \n\nWe can rewrite this implication as\n\n\t\t ", Cell[BoxData[ \(TraditionalForm\`\[Not] \(\[Not] \((p \[And] q\ \[And] \ \[Not] r)\)\)\ \ \[Or] \ \((\[Not] p \[Or] q)\)\)]], "\nand get \n\n\t\t ", Cell[BoxData[ \(TraditionalForm\`\((p \[And] q\ \[And] \ \[Not] r)\)\ \ \[Or] \ \((\ \[Not] p \[Or] q\ )\)\)]], ".\n\t\t \nBut the truth value of this formula does not depend on ", Cell[BoxData[ \(TraditionalForm\`r\)]], " (clear for ", Cell[BoxData[ \(TraditionalForm\`r \[Rule] \ True\)]], ", and a little calculation for ", Cell[BoxData[ \(TraditionalForm\`r \[Rule] False\)]], "). Hence the formula is equivalent to just \n\n\t\t", Cell[BoxData[ \(TraditionalForm\`\[Not] \ p\ \[Or] \ \ q\)]], "\n\t\t\nwhich is already in both DNF and CNF." }], "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Liars", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:10"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", CellTags->"c:11"], Cell["\<\ There are many puzzles that can be tackled by some logical \ reasoning. Here is a relatively simple one. There is an island where all the inhabitants are either chronical liars or \ always truthful. They all know each other, and know who lies and who says \ the truth. A stranger comes to the island and runs into three natives. The \ make the following assertions: \tA: \"We three are all liars.\" \tB: \"Exactly two of us are liars.\" \tC: \"The other two are liars.\"\ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:12"], Cell[TextData[{ "Which, if any, of these statements should the stranger believe? \nJustify \ your answer. \n\nYou can use ", StyleBox["Mathematica", FontSlant->"Italic"], " to do this, but it's probably easier to just use plain reasoning." }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, FontFamily->"Times", FontSize->18, CellTags->"c:13"], Cell["\<\ First note that A must be a liar: otherwise he would be telling the \ truth, but that contradicts his own statement. Hence, at least one of B and \ C must be telling the truth. Suppose B is telling the truth. Then A and C would have to be liars. For C, \ this means that one of A and B is not a liar, which is fine, since B is in \ fact telling the truth. On the other hand, if B lies, then there is at most one liar. But A is \ already a liar, and we have a contradiction. Hence A and C are liars, and B is telling the truth.\ \>", "Text"], Cell[TextData[{ "Note we could also model this by propositional formulae: ", Cell[BoxData[ \(TraditionalForm\`a\)]], " stands for \"A is saying the truth\" , and so on." }], "Text"], Cell["\<\ f1 = And[ Implies[ a, Not[Or[a,b,c]] ] , \t Implies[ Not[Or[a,b,c]], a ] ];\ \>", "Input"], Cell["\<\ f2 = And[ Implies[ b, exactlyTwo[Not[a],Not[b],Not[c]]] , Implies[ exactlyTwo[Not[a],Not[b],Not[c]], b ] ];\ \>", "Input"], Cell["\<\ f3 = And[ Implies[ c, And[Not[a],Not[b]] ] , Implies[ And[Not[a],Not[b]], c ] ];\ \>", "Input"], Cell["And[f1,f2,f3] // LogicalExpand", "Input"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Sums and Products", "Section", CellTags->"c:14"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", CellTags->"c:15"], Cell["\<\ When dealing with communication protocols and security, one often \ has to use more than just plain propositional logic: one also has to be able \ to draw conclusions from the (supposedly intelligent and rational) behavior \ of other people (or computers). These problems can be quite hard in general, \ but the one below is manageable. The one below requires some logical reasoning, as well as brute force \ calculation. But don't try brute force all the way, you have to reason \ first. \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:16"], Cell[TextData[{ "Suppose ", Cell[BoxData[ \(TraditionalForm\`x\)]], " and ", Cell[BoxData[ \(TraditionalForm\`y\)]], " are two integers in the range from 2 to 99. Compute their sum and \ product, and reveal the sum to Ms. S, and the product to Mr. P. Neither S \ nor P knows the other value. \n\n\tS:\t", Cell[BoxData[ \(TraditionalForm\`\(\(x\)\(\ \)\(+\)\(\ \)\(y\)\(\ \)\) = \ s\)]], "\n\tP:\t", Cell[BoxData[ \(TraditionalForm\`x\ y\ = \ p\)]], "\n\n\[Bullet] A day later, S calls P and tells him that he cannot \ possibly know ", Cell[BoxData[ \(TraditionalForm\`x\)]], " and ", Cell[BoxData[ \(TraditionalForm\`y\)]], ". \n\[Bullet] P thinks about this for a while, calls back S and tells \ her: \"I now know ", Cell[BoxData[ \(TraditionalForm\`x\)]], " and ", Cell[BoxData[ \(TraditionalForm\`y\)]], ".\"\n\[Bullet] S ponders for a while, calls up P, and says: \"I too know \ the numbers.\"\n \nWhat are the two numbers?\n\nWe have to make some tacit \ assumptions here: both S and P are rational beings, they know arithmetic, \ they don't lie. Of course, it's also not clear that there is a solution, or \ that it is unique -- you will see, it is. " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Hint", "Subsubsection", CellTags->"c:17"], Cell[TextData[{ "First figure out how much information S can extract from ", Cell[BoxData[ \(TraditionalForm\`s\)]], " : what are the possible values of ", Cell[BoxData[ \(TraditionalForm\`p\)]], " (or, alternatively, of ", Cell[BoxData[ \(TraditionalForm\`x\)]], " and ", Cell[BoxData[ \(TraditionalForm\`y\)]], "). Do the same for P. \n\nYou might find the function ", StyleBox["Divisors[]", "Input"], " very helpful.\n\nThen extract more information from the phone calls \ \[Ellipsis] " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsubsection", CellTags->"c:18"], Cell["Sit back, relax, get a bottle of the good stuff. ", "Text"], Cell[TextData[{ "We may safely assume that ", Cell[BoxData[ \(TraditionalForm\`2\ \[LessEqual] \ x\ \[LessEqual] \ y\ \[LessEqual] \ 99\)]], ". \nNote that it suffices for P to determine ", Cell[BoxData[ \(TraditionalForm\`s\)]], ", and for S to determine ", Cell[BoxData[ \(TraditionalForm\`p\)]], ".\n\nHere are functions that produce all possible values for ", Cell[BoxData[ \(TraditionalForm\`s\)]], " and ", Cell[BoxData[ \(TraditionalForm\`p\)]], ", given ", Cell[BoxData[ \(TraditionalForm\`p\)]], " and ", Cell[BoxData[ \(TraditionalForm\`s\)]], ", respectively. \nNo union is needed for the first function, since we are \ looking at an ascending branch of a parabola. " }], "Text"], Cell[BoxData[{ \(\(toprod[s_] := With[{num = Range[2, s/2]}, num\ \((s - num)\)];\)\), "\n", \(\(tosum[p_] := With[{div = Most@\(Rest@Divisors[p]\)}, Union[div + p/div]];\)\)}], "Input"], Cell[TextData[{ "Let's determine all products possibly associated with ", Cell[BoxData[ \(TraditionalForm\`s\ = \ 100\)]], ". " }], "Text"], Cell["toprod[100]", "Input"], Cell["\<\ Some of these products are assoicated with just one sum, others \ with several.\ \>", "Text"], Cell["\<\ tosum[291] tosum[384]\ \>", "Input"], Cell[TextData[{ "Thus, ", Cell[BoxData[ \(TraditionalForm\`p\ = \ 291\)]], " can be associated with only one sum ", Cell[BoxData[ \(TraditionalForm\`\(\(\(s\)\(\ \)\)\(=\)\(100\)\(\ \)\)\)]], ", but ", Cell[BoxData[ \(TraditionalForm\`p = 384\)]], " can be associated with 7 different values for ", Cell[BoxData[ \(TraditionalForm\`s\)]], ". Hence, for some values of ", Cell[BoxData[ \(TraditionalForm\`x\)]], " and ", Cell[BoxData[ \(TraditionalForm\`y\)]], ", P could actually figure out what they are, but not for others. Poor S \ is always lost (except in the degenerate cases ", Cell[BoxData[ \(TraditionalForm\`s = 4, \ 5, \ 195, \)]], Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(196\)\)\)]], "). \n\nHow can P determine the possible ", Cell[BoxData[ \(TraditionalForm\`s\)]], " values? One way is to use the function ", StyleBox["tosum[]", "Input", FontWeight->"Bold"], " from above, which is based on ", StyleBox["Divisors[]", "Input"], ". But we can also directly look at the prime decomposition of ", Cell[BoxData[ \(TraditionalForm\`p\)]], ". We can have at most 2 prime factors, and the exponents cannot be too \ large. It's slightly easier to just deal with the list of all factors \ produced by ", StyleBox["Divisors[]", "Input"], "." }], "Text"], Cell[BoxData[ \(solvable[x_] := Length[Divisors[x]] \[LessEqual] 4; \)], "Input"], Cell[BoxData[{ \(solvable /@ toprod[100]\), "\n", \(\(Length[tosum[#]] &\) /@ toprod[100]\)}], "Input"], Cell[TextData[{ "True corresponds to a count of 1, and they all match up. \n\nSince S can \ trivially find all additive decompositions of ", Cell[BoxData[ \(TraditionalForm\`s\)]], ", she can only make her first call after checking that for all such \ decompositions, the corresponding ", Cell[BoxData[ \(TraditionalForm\`p\)]], " values are not solvable. We write a function to check whether ", Cell[BoxData[ \(TraditionalForm\`s\)]], " is bad in this sense and compute the set ", StyleBox["bads", "Input"], " of all bad sum values ", Cell[BoxData[ \(TraditionalForm\`s\)]], ". " }], "Text"], Cell[BoxData[ \(badsum[s_] := \(! Or @@ \(solvable /@ toprod[s]\)\); \)], "Input"], Cell["\<\ bads = Select[ Range[4,196], badsum ] bads // Length\ \>", "Input"], Cell["Let's check one of those numbers:", "Text"], Cell["\<\ toprod[123] solvable /@ %\ \>", "Input"], Cell[TextData[{ "Works fine. \n\nHence, after the first call by S, P now knows in addition \ that ", Cell[BoxData[ \(TraditionalForm\`s\)]], " has to be one of these 53 values. Since P can figure out which one it is, \ ", Cell[BoxData[ \(TraditionalForm\`p\)]], " must have the special property that it occurs exactly once in all the \ products associated with ", Cell[BoxData[ \(TraditionalForm\`s\ \[Element] \ bads\)]], ". We can compute the set ", StyleBox["goodb", "Input"], " of all such product values. " }], "Text"], Cell[BoxData[{ \(prods = Flatten[toprod /@ bads]; \), "\n", \(goodp = Select[prods, Count[prods, #1] \[Equal] 1 &]; \), "\n", \(Length[goodp]\)}], "Input"], Cell[TextData[{ "Thus, ", Cell[BoxData[ \(TraditionalForm\`p\)]], " must be one of these 1106 values. \n\nLet's just check one of them:" }], "Text"], Cell["goodp[[500]]", "Input"], Cell["tosum[%]", "Input"], Cell["Intersection[%,bads]", "Input"], Cell[TextData[{ "When P calls S to tell her that he has determined ", Cell[BoxData[ \(TraditionalForm\`x\)]], " and ", Cell[BoxData[ \(TraditionalForm\`y\)]], ", S gains the additional information that ", Cell[BoxData[ \(TraditionalForm\`p\ \[Element] \ goodp\)]], ". In order to pin down ", Cell[BoxData[ \(TraditionalForm\`p\)]], ", S can now check how many such ", Cell[BoxData[ \(TraditionalForm\`p\)]], " are associated with exactly one ", Cell[BoxData[ \(TraditionalForm\`s\ \[Element] \ bads\)]], ". " }], "Text"], Cell["\<\ Length[Intersection[goodp,toprod[#]]]& /@ bads Count[%,1]\ \>", "Input"], Cell[TextData[{ "There is precisely one, namely the second, so S can also figure out ", Cell[BoxData[ \(TraditionalForm\`x\)]], " and ", Cell[BoxData[ \(TraditionalForm\`y\)]], ":" }], "Text"], Cell["\<\ bads[[2]] toprod[%] Intersection[goodp,%]\ \>", "Input"], Cell[TextData[{ "Hence, ", Cell[BoxData[ \(TraditionalForm\`s\ = \ 17\)]], " and ", Cell[BoxData[ \(TraditionalForm\`p\ = \ 52\)]], ", and " }], "Text"], Cell[BoxData[ \(Solve[{x + y \[Equal] 17, x\ y \[Equal] 52}, {x, y}]\)], "Input"], Cell[TextData[{ "and so ", Cell[BoxData[ \(TraditionalForm\`x\ = \ 4\)]], " and ", Cell[BoxData[ \(TraditionalForm\`y\ = \ 13\)]], ".\n\nOK, the last computation should have been done by hand. " }], "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["On Badgers", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:19"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", CellTags->"c:20"], Cell["\<\ Lewis Carroll has produced any number of (slightly bizarre) logic \ puzzles. Here is one. 1. Animals are always mortally offended if I fail to notice them. 2. The only animals that belong to me are in that field. 3. No animal can guess a conundrum, unless it has been properly trained in a \ Board-School. 4. None of the animals in that field are badgers. 5. When an animal is mortally offended, it always rushes about wildly and \ howls. 6. I never notice any animal, unless it belongs to me. 7. No animal, that has been properly trained in a Board-School, rushes about \ wildly and howls. This is complete nonsense semantically, but there is a logical structure: a \ collection of atomic facts such as \"an animal is noticed\" and \"an animal \ is mortally offended\" are connected.\ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:21"], Cell[TextData[{ "(a) Translate these assertions into formulae in propositional logic. To \ preserve the sanity of the graders, use the following variables with intended \ meaning as indicated in the table. \n\n\t", Cell[BoxData[ \(TraditionalForm\`n\)]], "\tnotice an animal\n\t", Cell[BoxData[ \(TraditionalForm\`m\)]], " \tis mine\n\t", Cell[BoxData[ \(TraditionalForm\`f\)]], "\tin the field\n\t", Cell[BoxData[ \(TraditionalForm\`b\)]], "\ta badger\n\t", Cell[BoxData[ \(TraditionalForm\`o\)]], "\toffended\n\t", Cell[BoxData[ \(TraditionalForm\`r\)]], "\trushes about\n\t", Cell[BoxData[ \(TraditionalForm\`s\)]], "\ttrained at school\n\t", Cell[BoxData[ \(TraditionalForm\`c\)]], "\tcan guess a conundrum\n\n(b) Determine what conclusions about badgers \ can be drawn from Carroll's assertions. \nExplain why your reasoning is \ correct. " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, FontFamily->"Times", FontSize->18, CellTags->"c:22"], Cell[TextData[{ "Here is the direct assault. \n\nSince Carrol only notices animals that \ belong to him, and all those are in the field, which contains no badgers, \ Carrol never notices a badger. Hence, badgers are mortally offended and rush \ about wildly and howl. Therefore, badgers have not been properly trained in a \ Board-School. Lastly, the can not can guess a conundrum. \n\nWe have three \ chains of implications:\n\n\t", Cell[BoxData[ \(TraditionalForm\`n\ \[Rule] \ \(m\ \[Rule] \ \(f\ \[Rule] \ \[Not] \ \ b\)\)\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`\[Not] n\ \[Rule] \ \(o\ \[Rule] r\)\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`c\ \[Rule] \ \(s\ \[Rule] \ \[Not] r\)\)]], "\n\nSince we are interested in badgers, we get ", Cell[BoxData[ \(TraditionalForm\`\[Not] f\)]], ", ", Cell[BoxData[ \(TraditionalForm\`\[Not] m\)]], ", ", Cell[BoxData[ \(TraditionalForm\`\[Not] n\)]], " from the first chain using modus tollens.\nFrom the second we get ", Cell[BoxData[ \(TraditionalForm\`o\)]], " and ", Cell[BoxData[ \(TraditionalForm\`r\)]], " by modus ponens, and thus from the third ", Cell[BoxData[ \(TraditionalForm\`\[Not] s\)]], " and ", Cell[BoxData[ \(TraditionalForm\`\[Not] c\)]], ", again by modus tollens. " }], "Text"], Cell[TextData[{ "\t\nLastly, we can write down a ", StyleBox["Mathematica", FontSlant->"Italic"], " formula that summarizes the given data (using the same propositional \ variables as above). " }], "Text"], Cell["\<\ fml = And[ \tImplies[ Not[n], o ], \tImplies[ m, f ], \tImplies[ c, s ], \tImplies[ f, Not[b] ], \tImplies[ o, r ], \tImplies[ n, m ], \tImplies[ s, Not[r] ] ]\ \>", "Input"], Cell[TextData[{ "\nIf we expand this formula into DNF, all conjuncts contain a literal ", Cell[BoxData[ \(TraditionalForm\`\(! b\)\)]], " (meaning we are not talking about badgers), except one. " }], "Text"], Cell["fml // LogicalExpand", "Input"], Cell[TextData[{ "We can extract that one conjunct by setting ", Cell[BoxData[ \(TraditionalForm\`b\)]], " to True. " }], "Text"], Cell["% /. b->True", "Input"], Cell["\<\ These are precisely the conclusions from above: offended, rushes \ about, can't guess a conundrum, and so on. \ \>", "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Equivalent Formulae", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:23"], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:24"], Cell[TextData[{ "Which of the following 5 formulae are equivalent? \n\n(a) ", Cell[BoxData[ \(TraditionalForm\`\((\ q\ \[Rule] \ \((r \[Or] s)\))\)\ \[And] \ \((\((q \[And] r)\)\ \[Rule] \ s)\)\)]], "\n(b) ", Cell[BoxData[ \(TraditionalForm\`\((\((p \[Or] r)\) \[Or] \ \((s \[Rule] p)\))\)\ \[And] \ \((p\ \[Rule] \ \((s \[Rule] r)\))\)\)]], "\n(c) ", Cell[BoxData[ \(TraditionalForm\`q\ \[Rule] s\)]], "\n(d) ", Cell[BoxData[ \(TraditionalForm\`\((s \[Rule] \((q \[Or] r)\))\)\ \[And] \ \((\((q \[And] s)\)\ \[Rule] r)\)\)]], "\n(e) ", Cell[BoxData[ \(TraditionalForm\`\((\((p \[Or] s)\) \[Or] \((q \[Rule] p)\))\)\ \[And] \ \((p \[Rule] \((q \[Rule] s)\))\)\)]], "\n\nYou can tackle this problem by hand, or by computer. " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", CellTags->"c:25"], Cell[TextData[{ "The easiest formula is (c): ", Cell[BoxData[ \(TraditionalForm\`q\ \[Rule] s\)]], ". \n\nIt is equivalent to (a): ", Cell[BoxData[ \(TraditionalForm\`\((\ q\ \[Rule] \ \((r \[Or] s)\))\)\ \[And] \ \((\((q \[And] r)\)\ \[Rule] \ s)\)\)]], "\nTo see this, note that both formulae are true whenever ", Cell[BoxData[ \(TraditionalForm\`q\)]], " is false (ex falsum quodlibet). \nBut when ", Cell[BoxData[ \(TraditionalForm\`q\)]], " is true, the first formula simplifies to ", Cell[BoxData[ \(TraditionalForm\`s\)]], " , and the second ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\((r \[Or] s)\)\ \[And] \ \((r \[Rule] \ s)\)\)\)\)]], " which again simplifies to ", Cell[BoxData[ \(TraditionalForm\`s\)]], ". \n\nCheck:" }], "Text"], Cell["\<\ Clear[p,q,r,s] LogicalExpand[ Implies[q,s] ] LogicalExpand[ Implies[q,r||s] && Implies[q&&r,s] ]\ \>", "Input"], Cell[TextData[{ "Formula (d) looks somewhat similar to (a), but we can use ", StyleBox["LogicalExpand", "Input"], " to check that it is in fact not equivalent to (c). " }], "Text"], Cell["LogicalExpand[ Implies[s,q||r] && Implies[q&&s,r] ]", "Input"], Cell["Let's try (b) :", "Text"], Cell["\<\ LogicalExpand[ (p||r||Implies[s,p]) && Implies[p,Implies[s,r]] \ ]\ \>", "Input"], Cell["\<\ It's equivalent to (d) . Lastly (e):\ \>", "Text"], Cell["\<\ LogicalExpand[ (p||s||Implies[q,p]) && Implies[p,Implies[q,s]] \ ]\ \>", "Input"], Cell["\<\ So, we have the following equivalences: \t(a), (c), (e) and (b), (d) \t\ \>", "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Red & White Hats", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:26"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", CellTags->"c:27"], Cell["\<\ Another logic puzzle. A prison warden is bored, and decides to amuse himself with a little game. He \ blindfolds three prisoners A, B and C, and places hats on their heads. He \ selects the hats from a supply of three white and two red hats. He hides the \ remaining two hats. He then explains to the prisoners what he has done, and \ that he is about to remove the blindfolds from A and B, but they are not \ allowed to peek at their own hats. C will remain blindfolded. After removal \ of the blindfolds, he tells the prisoners this: \"If you can tell me the color of your hat, you will be released from prison. \ To discourage guessing, a wrong answer will cost you your head. If you \ prefer, you can ask to be lead back to your cell.\" The following happens: 1) A says that he is unable to ascertain the color of his hat, and goes back \ to his cell. 2) Then B says that he too is unable to ascertain the color of his hat, and \ goes back to his cell. 3) But now C claims to know the color of his hat. C tells the warden, and gains his freedom.\ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:28"], Cell["\<\ Determine the color of C's hat, and explain his reasoning. Remember, a wrong guess leads straight to the Guillotine. \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", CellTags->"c:29"], Cell["\<\ First note that A cannot have seen two red hats (otherwise he would \ have known for sure that his was white). So A has to quit. By the same token, B did not see two red hats. But B also knows that his own \ or C's hat is white. If C had the red hat, B could conclude that his own is \ white. Therefore, C must be wearing a white hat, and B cannot tell whether \ his own is red or white. Thus C can determine his own hat color to be white, once B has quit. \ \>", \ "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Flipping Pebbles", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:30"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:31"], Cell["\<\ Consider a set of configurations of a system, and a collection of \ legitimate operations in the system. An important problem is to show that \ certain configurations can (or cannot) be reached from a given initial \ configuration using only legitimate operations. For example, one might be \ interested in showing that after bootup, an operating system can never enter \ a forbidden state, given any sequence of legitimate state change operations. Here is a much simpler, concrete example. Our little toy system consists of \ 7 pebbles or tokens, each white on one side, and black on the other. In the \ picture below, there is one token in each region (not the external region). \ Initially, all tokens show white. The only allowed operations are: \t\[Bullet] flip all tokens within one region, \t\[Bullet] reset all tokens in one region to white. \t\ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:32"], Cell["\<\ (a) Show that one cannot reach the configuration where all tokens \ are black except for the center one. (b) Hard: Determine how many configurations can be reached. \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Hint", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:33"], Cell["\<\ It may help to label the pebbles a, b, c, bc, ac, ab, abc: the \ operations then work on all pebbles whose name contains a certain letter. \ \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:34"], Cell[TextData[{ "\nCall the three sets A, B and C. We can index the 7 points with numbers \ 1 through 7 where the bit-pattern (padded to three binary digits) of the \ index indicates membership. E.g., P(5) lies in A and C, but not in B since \ ", Cell[BoxData[ \(TraditionalForm\`5\ \[Congruent] \ 101\)]], ", P(7) lies in all three sets since ", Cell[BoxData[ \(TraditionalForm\`7\ \[Congruent] \ 111\)]], ". Hence, we can think of any configuration as a 7-tuple of bits:\n\t", Cell[BoxData[ \(TraditionalForm\`\((1, 1, 0, 1, 0, 0, 0, 1)\)\)]], " \nindicates that the 4 points lying in an odd number of sets are black, \ all others white. The starting configuration is \n\t", Cell[BoxData[ \(TraditionalForm\`\((1, 1, 1, 1, 1, 1, 1)\)\)]], " \nand the target configuration is \n\t", Cell[BoxData[ \(TraditionalForm\`\((1, 1, 1, 1, 1, 1, 0)\)\)]], " \n\n", StyleBox["Claim", FontWeight->"Bold"], ": The target configuration cannot be reached. \n\nLet's take a look at the \ operations we have to manipulate these patterns. There are 6: \n\n\t", Cell[BoxData[ \(TraditionalForm\`F(X)\)]], " meaning: flip tokens in ", Cell[BoxData[ \(TraditionalForm\`X\ \[Element] \ {A, B, C}\)]], " and \n\t", Cell[BoxData[ \(TraditionalForm\`B(X)\)]], " meaning: blacken tokens in ", Cell[BoxData[ \(TraditionalForm\`X\ \[Element] \ {A, B, C}\)]], ".\n\t\nNote the following laws concerning the effect of sequences of \ operations:\n\n\t1.\t", Cell[BoxData[ \(TraditionalForm\`\(B(X)\)\ \(B(Y)\)\ = \ \(B(Y)\)\ \(B(X)\)\)]], "\n\t2.\t", Cell[BoxData[ \(TraditionalForm\`\(B(X)\)\ \(B(X)\)\ = \ \ B(X)\)]], "\n\t3.\t", Cell[BoxData[ \(TraditionalForm\`\(F(X)\)\ \(F(Y)\)\ = \ \(F(Y)\)\ \(F(X)\)\)]], "\n\t4.\t", Cell[BoxData[ \(TraditionalForm\`\(F(X)\)\ \(F(X)\)\ = \ I\)]], " (identity, no effect)\n\t\nFor the sake of a contradiction, assume that \ there is a sequence of operations that takes us from ", Cell[BoxData[ \(TraditionalForm\`\((1, 1, 1, 1, 1, 1, 1)\)\)]], " to ", Cell[BoxData[ \(TraditionalForm\`\((1, 1, 1, 1, 1, 1, 0)\)\)]], ". \nWe may assume that the sequence of operations begins with ", Cell[BoxData[ \(TraditionalForm\`B(A)\)]], ": since originally all pebbles are black, this makes no difference at all. \ \nNow consider the last blackening operation in the sequence. By symmetry, we \ may assume that it operates on set ", Cell[BoxData[ \(TraditionalForm\`A\)]], ". By laws 3 and 4 the operations following ", Cell[BoxData[ \(TraditionalForm\`B\)]], " can only be\n\t", Cell[BoxData[ \(TraditionalForm\`\[Ellipsis]\ \(B(A)\)\ \(F(X)\)\)]], " or \n\t", Cell[BoxData[ \(TraditionalForm\`\[Ellipsis]\ \(B(A)\)\ \(F(A)\)\ \(F(B)\)\ \(F( C)\)\)]], ".\nTo see this, note that ", Cell[BoxData[ \(TraditionalForm\`P(7)\)]], " is white in the end, but was black after ", Cell[BoxData[ \(TraditionalForm\`B(A)\)]], ", so there had to be an odd number of flip operations after ", Cell[BoxData[ \(TraditionalForm\`B(A)\)]], ". By symmetry, we need not consider any other cases. \nBut in case 1, the \ token in ", Cell[BoxData[ \(TraditionalForm\`X\ \[Intersection] \ A\)]], " other than ", Cell[BoxData[ \(TraditionalForm\`P(7)\)]], " is white in the end. \nIn case 2, the token in ", Cell[BoxData[ \(TraditionalForm\`A\ - \ B\ - \ C\)]], " is white in the end. \nIn either case, we have a contradiction. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell[TextData[{ "A much harder question is exactly which patterns are obtainable, and which \ are unreachable. For example, one can show that the bit-wise complement of \ any reachable pattern is also reachable. There are 16 unreachable patterns:\n\ \n\t\t", Cell[BoxData[ TagBox[GridBox[{ {"0", "0", "0", "0", "0", "0", "1"}, {"0", "0", "0", "1", "1", "1", "0"}, {"0", "0", "1", "0", "1", "1", "1"}, {"0", "0", "1", "1", "0", "0", "0"}, {"0", "1", "0", "0", "1", "0", "0"}, {"0", "1", "0", "1", "0", "1", "1"}, {"0", "1", "1", "0", "0", "1", "0"}, {"0", "1", "1", "1", "1", "0", "1"}, {"1", "0", "0", "0", "0", "1", "0"}, {"1", "0", "0", "1", "1", "0", "1"}, {"1", "0", "1", "0", "1", "0", "0"}, {"1", "0", "1", "1", "0", "1", "1"}, {"1", "1", "0", "0", "1", "1", "1"}, {"1", "1", "0", "1", "0", "0", "0"}, {"1", "1", "1", "0", "0", "0", "1"}, {"1", "1", "1", "1", "1", "1", "0"} }, RowSpacings->1, ColumnSpacings->1, RowAlignments->Baseline, ColumnAlignments->{Left}], (TableForm[ #, TableSpacing -> {1, 1}]&)]]], "\n\nThe last one is our target pattern.\n\t\t" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:35"], Cell[BoxData[{ \(pat = Thread[IntegerDigits[Range[7], 2, 3]]; \), "\n", \(TableForm[pat]\)}], "Input"], Cell[BoxData[{ \(\(flip[i_]\)[L_List] := Mod[L + pat\[LeftDoubleBracket]i\[RightDoubleBracket], 2]; \), "\n", \(\(set[i_]\)[L_List] := Max /@ Pairs[L, pat\[LeftDoubleBracket]i\[RightDoubleBracket]]; \)}], "Input"], Cell[BoxData[ \(\(flip[3]\)[Table[1, {7}]]\)], "Input"], Cell[BoxData[ \(\(set[1]\)[Table[0, {7}]]\)], "Input"], Cell[BoxData[{ \(ClearAll[dot]\), "\n", \(dot[L_List, "\"] := \(flip[1]\)[L]; \), "\n", \(dot[L_List, "\"] := \(flip[2]\)[L]; \), "\n", \(dot[L_List, "\"] := \(flip[3]\)[L]; \), "\n", \(dot[L_List, "\"] := \(set[1]\)[L]; \), "\n", \(dot[L_List, "\"] := \(set[2]\)[L]; \), "\n", \(dot[L_List, "\"] := \(set[3]\)[L]; \)}], "Input"], Cell[BoxData[ \(K = {"\", "\", "\", "\", "\", "\"}; \)], "Input"], Cell[BoxData[ \(reach = GenerateCSM[Table[1, {7}], dot, K]; \)], "Input"], Cell[BoxData[ \(Length[reach]\)], "Input"], Cell[BoxData[ \(\(all = Tuples[2, 7] - 1;\)\)], "Input"], Cell[BoxData[{ \(nreach = Complement[all, reach]; \), "\n", \(Length[nreach]\), "\n", \(TableForm[nreach]\)}], "Input"], Cell["Reorder columns: singletons, pairs, triple. ", "Text"], Cell[BoxData[ \(V = {a, b, a\ b, c, c\ a, c\ b, a\ b\ c}\)], "Input"], Cell[BoxData[ \(mix = {1, 2, 4, 6, 5, 3, 7}\)], "Input"], Cell[BoxData[ \(V\[LeftDoubleBracket]mix\[RightDoubleBracket]\)], "Input"], Cell[BoxData[ \(TableForm[ Sort[\((#1\[LeftDoubleBracket]mix\[RightDoubleBracket] &)\) /@ nreach]]\)], "Input"], Cell["Get conditions for non-reachability. ", "Text"], Cell[BoxData[ \(equiv[x_, y_] := Implies[x, y] && Implies[y, x]; \)], "Input"], Cell[BoxData[ \(nr1 = a \[Xor] b \[Xor] c \[Xor] abc\)], "Input"], Cell[BoxData[ \(nr2 = equiv[a, bc] && equiv[b, ac] && equiv[c, ab] || equiv[\(! a\), bc] && equiv[\(! b\), ac] && equiv[\(! c\), ab]\)], "Input"], Cell[BoxData[ \(nr = LogicalExpand[nr1 && nr2]\)], "Input"], Cell[BoxData[{ \(Length[nr]\), "\n", \(Length /@ nr\)}], "Input"], Cell[BoxData[ \(rr = LogicalExpand[\(! \((nr1 && nr2)\)\)]\)], "Input"], Cell[BoxData[ \(TableForm[rr /. \[InvisibleSpace]Or \[Rule] List]\)], "Input"], Cell[BoxData[{ \(Length[rr]\), "\n", \(Length /@ rr\)}], "Input"], Cell[TextData[{ "In other words: ", StyleBox["not", FontWeight->"Bold"], " reachable is equivalent with \n\n\t\tContains an odd number of a, b, c \ and abc, and\n\t\ta, b, c are all the same as bc, ac, ab or all the \ opposite.\n\t\t\nIt is not hard to see that this is an invariant. " }], "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Flipping Tokens", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:36"], Cell[CellGroupData[{ Cell["Code -- Don't Look, but Execute First", "Subsubsection", CellTags->"c:37"], Cell[BoxData[{ \(Clear[toDisk, colorMatrix, drawMatrix, ls, rs, ds, us, flipTokens, flipPositions]\), "\n", \(\(toDisk[col_List, dx_, dy_, rr_]\)[ c_, {x_, y_}] := {col\[LeftDoubleBracket]c + 1\[RightDoubleBracket], Disk[{x + dx, y + dy}, rr]}; \), "\n", \(colorMatrix[M_?MatrixQ] := Graphics[MapIndexed[ toDisk[{Blue, Red, Green}, \(- .5\), \(- .5\), .3], Reverse /@ Transpose[M], {2}]]; \), "\n", \(drawMatrix[M_?MatrixQ] := Module[{n, m}, {n, m} = Dimensions[M]; Show[{colorMatrix[M], GridLine[n + 1, m + 1, GridOffset \[Rule] {1, 1}, PlotStyle \[Rule] {GrayLevel[ .5], 0.01}]}, AspectRatio \[Rule] n\/m, Background \[Rule] Yellow]]; \), "\n", \(drawMatrix[L_List] := drawMatrix[{L}]; \), "\n", \(ls[M_?MatrixQ] := \((Append[Rest[#1], 0] &)\) /@ M; \), "\n", \(rs[M_?MatrixQ] := \((Prepend[Drop[#1, \(-1\)], 0] &)\) /@ M; \), "\n", \(ds[M_?MatrixQ] := Prepend[Drop[M, \(-1\)], Table[0, {Length[First[M]]}]]; \), "\n", \(us[M_?MatrixQ] := Append[Rest[M], Table[0, {Length[First[M]]}]]; \), "\n", \(flipTokens[M_?MatrixQ] := Mod[Through[\((\(#1 &\) + ls + us + ds + rs)\)[M]], 2]; \), "\n", \(flipTokens[L_List] := flipTokens[{L}]; \), "\n", \(flipPositions[L_List, n_Integer] := \((Count[L, #1] &)\) /@ Range[n]; \), "\n", \(flipPositions[L_List, n_Integer, m_Integer] := Table[Count[L, {i, j}], {i, n}, {j, m}]; \)}], "Input"] }, Closed]], Cell[CellGroupData[{ Cell["Background", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:38"], Cell[TextData[{ "An interesting class of problems deals with the question whether a certain \ system can ever reach a certain state, given a collection of possible \ transitions the system can make. \n\nAs an example, consider a collection of \ tokens, blue on one side, and red on the other. Suppose we have 5 tokens \ aligned on a straight line. Originally all tokens are blue side up (the \ original state of the system). The admissible transitions are described as \ follows: \n\n\t\[Bullet] Pick an arbitrary token, and flip it over; also, \ flip over its two neighbors. \n\nCan the system reach the all-red state? \n\n\ Here are some little function that helps to check the result of flipping \ tokens. \nThe first, ", StyleBox["flipPositions", "Input"], ", takes as input a list of chosen positions, and returns as output a list \ that indicates where and how often to flip a token. Note that we also have to \ provide the number of tokens as input. \n\nThe next function, ", StyleBox["flipTokens", "Input"], ", determines the result of flipping the tokens. It returns the token \ sequence as a binary list: 0 represents Blue, and 1 represents Red. The last \ function, ", StyleBox["drawMatrix", "Input"], ", is entirely frivolous, and just draws a beautiful picture. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell["\<\ flipPositions[ {1,2,3,1}, 5 ] % // flipTokens % // drawMatrix;\ \>", "Input"], Cell["\<\ In other words, flipping tokens 1, 2, 3 and 1 won't get us to \ all-red. But, flipping 2 and 5 will:\ \>", "Text"], Cell["\<\ flipPositions[ {2,5}, 5 ] % // flipTokens % // drawMatrix;\ \>", "Input"], Cell["For six tokens we can also flip 2 and 5. ", "Text"], Cell["\<\ flipPositions[ {2,5}, 6 ] % // flipTokens % // drawMatrix;\ \>", "Input"], Cell[TextData[{ "Figure out how to handle 7 tokens, and you will see that one can prove by \ induction on ", Cell[BoxData[ \(TraditionalForm\`n\)]], " that any linear arrangements of tokens can always be brought into the \ all-red state. " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:39"], Cell[TextData[{ "Consider all 2 by ", Cell[BoxData[ \(TraditionalForm\`n\)]], " grids of tokens.\n\n(a) Show that order of the flip operations does not \ matter. \n\n(b) Show that flipping the same token twice undoes the first \ flip, and so two flips have no effect.\n\n(c) Show that all 2 by ", Cell[BoxData[ \(TraditionalForm\`n\)]], " grids of tokens can reach the the all-red state by flipping tokens and \ their neighbors, starting from all-blue. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell["Hint", "Subsubsection", CellTags->"c:40"], Cell["\<\ Note that once we decide what to do with the tokens in the first \ column, everything else is fixed. Here is one example of a failed attempt for 2 by 4:\ \>", "Text", Evaluatable->False, AspectRatioFixed->True], Cell["\<\ flipPositions[ {{1,1},{2,4}}, 2, 4 ] % // flipTokens // drawMatrix;\ \>", "Input"] }, Closed]], Cell[CellGroupData[{ Cell["Comment", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:41"], Cell[TextData[{ "One can prove much more: all ", Cell[BoxData[ \(TraditionalForm\`n\)]], " by ", Cell[BoxData[ \(TraditionalForm\`m\)]], " grids of tokens can reach the all-red state. We could even wrap the \ grids around to make a cylinder or torus, or consider a higher dimensional \ version. In fact, we can assume any neighborhood relationship between the \ tokens whatsoever. But, the proof requires algebra for the general case. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, FontFamily->"Times", FontSize->18, CellTags->"c:42"], Cell[CellGroupData[{ Cell["Part a", "Subsubsection", CellTags->"c:43"], Cell[TextData[{ "For each token ", Cell[BoxData[ \(TraditionalForm\`t\)]], ", let ", Cell[BoxData[ \(TraditionalForm\`c(\ t, L\ )\)]], " be the count of all flips performed on that token if we perform a \ sequence ", Cell[BoxData[ \(TraditionalForm\`L\)]], " of flips (either because the token itself or one of its neighbors was \ chosen). \nMore precisely, ", Cell[BoxData[ \(TraditionalForm\`c(\ t, \(()\)\ )\ = \ 0\)]], " for all tokens. \nAnd ", Cell[BoxData[ \(TraditionalForm\`c(\ \ t, \ L\ s\ )\ = c(\ t, L\ )\)]], " if ", Cell[BoxData[ \(TraditionalForm\`t\)]], " is neither equal to ", Cell[BoxData[ \(TraditionalForm\`s\)]], " nor one of its neighbors. \nOtherwise, ", Cell[BoxData[ \(TraditionalForm\`c(\ \ t, \ L\ s\ )\ = c(\ t, L\ )\)]], " + 1.\nBut then ", Cell[BoxData[ \(TraditionalForm\`c(\ t, \ L\ \(s\_1\) s\_\(\(\ \)\(2\)\)\ K\ )\ = \ c(\ t, \ L\ s\_2\ s\_1\ K)\)]], ". \nHence we can rearrange the list of flips any which way we like. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell["Part b", "Subsubsection", CellTags->"c:44"], Cell[TextData[{ "Consider again ", Cell[BoxData[ \(TraditionalForm\`c(\ t, L\ )\)]], " from part (a). Clearly, token ", Cell[BoxData[ \(TraditionalForm\`t\)]], " is red in the end iff ", Cell[BoxData[ \(TraditionalForm\`c(\ t, L\ )\)]], " is odd. Hence, we can delete any double occurence of a token from ", Cell[BoxData[ \(TraditionalForm\`L\)]], ". \n\nTogether with part (a), this means that we really have to select a \ ", StyleBox["set", FontColor->RGBColor[0, 0, 1]], " of tokens, rather than a ", StyleBox["sequence", FontColor->RGBColor[0, 0, 1]], ". Hence, we can apply brute force search to each given grid: there are \ only finitely many subsets (whereas the number of sequences is infinite). In \ reality, this does not help much, there are ", Cell[BoxData[ \(TraditionalForm\`2\^\(\(\ \)\(2\ n\)\)\)]], " sets to consider. " }], "Text", Evaluatable->False, AspectRatioFixed->True] }, Closed]], Cell[CellGroupData[{ Cell["Part c", "Subsubsection", CellTags->"c:45"], Cell[TextData[{ "Now the painful part: every 2 by ", Cell[BoxData[ \(TraditionalForm\`n\)]], " grid can reach all-red.\n\nAs indicated in the hint, the selection of \ tokens in the first column determines all other choices. More precisely, \ suppose ", Cell[BoxData[ \(TraditionalForm\`L\)]], " is choice of tokens that produces all-red. Here we think of ", Cell[BoxData[ \(TraditionalForm\`L\)]], " as a subset of the set of all positions ", Cell[BoxData[ \(TraditionalForm\`{\ \ {i, j}\ | \ \ i\ = 1, 2, \ \ 1\ \[LessEqual] \ j \[LessEqual] n\ }\)]], ". Then ", Cell[BoxData[ \(TraditionalForm\`L\)]], " is completely determined by ", Cell[BoxData[ \(TraditionalForm\`L\ \[Intersection] \ {\ {1, 1}, {2, 1}\ }\)]], ". \n\nSuppose we don't use any token in the first column, ", Cell[BoxData[ \(TraditionalForm\`L\ \[Intersection] \ {\ {1, 1}, {2, 1}\ }\ = \ \[EmptySet]\)]], ". Then we must have ", Cell[BoxData[ \(TraditionalForm\`{1, 2}, {2, 2}\ \[Element] \ L\)]], ", for otherwise the first two tokens would not be red in the end: no \ token ", Cell[BoxData[ \(TraditionalForm\`{i, j}, \ j\ > 2\)]], ", can influence the first two. By the same argument we must have ", Cell[BoxData[ \(TraditionalForm\`{1, 3, {2, 3}\ \[Element] \ L\)]], ", ", Cell[BoxData[ \(TraditionalForm\`{1, 4}, {2, 4}\ \[NotElement] \ L\)]], ", and so on. Here is the pattern:" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell["\<\ pos = flipPositions[ \ {{1,2},{2,2},{1,3},{2,3},{1,6},{2,6},{1,7},{2,7}}, 2, 8 ]; pos // drawMatrix; tok = flipTokens[pos]; tok // drawMatrix;\ \>", "Input"], Cell[TextData[{ "We can deal with all cases ", Cell[BoxData[ \(TraditionalForm\`n\ = \ 4\ m\)]], " in this way. \nFor ", Cell[BoxData[ \(TraditionalForm\`n\ = \ 4 m\ + \ 2\)]], " we use the same pattern, but shifted by one column. " }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell["\<\ pos = flipPositions[ \ {{1,1},{2,1},{1,2},{2,2},{1,5},{2,5},{1,6},{2,6}}, 2, 6 ]; pos // drawMatrix; tok = flipTokens[pos]; tok // drawMatrix;\ \>", "Input"], Cell[TextData[{ "And for odd ", Cell[BoxData[ \(TraditionalForm\`n\)]], " we start with a singly token in the first column:" }], "Text", Evaluatable->False, AspectRatioFixed->True], Cell["\<\ pos = flipPositions[ {{1,1},{2,3},{1,5},{2,7}}, 2, 7 ]; pos // drawMatrix; tok = flipTokens[pos]; tok // drawMatrix;\ \>", "Input"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Flipping/Removing Tokens", "Section", Evaluatable->False, PageBreakAbove->True, AspectRatioFixed->True, CellTags->"c:46"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", CellTags->"c:47"], Cell[TextData[{ "An interesting class of problems deals with the question whether a certain \ system can ever reach a certain state, given a collection of possible \ transitions the system can make. \nHere is an example. \n\nConsider a \ collection of tokens, blue on one side, and red on the other. Suppose we have \ ", Cell[BoxData[ \(TraditionalForm\`n\)]], " tokens aligned on a straight line. Originally all tokens are randomly \ blue or red side up (the original state of the system). The admissible \ transitions are described as follows: \n\n\t\[Bullet] Pick an arbitrary blue \ token, and remove it; also, flip over its neighbors, if any. \n\nTokens \ separated by a gap are not considered adjacent, so \"flip the neighbors\" is \ a conditional operation. \n" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:48"], Cell["\<\ Characterize all initial states for which one can remove all the \ tokens. \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", FontColor->RGBColor[0, 0, 1], CellTags->"c:49"], Cell[CellGroupData[{ Cell["Experiments", "Subsubsection", CellTags->"c:50"], Cell[TextData[{ "Here is a computational approach: simulate the problem, run a few \ examples, form the right conjecture, and then prove the conjecture \ rigorously. \n\nTo keep the program simple, it is best to identify \n\tblue \ \t\[DoubleLongRightArrow] 1\n\tred \t\[DoubleLongRightArrow] -1\n\tgap \t\ \[DoubleLongRightArrow] 0\nso we are dealing with lists whose entries are ", Cell[BoxData[ \(TraditionalForm\`\(-1\), 0, 1\)]], ". Needless to say, initially there are only entries ", Cell[BoxData[ \(TraditionalForm\`\(-1\), \ 1\)]], ". \n\nNote that the choice of handle matters: \n\n\t", Cell[BoxData[ FormBox[ RowBox[{ RowBox[{"(", RowBox[{ StyleBox["1", FontColor->RGBColor[0, 0, 1]], ",", "1", ",", "1"}], ")"}], " ", "\[Rule]", " ", \(\((0, \(-1\), 1)\)\ \[Rule] \ \(\((0, 1, 0)\)\ \[Rule] \ \((0, 0, 0)\)\)\)}], TraditionalForm]]], "\nbut \n\t", Cell[BoxData[ FormBox[ RowBox[{ RowBox[{"(", RowBox[{"1", ",", StyleBox["1", FontColor->RGBColor[0, 0, 1]], ",", "1"}], ")"}], " ", "\[Rule]", " ", \((\(-1\), 0, \(-1\))\), " "}], TraditionalForm]]], "\n\ncomes to a grinding halt.\n\nHere is a collection of ", StyleBox["Mathematica", FontSlant->"Italic"], " rules that describe how such a list is processed if we always choose the \ leftmost handle (i.e., we operate on the first 1 or -1). The action function \ then applies these rules to a given list repeatedly. As it turns out, this is \ all we need for the problem at hand, otherwise we would have to implement a \ slightly more complicated procedure that keeps track of all possible \ replacements. \n\nHere is a collection of ", StyleBox["Mathematica", FontSlant->"Italic"], " rules that describe all possible operations on a list. Since there are up \ to ", Cell[BoxData[ \(TraditionalForm\`n\)]], " handles, we may get up to ", Cell[BoxData[ \(TraditionalForm\`n\)]], " many next lists in a single step (only the first step really, then only \ ", Cell[BoxData[ \(TraditionalForm\`n - 1\)]], ", ", Cell[BoxData[ \(TraditionalForm\`n - 2\)]], ", and so forth). " }], "Text"], Cell[BoxData[{ \(\(rules = {\[IndentingNewLine]{1, b_, yy___} \[RuleDelayed] {0, \(-b\), yy}, \[IndentingNewLine]{xx___, a_, 1, b_, yy___} \[RuleDelayed] {xx, \(-a\), 0, \(-b\), yy}, \[IndentingNewLine]{xx___, a_, 1} \[RuleDelayed] {xx, \(-a\), 0}\[IndentingNewLine]};\)\), "\n", \(\(move[L_List] := ReplaceList[L, rules];\)\)}], "Input"], Cell["A test:", "Text"], Cell["\<\ move[{1,1,1}] move[{-1,1,1,-1}]\ \>", "Input"], Cell[TextData[{ "Since we need to apply the move operation repeatedly, we have to be \ careful with lists of configurations as input. Using the pattern matcher in \ ", StyleBox["Mathematica", FontSlant->"Italic"], " this is fairly easy to do. Since we will use a fixed point operation in a \ minute, we make sure that lists without handles are returned as is. " }], "Text"], Cell[BoxData[{ \(ClearAll[move]\), "\n", \(\(move[{A__Integer}] := \[IndentingNewLine]\t ReplaceList[\ {A}, rules]\ \ /; \ Count[{A}, 1] > 0;\)\ \ \ \ \), "\n", \(\(move[{A__Integer}] := {{A}};\)\ \ \ \ \), "\n", \(move[{L__List}] := \ Union[\ Flatten[\ Map[\ move, \ {L}\ ], \ 1\ ]]\)}], "Input"], Cell["A little experiment. ", "Text"], Cell["\<\ move[{-1,1,-1,1,-1}] move[%] move[%] move[%] move[%]\ \>", "Input"], Cell["\<\ After 4 moves we are stuck with 1 or 2 red tokens. To avoid typing, we should use a fixed point operation. Note that since the \ actual fixed point is the empty list we have to back up a little. \ \>", \ "Text"], Cell[BoxData[ \(\(iterate[A_List]\ := \ FixedPoint[\ move, \ A\ ];\)\)], "Input"], Cell["This example won't work out:", "Text"], Cell[BoxData[ \(iterate[{\(-1\), 1, \(-1\), 1, \(-1\)}]\)], "Input"], Cell["But this one will:", "Text"], Cell["iterate[{1,-1,1,1,1,-1,-1,1,-1,-1,-1}]", "Input"], Cell["iterate[{1,1,1}]", "Input"], Cell["\<\ Since we are not really interested in all the failed attempts, we \ should just check whether the all-zeros lists appears. \ \>", "Text"], Cell[BoxData[ \(\(test[A_List]\ := \ MemberQ[\ iterate[A], \ Table[0, {Length[A]}]];\)\)], "Input"], Cell[BoxData[ \(test[{1, 1, 1}]\)], "Input"], Cell[BoxData[ \(test[{1, 1, 1, \(-1\), \(-1\), \(-1\), 1}]\)], "Input"], Cell["We can even automate the list production routine a bit. ", "Text"], Cell["\<\ L = Table[ 2 Random[Integer,{0,1}]-1, {10} ] test[L]\ \>", "Input"] }, Closed]], Cell[CellGroupData[{ Cell["Experiments", "Subsubsection", CellTags->"c:51"], Cell[TextData[{ "Now comes the hard part: we need a conjecture. Looking at random lists may \ or may not produce the crucial insight, so how about checking all lists of \ some length, say, ", Cell[BoxData[ \(TraditionalForm\`n = 7\)]], "?" }], "Text"], Cell[BoxData[{ \(\(L\ = \ Tuples[2, 7]\ /. \ 2 \[Rule] \(-1\);\)\), "\n", \(L\ // \ Length\), "\n", \(\(LL\ = \ Select[\ L, \ test\ ];\)\), "\n", \(LL\ // \ Length\)}], "Input"], Cell["\<\ Exactly half! This is probably no coincidence. Let's take a look \ at some of the lists, in graphical form. \ \>", "Text"], Cell[BoxData[ \(PlotMatrix[Thread[Take[LL, 32]] /. \[InvisibleSpace]{\(-1\) \[Rule] 5}, GridLines \[Rule] True]; \)], "Input"], Cell[TextData[{ "Highly regular. Note that the number of red tokens is always even. By \ looking at a few more values of ", Cell[BoxData[ \(TraditionalForm\`n\)]], ", one might be led to the observation that the number of blue tokens in \ the original list is crucial. More precisely, we seem to be able to remove \ all tokens if, and only if, the number of blue tokens is originally odd. \n\n\ So, here is our \n\n", StyleBox["Conjecture", FontColor->RGBColor[0, 0, 1]], ": \nAll tokens can be removed iff the number of blue tokens originally is \ odd. \n\nNote that the length of the list plays no role here. " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Proof", "Subsubsection", CellTags->"c:52"], Cell[TextData[{ "First assume the number of 1's is odd. \nThe claim is clearly true if the \ list has length 1. So suppose we have a list ", Cell[BoxData[ \(TraditionalForm\`L\)]], " of length ", Cell[BoxData[ \(TraditionalForm\`n > 1\)]], ". Consider the first 1 in ", Cell[BoxData[ \(TraditionalForm\`L\)]], ":\n\t", Cell[BoxData[ FormBox[ RowBox[{"L", " ", "=", " ", RowBox[{"(", RowBox[{\(-1\), ",", \(-1\), ",", "\[Ellipsis]", ",", " ", \(-1\), ",", " ", StyleBox["1", FontWeight->"Bold", FontColor->RGBColor[0, 0, 1]], ",", " ", "x", ",", "\[Ellipsis]"}], " ", ")"}]}], TraditionalForm]]], "\nBy removing it, we generate \n\t", Cell[BoxData[ FormBox[ RowBox[{"L", " ", "=", " ", RowBox[{"(", RowBox[{\(-1\), ",", "\[Ellipsis]", ",", " ", \(-1\), ",", "1", ",", StyleBox["0", FontWeight->"Bold", FontColor->RGBColor[0, 0, 1]], ",", " ", \(-x\), ",", "\[Ellipsis]"}], " ", ")"}]}], TraditionalForm]]], "\nBoth pieces before and after the 0 have an odd number of 1's, and we are \ done by IH. The case where there are no -1's before the first 1 is entirely \ similar. \n\nThe opposite direction is a little harder: we have to make sure \ that no replacement sequence can produce all 0's if we start with an even \ number of 1's. The argument is really quite similar: consider an arbitrary 1 \ somewhere in the list, and show that at least one of the two sublists \ generated by the replacement has again an even number of 1's. " }], "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Natural Deduction", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:53"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", CellTags->"c:54"], Cell["\<\ Use the natural deduction system shown in class (see book or \ lecture notes). Make sure to take a look at the examples in chapter 2 (there are more in \ chapter 7, and in the back of the book in the problem solutions section). \ \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:55"], Cell[TextData[{ "\na) Show that all the rules in Natural Deduction involving ", Cell[BoxData[ \(TraditionalForm\`\(\(\[And]\)\(\ \)\)\)]], " and \[Implies] are sound: \nwhenever the premises are true under some \ truth assignment, so are the conclusions. \n\nb) Give a derivation for ", Cell[BoxData[ \(TraditionalForm\`p\ \[Implies] \ \((\ q\ \[Implies] \ r)\), \ \ p\ \[Implies] \ q\ \ \[RightTee] \ \ p\ \[Implies] \ \(\(r\)\(.\)\)\)]], "\n\nc) Give a derivation for ", Cell[BoxData[ \(TraditionalForm\`p\ \[And] \ q\ \ \[RightTee] \ \ \[Not] \ \((\ \[Not] p\ \[Or] \ \[Not] \ q)\)\)]], "\n\nd) Give a derivation for ", Cell[BoxData[ \(TraditionalForm\`p\ \[Or] \ q\ \ \[RightTee] \ \ \[Not] \ \((\ \[Not] p\ \[And] \ \[Not] \ q)\)\)]], "\n\ne) Give a derivation for ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\[Not] \ p\ \[Or] \ q\ \ \[RightTee] \ \ p\ \[Implies] \ q\)\)\)]], "\n\nf) Give a derivation for ", Cell[BoxData[ \(TraditionalForm\`p \[Implies] \ q\ \ \[RightTee] \ \ \[Not] p\ \[Or] \ q\)]] }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Comments", "Subsubsection", CellTags->"c:56"], Cell[TextData[{ "The ", Cell[BoxData[ \(TraditionalForm\`p\)]], " and ", Cell[BoxData[ \(TraditionalForm\`q\)]], " here really stand for formulae, not just variables -- but it's too \ cumbersome to type all the ", Cell[BoxData[ \(TraditionalForm\`\[Phi]\)]], "'s and ", Cell[BoxData[ \(TraditionalForm\`\[Psi]\)]], "'s. \n\nFor the derivation, you can use that we have shown in class that \n\ \[Bullet] Law of the excluded middle: ", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\(\ \)\(\ \)\) \(\[Not] \ p\ \[Or] \ p\)\)\)]], "\n\[Bullet] Deduction Theorem: ", Cell[BoxData[ \(TraditionalForm\`\[CapitalGamma], \ p\ \[RightTee] \ q\)]], " if, and only if, ", Cell[BoxData[ \(TraditionalForm\`\[CapitalGamma]\ \[RightTee] \ \ \(\(p\)\(\[Implies]\)\(q\)\(\ \)\)\)]], "\n\nTo write down these formal proofs, follow the table format shown in \ class: \nfirst column: index, second column: formula, third column: \ justification.\nExample: \n\n", Cell[BoxData[ \(TraditionalForm\`p\ \[And] \ q, \ p\ \[Implies] \ \ r, \ \ q\ \[Implies] \ s\ \ \[RightTee] \ \ r\ \[And] \ s\)]], "\n\n", StyleBox["1\tp \[And] q\t\t\tprem\n2\tp ", FontColor->RGBColor[0, 0, 1]], "\[Implies]", StyleBox[" r\t\t\tprem\n3\tq ", FontColor->RGBColor[0, 0, 1]], "\[Implies]", StyleBox[" s \t\t\tprem\n", FontColor->RGBColor[0, 0, 1]], "4\tp\t\t\t\[And] e, 1\n5\tr\t\t\t\[Implies] e, 2, 4\n6\tq\t\t\t\[And] e, 1 \ \n7\ts\t\t\t\[Implies] e, 3, 6\n", StyleBox["8\tr \[And] s\t\t\t\[And] i, 5, 7", FontColor->RGBColor[0, 0, 1]] }], "Text"], Cell[TextData[{ "Don't worry about the colors. \n\nTo get special symbols such as \ \[Implies], \[And] or \[Or] one way is to start with the palette File \ \[Rule] Palettes \[Rule] CompleteCharacters. \nYou can just click on the \ symbol to insert it into your notebook. \n\n", StyleBox["NOTE", FontColor->RGBColor[1, 0, 0]], ": At the bottom of the palette window you will see keyboard shortcuts. \n\ \nFor example, to get an \[Implies] you only need to type \[EscapeKey]=>\ \[EscapeKey], for \[And] type \[EscapeKey]and\[EscapeKey], and so on. \n" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", CellTags->"c:57"], Cell[CellGroupData[{ Cell["Part a", "Subsubsection", CellTags->"c:58"], Cell[TextData[{ "This is brute force: assume the premises of a rule of inference are true \ (under some truth assignment) and show that the conclusion is also true \ (under the same assignment). \nIn the process we use the truth tables for the \ various functions ", Cell[BoxData[ \(TraditionalForm\`H\_not\)]], ", ", Cell[BoxData[ \(TraditionalForm\`H\_and\)]], ", ", Cell[BoxData[ \(TraditionalForm\`H\_or\)]], " and so on. \n\nWe'll just do two interesting cases:\n\n\[Or] elimination\n\ We have p \[Or] q, and from assumption p we can derive r, and from \ assumption q we can derive r. \nBy induction, these derivations preserve \ truth: if p is true, then so is r, and if q is true, then so is r. \nBut if p \ \[Or] q is true, at least one of p or q must be true (look at the table for \ ", Cell[BoxData[ \(TraditionalForm\`H\_or\)]], " ). \nHence r must be true. \n\nmodus tollens\nWe have p \[Implies] q, \ and \[Not] q. \nIf p were true, then q would also have to be true (look at \ the table for ", Cell[BoxData[ \(TraditionalForm\`H\_implies\)]], " ), contradicting the truth of \[Not] q. Hence p must be false, and \[Not] \ p must be true. \n" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part b", "Subsubsection", CellTags->"c:59"], Cell[TextData[{ Cell[BoxData[ FormBox[ RowBox[{" ", FormBox[\(p\ \[Implies] \ \((\ q\ \[Implies] \ r)\), \ \ p\ \[Implies] \ q\ \ \[RightTee] \ \ p\ \[Implies] \ r\), "TraditionalForm"]}], TraditionalForm]]], "\n\n1\tp \[Implies] (q \[Implies] r)\t\tprem\n2\tp \[Implies] q\t\t\tprem\n\ 3\tp\t\t\tassmp\n4\tq \[Implies] r\t\t\t\[Implies] e, 1, 3\n5\tq\t\t\t\ \[Implies] e, 2, 3\n6\tr\t\t\t\[Implies] e, 4, 5\n7\tp \[Implies] r\t\t\t\ \[Implies] i, 3 - 6\n" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part c", "Subsubsection", CellTags->"c:60"], Cell[TextData[{ Cell[BoxData[ \(TraditionalForm\`p\ \[And] \ q\ \ \[RightTee] \ \ \[Not] \ \((\ \[Not] p\ \[Or] \ \[Not] \ q)\)\)]], "\n\nThis is one half of de Morgan's law, but we have to give a proof in \ the system. \nThere are many ways to attack this problem, here is a rather \ overblown way that demonstrates how to use the deduction theorem (your \ solution was probably more direct). \nBy the deduction theorem our problem \ reduces to the following:\n\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(p\ \[And] \ q\ \ \[Implies] \ \ \[Not] \ \((\ \[Not] p\ \[Or] \ \[Not] \ q)\)\)\)]], "\n\nIn general, one can easily prove ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\ \)\) \(\[Phi]\ \[Implies] \ \[Psi]\ \ \[RightTee] \ \ \[Not] \ \[Psi]\ \[Implies] \ \[Not] \ \[Phi]\)\)]], ", \n(Proof: modus tollens, deduction theorem)\nso it suffices to show \n\ \n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[Not] \ \(\[Not] \ \((\ \ \[Not] p\ \[Or] \ \[Not] \ q)\)\)\ \[Implies] \ \[Not] \ \((p\ \[And] \ q)\)\)\)]], "\n\nor, by the deduction theorem and the double negation rules, \n\n\t", Cell[BoxData[ FormBox[ RowBox[{" ", StyleBox[\(\[Not] p\ \[Or] \ \[Not] \ q\ \ \[RightTee] \ \ \[Not] \ \((p\ \[And] \ q)\)\), FontColor->RGBColor[1, 0, 0]]}], TraditionalForm]]], "\n\nOK, here goes:\n\n", StyleBox["Claim", FontWeight->"Bold"], ": \[Not] p ", StyleBox["\[RightTee]", FontWeight->"Bold"], " \[Not] ( p \[And] q ) and \[Not] q ", StyleBox["\[RightTee]", FontWeight->"Bold"], " \[Not] ( p \[And] q ) \n\n", StyleBox["1\t\[Not] p \t\t\tpremise", FontColor->RGBColor[0, 0, 1]], "\n\n2\tp \[And] q\t\t\tassmp.\n3\tp\t\t\t\[And] e\n\n4\tp \[And] q \ \[Implies] p\t\t\[Implies] i\n", StyleBox["5\t\[Not] ( p \[And] q )\t\tmt", FontColor->RGBColor[0, 0, 1]], "\n\n", StyleBox["Main argument", FontWeight->"Bold"], ":\n\n1\t\[Not] p \[Or] \[Not] q\t\tpremise\n\n2\t\[Not] p\t\t\tassmp.\n3\t\ \[Not] ( p \[And] q )\t\tclaim\n\n4\t\[Not] q\t\t\tassmp.\n5\t\[Not] ( p \ \[And] q )\t\tclaim\n\n6\t\[Not] ( p \[And] q )\t\t\[Or] e\n\nQED\n" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part d", "Subsubsection", CellTags->"c:61"], Cell[TextData[{ Cell[BoxData[ \(TraditionalForm\`p\ \[Or] \ q\ \ \[RightTee] \ \ \[Not] \ \((\ \[Not] p\ \[And] \ \[Not] \ q)\)\)]], "\n\nHere the overblown approach from part c pays off. We already have \n\n\ \t", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\[Not] \[Phi]\ \[Or] \ \[Not] \ \[Psi]\ \ \ \[RightTee] \ \ \[Not] \ \((\[Phi]\ \[And] \ \[Psi])\)\)\)\)]], "\n\t\nfor any formula \[Phi] and \[Psi]. Pick in particular \[Phi] = \ \[Not] p and \[Psi] = \[Not] q, so we have already shown\n\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\[Not] \(\[Not] \ p\)\ \[Or] \ \[Not] \(\[Not] \ q\)\ \ \[RightTee] \ \ \[Not] \ \((\[Not] p \[And] \[Not] q)\)\ \)\)\)]], "\n\t\nand remains to show that \t", Cell[BoxData[ \(TraditionalForm\`\(p\ \[Or] \ q\) \(\(\ \)\(\ \)\) \[RightTee] \)]], " ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\[Not] \(\[Not] \ p\)\ \[Or] \ \[Not] \(\[Not] \ q\)\)\)\)]], ". \nBut that is easy:\n\n1\tp \[Or] q\t\t\tprem\n2\tp\t\t\tassm\n3\t\[Not]\ \[Not]p\t\t\t\[Not]\[Not] i\n4\t\[Not]\[Not] p \[Or] \[Not]\[Not] q\t\t\[Or] \ i\n5\tq\t\t\tassm\n6\t\[Not]\[Not]q\t\t\t\[Not]\[Not] i\n7\t\[Not]\[Not] p \ \[Or] \[Not]\[Not] q\t\t\[Or] i\n8\t\[Not]\[Not] p \[Or] \[Not]\[Not] q\t\t\ \[Or] e" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part e", "Subsubsection", CellTags->"c:62"], Cell[TextData[{ Cell[BoxData[ \(TraditionalForm\`\[Not] \ p\ \[Or] \ q\ \ \[RightTee] \ \ p\ \[Implies] \ q\)]], "\n\nBy the deduction theorem it suffices to show\n\n", Cell[BoxData[ \(TraditionalForm\`\[Not] \ p\ \[Or] \ q, \ p\ \ \[RightTee] \ \ q\)]], "\n\n1\t\[Not] p \[Or] q\t\t\tprem\n2\tp\t\t\tprem\n3\t\[Not] p\t\t\tassm\n\ 4\t\[UpTee]\t\t\t\[UpTee] i\n5\tq\t\t\t\[UpTee] e\n6\tq\t\t\tassm\n7\tq\t\t\t\ \[Or] e 1, 3-5, 6" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part f", "Subsubsection", CellTags->"c:63"], Cell[TextData[{ Cell[BoxData[ \(TraditionalForm\`p \[Implies] \ q\ \ \[RightTee] \ \ \[Not] p\ \[Or] \ q\)]], "\n\nWe may use the excluded middle, so we can argue as follows\n\n1\tp \ \[Implies] q\t\t\tprem\n2\t\[Not] p \[Or] p\t\t\texc.mid.\n3\t\[Not]p\t\t\t\ assm\n4\t\[Not]p\[Or]q\t\t\t\[Or] i\n5\tp\t\t\tassm\n6\tq\t\t\t\[Implies] e\n\ 7\t\[Not]p\[Or]q\t\t\t\[Or] i\n8\t\[Not]p\[Or]q\t\t\t\[Or] e" }], "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Predicate Badgers", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:64"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", CellTags->"c:65"], Cell[TextData[{ "Recall the Lewis Carroll puzzles from last week.\n\n\n1. Animals are \ always mortally offended if I fail to notice them.\n2. The only animals that \ belong to me are in that field. \n3. No animal can guess a conundrum, unless \ it has been properly trained in a Board-School.\n4. None of the animals in \ that field are badgers. \n5. When an animal is mortally offended, it always \ rushes about wildly and howls. \n6. I never notice any animal, unless it \ belongs to me. \n7. No animal, that has been properly trained in a \ Board-School, rushes about wildly and howls. \n\nOne can handle this problem \ quite nicely in propositional logic, but it actually can be more naturally \ expressed in predicate logic. For example, the first assertion can be \ written as \n\n\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] x\ \((\ \[Not] \ N(x)\ \[Implies] \ O(x)\ )\)\)]], "." }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:66"], Cell["\<\ a) Rewrite all of Carroll's assertions as formulae in predicate \ logic. State clearly what the intended meaning of the relation symbols is, \ and what the intended range of the quantifiers is. b) Then use natural deduction to show that the conclusions you drew about \ badgers last week can really be derived in a formal manner. You may use the valid formulae in 7.2.2 (conversion between existential and \ universal quantifiers). Also, feel free to use any equivalences that do not \ involve quantifier manipulations, and focus in your proof on the latter. The argument is a bit long (24 lines in my solution), but all very \ mechanical. You only need to invoke a few inference rules. \ \>", "Text"], Cell[TextData[{ "To preserve the sanity of the graders, use the following unary relation \ symbols, with intended intrepretation as follows:\n\n", Cell[BoxData[ \(TraditionalForm\`N\)]], "\tnotice an animal\n", Cell[BoxData[ \(TraditionalForm\`M\)]], " \tis mine\n", Cell[BoxData[ \(TraditionalForm\`F\)]], "\tin the field\n", Cell[BoxData[ \(TraditionalForm\`B\)]], "\ta badger\n", Cell[BoxData[ \(TraditionalForm\`O\)]], "\toffended\n", Cell[BoxData[ \(TraditionalForm\`R\)]], "\trushes about and howls\n", Cell[BoxData[ \(TraditionalForm\`C\)]], "\tcan guess a conundrum" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", CellTags->"c:67"], Cell["\<\ The assertions then can be translated into the following formulae \ (note that the translations are not unique, yours make look slightly \ different -- though they should be equivalent). \ \>", "Text"], Cell[TextData[{ "\nA1\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] x\ \((\ \[Not] \ N(x)\ \[Implies] \ O(x)\ )\)\)]], "\nA2\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] x\ \((\ M(x)\ \[Implies] \ F(x)\ )\)\)]], "\nA3\t\t", Cell[BoxData[ \(TraditionalForm\`\[Not] \ \[Exists] \ x\ \ \((\ C(x)\ \[And] \ \[Not] \ S(x)\ )\)\)]], "\nA4\t\t", Cell[BoxData[ \(TraditionalForm\`\[Not] \ \[Exists] \ x\ \ \((\ F(x)\ \[And] \ B(x)\ )\)\)]], "\nA5\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] x\ \((\ O(x)\ \[Implies] \ R(x)\ )\)\)]], "\nA6\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] x\ \((\ N(x)\ \[Implies] \ M(x)\ )\)\)]], "\nA7\t\t", Cell[BoxData[ \(TraditionalForm\`\[Not] \ \[Exists] \ x\ \ \((\ S(x)\ \[And] \ R(x)\ )\)\)]], "\n\nThe first step is to rewrite A3, A4, and A7 with universal \ quantifiers. \nWe also use ", Cell[BoxData[ \(TraditionalForm\`\[Not] \ \((\ \[Psi]\ \[And] \ \[Phi]\ )\)\ \ \[DoubleLeftRightArrow] \ \(\[Not] \ \[Psi]\)\ \[Or] \ \[Not] \ \[Phi]\)]], " and the characterization of implication in terms of a disjunction. \n\n\ A3\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \ \((\ C(x)\ \[Implies] \ S(x)\ )\)\)]], "\nA4\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \ \((\ F(x)\ \[Implies] \ \[Not] \ B(x)\ )\)\)]], "\nA7\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \ \((\ S(x)\ \[Implies] \ \[Not] \ R(x)\ )\)\)]], "\n\nNow the main proof.\n\n1\t\t", Cell[BoxData[ \(TraditionalForm\`B(x)\)]], "\t\t\t\t\tassmp.\n2\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \ \((\ F(x)\ \[Implies] \ \[Not] \ B(x)\ )\)\)]], "\t\t\tA4\n3\t\t", Cell[BoxData[ \(TraditionalForm\`F(x)\ \[Implies] \ \[Not] \ B(x)\)]], "\t\t\t\[ForAll] e, 2\n4\t\t", Cell[BoxData[ \(TraditionalForm\`\[Not] \ F(x)\)]], "\t\t\t\t\tmt, 1, 3\n5\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] x\ \((\ M(x)\ \[Implies] \ F(x)\ )\)\)]], "\t\t\tA2\n6\t\t", Cell[BoxData[ \(TraditionalForm\`M(x)\ \[Implies] \ F(x)\)]], "\t\t\t\t\[ForAll] e, 5\n7\t\t", Cell[BoxData[ \(TraditionalForm\`\[Not] \ M(x)\)]], "\t\t\t\t\tmt, 4, 6\n8\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] x\ \((\ N(x)\ \[Implies] \ M(x)\ )\)\)]], "\t\t\tA6\n9\t\t", Cell[BoxData[ \(TraditionalForm\`N(x)\ \[Implies] \ M(x)\)]], "\t\t\t\t\[ForAll] e, 6\n10\t\t", Cell[BoxData[ \(TraditionalForm\`\[Not] \ N(x)\)]], "\t\t\t\t\tmt, 7, 9\n11\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] x\ \((\ \[Not] \ N(x)\ \[Implies] \ O(x)\ )\)\)]], "\t\t\tA1\n12\t\t", Cell[BoxData[ \(TraditionalForm\`\[Not] \ N(x)\ \[Implies] \ O(x)\)]], "\t\t\t\[ForAll] e, 11\n13\t\t", Cell[BoxData[ \(TraditionalForm\`O(x)\)]], "\t\t\t\t\t\[Implies] e, 10, 12\n14\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] x\ \((\ O(x)\ \[Implies] \ R(x)\ )\)\)]], "\t\t\tA5\n15\t\t", Cell[BoxData[ \(TraditionalForm\`O(x)\ \[Implies] \ R(x)\)]], "\t\t\t\t\[ForAll] e, 14\n16\t\t", Cell[BoxData[ \(TraditionalForm\`R(x)\)]], "\t\t\t\t\t\[Implies] e, 13, 15\n17\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \ \((\ S(x)\ \[Implies] \ \[Not] \ R(x)\ )\)\)]], "\t\t\tA7\n18\t\t", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(S(x)\ \[Implies] \ \[Not] \ R(x)\)\)\)]], "\t\t\t\t\[ForAll] e, 17\n19\t\t", Cell[BoxData[ \(TraditionalForm\`\[Not] \ S(x)\)]], "\t\t\t\t\tmt, 16, 18\n20\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \ \((\ C(x)\ \[Implies] \ S(x)\ )\)\)]], "\t\t\tA3\n21\t\t", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(C(x)\ \[Implies] \ S(x)\)\)\)]], "\t\t\t\t\[ForAll] e, 17\n22\t\t", Cell[BoxData[ \(TraditionalForm\`\[Not] \ C(x)\)]], "\t\t\t\t\tmt, 19, 21\n23\t\t", Cell[BoxData[ \(TraditionalForm\`B(x)\ \[Implies] \ \[Not] \ C(x)\)]], "\t\t\t\t\[Implies] i, 1, 22\n24\t\t", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \((\ B(x)\ \[Implies] \ \[Not] \ C(x)\ )\)\)]], "\t\t\t\[ForAll] i, 23" }], "Text"], Cell[TextData[{ "By discharging the assumption earlier, we could have shown analogous \ results relating badgers to other properties. E.g., ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\[ForAll] x\ \((\ B(x)\ \[Implies] \ R(x)\ )\)\)\)\)]], "." }], "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Quantifiers", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:68"], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:69"], Cell[TextData[{ "Which of the following sentences is valid? Give reasons for your answer. \n\ a) ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \(\[Exists] \ y\ \(\[Phi](x, y)\)\)\ \ \[Implies] \ \[Exists] \ y\ \(\[ForAll] \ x\ \ \(\[Phi](x, y)\)\)\)]], "\nb) ", Cell[BoxData[ \(TraditionalForm\`\[Exists] \ y\ \(\[ForAll] \ x\ \ \(\[Phi](x, y)\)\)\ \[Implies] \[ForAll] \ x\ \(\[Exists] \ \(\(\(y\)\(\ \)\) \(\[Phi](x, y)\)\(\ \)\)\)\)]], "\nc) ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \(\[Exists] \ y\ \(\[Phi](x, y)\)\)\ \ \[Implies] \ \[ForAll] \ y\ \(\[Exists] \ x\ \ \(\[Phi](x, y)\)\)\)]], "\n" }], "Text", Evaluatable->False, AspectRatioFixed->True, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, FontFamily->"Times", FontSize->18, CellTags->"c:70"], Cell[CellGroupData[{ Cell["Part a", "Subsubsection", CellTags->"c:71"], Cell[TextData[{ "False. Take ", Cell[BoxData[ \(TraditionalForm\`\(\(\[Phi](x, y)\)\(\ \)\)\)]], " to be ", Cell[BoxData[ \(TraditionalForm\`x\ < \ y\)]], " over, say, the natural numbers. The premise says: for every natural \ number there is a larger one, but the conclusion says there is a number \ larger than all numbers. " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part b", "Subsubsection", CellTags->"c:72"], Cell[TextData[{ "True. The premise says that the is a uniform witness ", Cell[BoxData[ \(TraditionalForm\`y\)]], " that works for all choices of ", Cell[BoxData[ \(TraditionalForm\`x\)]], ". The conclusion only says that for every ", Cell[BoxData[ \(TraditionalForm\`x\)]], " there is a witness ", Cell[BoxData[ \(TraditionalForm\`y\)]], ", which might depend on ", Cell[BoxData[ \(TraditionalForm\`x\)]], ". " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part c", "Subsubsection", CellTags->"c:73"], Cell[TextData[{ "False. Again take ", Cell[BoxData[ \(TraditionalForm\`\(\(\[Phi](x, y)\)\(\ \)\)\)]], " to be ", Cell[BoxData[ \(TraditionalForm\`x\ < \ y\)]], " over, say, the natural numbers. The premise says: for every natural \ number there is a larger one, but the conclusion says for every number there \ is a smaller one (false for 0). " }], "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Quantifier Transformations", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:74"], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:75"], Cell[TextData[{ "a) Show that ", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[ForAll] x\ \(\[Phi]( x)\)\ \ \[LeftRightArrow] \ \(\[Not] \ \[Exists] x\ \(\[Not] \ \ \[Phi](x)\)\)\)\)]], "\n\nb) Show that ", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[Exists] x\ \(\[Phi]( x)\)\ \ \[LeftRightArrow] \ \(\[Not] \ \[ForAll] x\ \(\[Not] \ \ \[Phi](x)\)\)\)\)]], "\n\nNote that we are asking for derivations, not just an intuitive \ validity test. \n\nIt is probably best first to draw a proof tree on paper \ (see the lecture notes and/or the book), and then flatten out the tree into a \ linear sequence. Make sure to check that the quantifier rules are properly \ used. " }], "Text", Evaluatable->False, AspectRatioFixed->True, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, FontFamily->"Times", FontSize->18, CellTags->"c:76"], Cell["\<\ To make the argument a bit more transparent, first a little \ auxiliary claim: an implication and its contrapositive are (provably) \ equivalent. We could combine everything into a single long derivation, but \ it's easier to see what is going on if we break the argument apart. \ \>", "Text"], Cell[CellGroupData[{ Cell["Claim 1: The Contrapositive", "Subsubsection", CellTags->"c:77"], Cell[TextData[{ "The contrapositive is provably equivalent to an implication:\n\n\t(1) ", Cell[BoxData[ \(TraditionalForm\`\(\(\(\[Phi]\)\(\ \)\)\(\[Rule]\)\(\ \)\(\[Psi]\ \ \ \[RightTee] \ \[Not] \ \[Psi]\ \[Rule] \ \[Not] \ \[Phi]\)\(\ \)\)\)]], "\n\t(2) ", Cell[BoxData[ \(TraditionalForm\`\(\(\(\[Not] \[Phi]\)\(\ \)\)\(\[Rule]\)\(\ \)\(\ \[Not] \[Psi]\ \ \[RightTee] \ \ \[Psi]\ \[Rule] \ \ \[Phi]\)\(\ \)\)\)]], "\n\nHere is a derivation for (1):\n\n1\t\[Phi] \[Rule] \[Psi] \t\t\tprem\n\ 2\t\[Not] \[Psi]\t\t\tassm\n3\t\[Phi]\t\t\tassm\n4\t\[Psi]\t\t\t\[Rule] e, 1, \ 3\n5\t\[UpTee]\t\t\t\[Not] e, 2, 4\n6\t\[Not] \[Phi]\t\t\t\[Not] i, 3, 5\n7\t\ \[Not] \[Psi] \[Rule] \[Not] \[Phi]\t\t\[Rule] i, 2, 6\n\n(2) follows from \ (1) and the double negation rules. \n" }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Claim 2: Negating Biconditionals", "Subsubsection", CellTags->"c:78"], Cell[TextData[{ "From claim 1 we can conclude that a biconditional is provable iff the \ biconditional where each side is negated is provable. \n", StyleBox["\n\t", FontWeight->"Bold"], " ", Cell[BoxData[ \(TraditionalForm\`\[Phi]\ \[LeftRightArrow] \ \[Psi]\ \ \[RightTee] \ \ \[Not] \ \(\(\(\[Phi]\)\(\ \)\)\(\[LeftRightArrow]\)\(\ \)\(\[Not] \ \[Psi]\ \)\(\ \)\)\)]] }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Main Part", "Subsubsection", CellTags->"c:79"], Cell[TextData[{ "Now for the main argument. We have to show\n\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[ForAll] x\ \(\[Phi]( x)\)\ \ \[LeftRightArrow] \ \(\[Not] \ \[Exists] x\ \(\[Not] \ \ \[Phi](x)\)\)\)\)]], "\n\nBy the claim, it suffices to show \n\n\ta) ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\[ForAll] x\ \ \ \[Phi]\ \ \[RightTee] \ \ \[Not] \ \[Exists] \ \(\[Not] x\ \ \[Phi]\)\)\)\)]], "\n\tb) ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\[Not] \ \[ForAll] x\ \ \ \[Phi]\ \ \ \[RightTee] \ \ \[Exists] \ \(\[Not] x\ \ \[Phi]\)\)\)\)]], "\n\nWe have dropped the ", Cell[BoxData[ \(TraditionalForm\`\((x)\)\)]], " in ", Cell[BoxData[ \(TraditionalForm\`\[Phi](x)\)]], " and ", Cell[BoxData[ \(TraditionalForm\`\[Psi](x)\)]], " for the sake of legibility. \nTo see that this is enough, note the it \ follows from a) by \[Rule] i that\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[ForAll] x\ \[Phi]\)\ \ \ \[Rule] \ \[Not] \ \[Exists] x\ \(\[Not] \ \[Phi]\)\)]], " \nand from b) that \n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[Not] \ \[ForAll] x\ \ \[Phi]\)\ \ \[Rule] \ \[Exists] x\ \(\[Not] \ \[Phi]\)\)]], ".\nFrom b) and the claim we get ", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[Not] \ \[Exists] x\ \(\ \[Not] \ \[Phi]\)\)\ \ \[Rule] \ \[ForAll] \ x\ \[Phi]\)]], "." }], "Text"], Cell["\<\ Part a) 1\t\[Exists] x \[Not] \[Phi]\t\t\t\tassm 2\t\[Not] \[Phi]\t\t\t\tassm 3\t\[ForAll] x \[Phi]\t\t\t\tprem 4\t\[Phi]\t\t\t\t\[ForAll] e, 3 5\t\[UpTee]\t\t\t\t\[UpTee] i, 2, 4 6\t\[UpTee]\t\t\t\t\[Exists] e, 1, 2-5 7\t\[Not] \[Exists] x \[Not] \[Phi]\t\t\t\[Not] i, 1-6 \ \>", "Text"], Cell["\<\ Part b) 1\t\[Not] \[ForAll] x \[Phi]\t\t\t\tprem 2\t\[Phi]\t\t\t\tassm 3\t\[ForAll] x \[Phi]\t\t\t\t\[ForAll] i, 2 4\t\[UpTee]\t\t\t\t\[UpTee] i, 2, 3 5\t\[Not] \[Phi]\t\t\t\t\[Not] i, 2 - 4 6\t\[Exists] x \[Not] \[Phi]\t\t\t\t\[Exists] i, 5 \ \>", "Text"], Cell[TextData[{ "It remains to show that \n\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[Exists] x\ \(\[Phi]( x)\)\ \ \[LeftRightArrow] \ \(\[Not] \ \[ForAll] x\ \(\[Not] \ \ \[Phi](x)\)\)\)\)]], "\n\nWe could give direct deduction proofs, but that is a bit tedious. \ Let's exploit the previous result, and our claims. \nWe have to show \n\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[Exists] x\ \[Phi]\ \ \ \[LeftRightArrow] \ \(\[Not] \ \[ForAll] x\ \(\[Not] \ \[Phi]\)\)\)\)]], "\n\nbut we already know \t\n\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[ForAll] x\ \[Phi]\ \ \ \[LeftRightArrow] \ \(\[Not] \ \[Exists] x\ \(\[Not] \ \[Phi]\)\)\)\)]], "\n\nReplace ", Cell[BoxData[ \(TraditionalForm\`\(\(\[Phi]\) \(\(\ \)\(\ \)\) \(by\) \(\(\ \)\(\ \ \)\) \(\[Not] \ \[Psi]\)\(\ \)\)\)]], " and apply claim 2:\n\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[Not] \ \[ForAll] x\ \(\ \[Not] \ \[Psi]\ \ \[LeftRightArrow] \ \(\[Not] \ \(\[Not] \ \[Exists] x\ \(\ \[Not] \ \(\[Not] \ \[Psi]\)\)\)\)\)\)\)]], "\n\nwhich can be rewritten as \n\n\t", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\ \)\) \(\[Exists] x\ \ \[Psi]\ \ \ \[LeftRightArrow] \ \(\[Not] \ \[ForAll] x\ \(\[Not] \[Psi]\)\)\)\)]], "\n\nDone!" }], "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Maximally Consistent Sets", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:81"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", CellTags->"c:82"], Cell[TextData[{ "Recall that a set of formulae ", Cell[BoxData[ \(TraditionalForm\`\[CapitalGamma]\)]], " is consistent if not ", Cell[BoxData[ \(TraditionalForm\`\(\(\(\[CapitalGamma]\)\(\ \)\(\[RightTee]\)\)\(\ \)\ \(\[UpTee]\)\)\)]], ". \nIt is deductively closed if for any formula ", Cell[BoxData[ \(TraditionalForm\`\[Phi]\)]], " we have ", Cell[BoxData[ \(TraditionalForm\`\[CapitalGamma]\ \[RightTee] \ \[Phi]\)]], " implies ", Cell[BoxData[ \(TraditionalForm\`\[Phi]\ \[Element] \ \[CapitalGamma]\)]], ". \t\n", Cell[BoxData[ \(TraditionalForm\`\[CapitalGamma]\)]], " is maximally consistent if no proper superset of formulae is still \ consistent. " }], "Text", Evaluatable->False, AspectRatioFixed->True, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:83"], Cell[TextData[{ "Let ", Cell[BoxData[ \(TraditionalForm\`\[CapitalGamma]\)]], " be a set of formulae that is both consistent and deductively closed. \n\ Show that the following are equivalent:\n(a) ", Cell[BoxData[ \(TraditionalForm\`\[CapitalGamma]\)]], " is maximally consistent.\n(b) For any formula \[Phi], ", Cell[BoxData[ \(TraditionalForm\`\[Phi]\ \[Element] \ \[CapitalGamma]\)]], " or ", Cell[BoxData[ \(TraditionalForm\`\[Not] \[Phi]\ \[Element] \ \[CapitalGamma]\)]], ".\n(c) ", Cell[BoxData[ \(TraditionalForm\`\[Phi]\ \[Or] \ \[Psi]\ \[Element] \ \ \[CapitalGamma]\)]], " implies ", Cell[BoxData[ \(TraditionalForm\`\[Phi]\ \[Element] \ \[CapitalGamma]\)]], " and ", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\[Psi]\ \[Element] \ \ \[CapitalGamma]\)\)\)]], "." }], "Text", Evaluatable->False, AspectRatioFixed->True, Background->GrayLevel[1]], Cell["\<\ Make sure to show that all three assertions are equivalent. For \ examples, you could prove that (a) implies (b), (b) implies (c), and (c) \ implies (a). State clearly how your proof works. \ \>", "Text", Evaluatable->False, AspectRatioFixed->True, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, FontFamily->"Times", FontSize->18, CellTags->"c:84"], Cell[CellGroupData[{ Cell["(a) implies (b)", "Subsubsection", CellTags->"c:85"], Cell[TextData[{ "Suppose that \[Phi] is not in \[CapitalGamma]. \nThen \[CapitalGamma] + \ \[Phi] is inconsistent since \[CapitalGamma] is maximally consistent. \nSo \ ", Cell[BoxData[ \(TraditionalForm\`\[CapitalGamma], \ \[Phi]\ \[RightTee] \ \(\(\ \[UpTee]\)\(\ \)\)\)]], " and therefore ", Cell[BoxData[ \(TraditionalForm\`\[CapitalGamma]\ \[RightTee] \ \[Phi]\ \[Rule] \ \ \[UpTee] \)]], ". \nIt is easy to see that ", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\(\ \)\(\ \)\) \(\[Not] \ \[Phi]\ \ \ \[LeftRightArrow] \ \ \((\ \[Phi]\ \[Rule] \ \[UpTee] \ )\)\)\)\)]], ", so ", Cell[BoxData[ \(TraditionalForm\`\[CapitalGamma]\ \[RightTee] \ \[Not] \ \[Phi]\)]], ". \nBut that means \[Not] \[Phi] is in \[CapitalGamma], since \ \[CapitalGamma] is closed under deduction. " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["(b) implies (c)", "Subsubsection", CellTags->"c:86"], Cell[TextData[{ "If \[Phi] \[Element] \[CapitalGamma] or \[Psi] \[Element] \[CapitalGamma] \ then \[Phi] \[Or] \[Psi] \[Element] \[CapitalGamma] by \[Or] introduction \ and the closure property of \[CapitalGamma]. \n\nSo suppose that \[Phi]\[Or]\ \[Psi] is in \[CapitalGamma], but neither \[Phi] \[Element] \[CapitalGamma] \ nor \[Psi] \[Element] \[CapitalGamma]. \nBy the assumption, \[Not] \[Phi] \ \[Element] \[CapitalGamma] and \[Not] \[Psi] \[Element] \[CapitalGamma]. \ Hence \[Not] \[Phi] \[And] \[Not] \[Psi] \[Element] \[CapitalGamma]. \nIt \ is easy to see (sort of) that ", Cell[BoxData[ \(TraditionalForm\`\(\(\[RightTee]\)\(\(\ \)\(\ \)\) \(\[Not] \ \[Phi]\ \ \[And] \ \[Not] \ \[Psi]\ \ \[LeftRightArrow] \ \ \(\[Not] \ \((\ \[Phi]\ \ \[Or] \ \[Psi]\ )\)\)\)\)\)]], ", so \[CapitalGamma] contains \[Not] ( \[Phi] \[Or] \[Psi] ).\nBut then \ \[CapitalGamma] is inconsistent, contradiction." }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["(c) implies (a)", "Subsubsection", CellTags->"c:87"], Cell["\<\ Suppose that \[CapitalGamma] + \[Phi] is consistent but that \ \[Phi] \[NotElement] \[CapitalGamma]. Since \[Phi] \[Or] \[Not] \[Phi] is derivable, and thus in \ \[CapitalGamma], we must have \[Not] \[Phi] in \[CapitalGamma], contradicting \ the consistency of \[CapitalGamma] + \[Phi]. \ \>", "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Formulae over \[DoubleStruckCapitalQ] and \[DoubleStruckCapitalR]", \ "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:88"], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:89"], Cell[TextData[{ "Consider the usual structure \[DoubleStruckCapitalR] of the real numbers, \ and the structure of the rational numbers ", Cell[BoxData[ \(TraditionalForm\`\[DoubleStruckCapitalQ]\)]], ". \nLet 2 be a constant denoting the number two. \nFor each of the \ following formulae determine whether it holds over either structure.\n\na) \ ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \(\[Exists] \ y\ \((\ x\ = \ y + y\ )\)\)\)]], "\nb) ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ \(\[Exists] \ y\ \((\ x\ > \ 0 \[Implies] x\ = \ y\[CenterDot]y\ )\)\)\)]], "\nc) ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \ x\ , \ y \(\[Exists] \ z\ \((\ x\ > \ y \[Implies] x\ > \ z\ \[And] \ z\ > \ y\ )\)\)\)]], "\nd) ", Cell[BoxData[ \(TraditionalForm\`\[Exists] \ x\ , \ u, \ v\ , w\ \((\ x\ \ \[CenterDot]\ x\ \[CenterDot]\ x\ = \ \(u\ \ \[And] \ x\ \[CenterDot]\ x\ = \ \(v\ \[And] \ 2\[CenterDot]\ x\ + \ w\ = \(0 \[And] \ u\ + v + w = \ 2\ \ \[And] \ x\ + 1\ \[NotEqual] \ 0\)\)\))\)\)]] }], "Text", Evaluatable->False, AspectRatioFixed->True, Background->GrayLevel[1]], Cell["(x^2 - 2)(x+1) // Expand", "Input"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, FontFamily->"Times", FontSize->18, CellTags->"c:90"], Cell[CellGroupData[{ Cell["Part a", "Subsubsection", CellTags->"c:91"], Cell["True over both structures: we can divide by 2. ", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part b", "Subsubsection", CellTags->"c:92"], Cell["\<\ True over the reals, false over the rationals: not every positive \ rational number has a square root in the rationals. \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part c", "Subsubsection", CellTags->"c:93"], Cell["\<\ True in both structures. The formula says the standard order is \ dense. \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part d", "Subsubsection", CellTags->"c:94"], Cell[TextData[{ "True in both structures. The formula says ", Cell[BoxData[ \(TraditionalForm\`\(-2\) - 2\ x + x\^2 + x\^3\)]], " has a root other than ", Cell[BoxData[ \(TraditionalForm\`\(-1\)\)]], ", but the other two roots are irrational:" }], "Text"], Cell[BoxData[ \(\(\(-2\)\(-\)\(2\ x\)\(+\)\(x^2\)\(\ \)\(+\)\(\ \)\(x^3\)\(\ \)\) // \ Factor\)], "Input"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Davis Putnam", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:95"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:96"], Cell["\<\ In class you have seen the Davis/Putnam algorithm, a method to \ determine whether a formula in CNF is satisfiable. The algorithm looks \ essentially like this\ \>", "Text"], Cell[TextData[{ StyleBox["DavisPutnam[ S ]\n\tdo\n\t\tremove a unit clause\n\tuntil( no \ unit clauses are left );\n\t\n\tif( there is an empty clause ) return False;\ \n\tif( there are no clauses left ) return True;\n\t\n\tpick a literal x in \ S;\n\treturn DavisPutnam[ S + {x} ] || DavisPutnam[ S + {Not[x]}];", "Input"], "\n\t" }], "Program"], Cell[TextData[{ "In this problem, you are supposed to apply the Davis/Putnam algorithm by \ hand to some small formulae. To facilitate grading, let us adopt the \ following convention:\n\n\t\[FilledCircle] Always remove the \ lexicographically smallest literal if there are several unit clauses.\n\t\ \[FilledCircle] Always split with the lexicographically smallest literal.\n\t\ \nSo the priority ranking is ", Cell[BoxData[ FormBox[ RowBox[{ RowBox[{"a", " ", ",", " ", FormBox[\(\(\[InvisibleSpace]\)\(\[Not] a\)\), "TraditionalForm"], " ", ",", " ", "b", " ", ",", " ", \(\[Not] \ b\), " ", ",", " ", "c", ",", " ", "\[Ellipsis]"}], " "}], TraditionalForm]]], "\nWrite down all the intermediate results after each unit clause removal, \ and indicate clearly which literal is used (both for removal and splitting). \ Put each splitting case into a separate cell. In the end, state clearly if \ the formula is satisfiable or not. \n\nYou don't have to bother with pretty \ negation signs ", Cell[BoxData[ \(TraditionalForm\`\[Not] \ x\)]], ", a simple ", Cell[BoxData[ \(TraditionalForm\`\(! x\)\)]], " will do. " }], "Text"], Cell[TextData[{ StyleBox["Example", FontWeight->"Bold"], ":\n\n\t", Cell[BoxData[ \(TraditionalForm\`{{a, b}, {a, c}, {b, c}, {a, b, c}, {\[InvisibleSpace]\[Not] a, \[InvisibleSpace]\[Not] b, \ \[InvisibleSpace]\[Not] c}}\)]], "\n\t\nThere are no unit clauses, so we must split the formula right away, \ and, by our convention, we must split on ", Cell[BoxData[ \(TraditionalForm\`a\)]], ". It so happens that the first split already leads to success, we show \ the ", Cell[BoxData[ \(TraditionalForm\`\[Not] a\)]], " branch only to demonstrate nice typesetting. " }], "Text"], Cell[TextData[{ Cell[BoxData[ \(TraditionalForm\`a\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{\ {b, c}, {\[InvisibleSpace]\[Not] b, \[InvisibleSpace]\[Not] c}\ }\)]], "\n", Cell[BoxData[ \(TraditionalForm\`b\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{\ {\[InvisibleSpace]\[InvisibleSpace]\[Not] c}\ \ }\)]], "\n", Cell[BoxData[ \(TraditionalForm\`\[Not] c\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{\ \ \ }\)]], "\t\tempty sentence \[DoubleLongRightArrow] True, done" }], "Text"], Cell[TextData[{ Cell[BoxData[ \(TraditionalForm\`\[Not] a\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{\({b}\)\(,\)\({c}\)\(,\)\({b, c}\)\(,\)\({b, c}\)\(\ \)}\)]], "\n", Cell[BoxData[ \(TraditionalForm\`b\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{\ {c}\ }\)]], "\n", Cell[BoxData[ \(TraditionalForm\`c\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{\ \ \ }\)]], "\t\tempty sentence \[DoubleLongRightArrow] True, done once again." }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:97"], Cell[TextData[{ "Apply the Davis/Putnam algorithm to the following formulae. If the formula \ turns out to be satisfiable, determine a satisfying assignment and use ", StyleBox["Mathematica", FontSlant->"Italic"], " to check that your assignment really works. \n\na) ", Cell[BoxData[ \(TraditionalForm\`{\ \ {a, b, c}, \ {\[Not] a, b, c}, {\[Not] a, \[Not] b, c}, \ {\[Not] b, \[Not] c}\ }\)]], "\n\nb) ", Cell[BoxData[ \(TraditionalForm\`{{a, b}, {a, c}, {b, c}, {\[InvisibleSpace]\[Not] a, \[InvisibleSpace]\[Not] b}, {\ \[InvisibleSpace]\[Not] a, \[InvisibleSpace]\[Not] c}, {\[InvisibleSpace]\ \[Not] b, \[InvisibleSpace]\[Not] c}, {a, b, c}}\)]] }], "Text", Evaluatable->False, AspectRatioFixed->True, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", Evaluatable->False, AspectRatioFixed->True, FontFamily->"Times", FontSize->18, CellTags->"c:98"], Cell[CellGroupData[{ Cell["Part a", "Subsubsection", CellTags->"c:99"], Cell[TextData[{ "We indicate the next literal to be use for unit clause elimination or \ splitting on the left.\n\n\t ", Cell[BoxData[ \(TraditionalForm\`{\ \ {a, b, c}, \ {\[Not] a, b, c}, {\[Not] a, \[Not] b, c}, \ {\[Not] b, \[Not] c}\ \ }\)]], "\n", Cell[BoxData[ \(TraditionalForm\`a\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{\ \ \ {b, c}, {\[Not] b, c}, \ {\[Not] b, \[Not] c}\ \ }\)]], "\n", Cell[BoxData[ \(TraditionalForm\`b\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{\ \ \ {c}, \ {\[Not] c}\ \ }\)]], "\n", Cell[BoxData[ \(TraditionalForm\`c\)]], " \t\n\t", Cell[BoxData[ \(TraditionalForm\`{{}}\)]], "\t\tempty clause \[Rule] False\n", Cell[BoxData[ \(TraditionalForm\`\[Not] b\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{\ \ \ {c}\ \ }\)]], "\n", Cell[BoxData[ \(TraditionalForm\`c\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{\ }\)]], "\t \tempty sentence \[Rule] True\n\nThe formula is satisfiable. \nCheck \ the truth assignment found:" }], "Text"], Cell[BoxData[ \(\((a || b || c)\) && \((\(! a\) || b || c)\) && \((\(! a\) || \(! b\) || c)\) && \((\(! b\) || \(! c\))\) /. \[InvisibleSpace]{a \[Rule] True, b \[Rule] False, c \[Rule] True}\)], "Input"] }, Closed]], Cell[CellGroupData[{ Cell["Part b", "Subsubsection", CellTags->"c:100"], Cell[TextData[{ "\t ", Cell[BoxData[ \(TraditionalForm\`{{a, b}, {a, c}, {b, c}, {\[InvisibleSpace]\[Not] a, \[InvisibleSpace]\[Not] b}, {\ \[InvisibleSpace]\[Not] a, \[InvisibleSpace]\[Not] c}, {\[InvisibleSpace]\ \[Not] b, \[InvisibleSpace]\[Not] c}, {a, b, c}}\)]] }], "Text", Evaluatable->False, AspectRatioFixed->True, Background->GrayLevel[1]], Cell[TextData[{ Cell[BoxData[ \(TraditionalForm\`a\)]], "\n\t ", Cell[BoxData[ \(TraditionalForm\`{{b, c}, {\[InvisibleSpace]\[InvisibleSpace]\[Not] b}, \ {\[InvisibleSpace]\[Not] c}, {\[InvisibleSpace]\[Not] b, \[InvisibleSpace]\ \[Not] c}}\)]], "\n", Cell[BoxData[ \(TraditionalForm\`\[Not] b\)]], " \n\t ", Cell[BoxData[ \(TraditionalForm\`{{c}, {\[InvisibleSpace]\[Not] c}, {c}}\)]], "\n", Cell[BoxData[ \(TraditionalForm\`c\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{{}}\)]], "\t\tempty clause \[DoubleLongRightArrow] False\n" }], "Text", Evaluatable->False, AspectRatioFixed->True, Background->GrayLevel[1]], Cell[TextData[{ " ", Cell[BoxData[ \(TraditionalForm\`\[Not] a\)]], "\n\t ", " ", Cell[BoxData[ \(TraditionalForm\`{{b}, {c}, {b, c}, {\[InvisibleSpace]\[Not] b, \[InvisibleSpace]\[Not] c}, {b, c}}\)]], "\n", Cell[BoxData[ \(TraditionalForm\`b\)]], " \n\t ", Cell[BoxData[ \(TraditionalForm\`{{c}, {\[InvisibleSpace]\[Not] c}, {c}}\)]], "\n", Cell[BoxData[ \(TraditionalForm\`c\)]], "\n\t", Cell[BoxData[ \(TraditionalForm\`{{}}\)]], "\t\tempty clause \[DoubleLongRightArrow] False\n" }], "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Date Game", "Section", Evaluatable->False, PageBreakAbove->True, AspectRatioFixed->True, CellTags->"c:101"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", CellTags->"c:102"], Cell["\<\ Here is an admittedly boring two-person game. However, the game \ admits a nice analysis and can be generalized in many ways. The two players alternately name dates, subject to certain rules. \[Bullet] The starting date is January 1. \[Bullet] A player may increase either the month of the current date, or the \ day, but not both. \[Bullet] The player who reaches December 31 wins. \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:103"], Cell["\<\ a) Show that the first player has a winning strategy. b) Write a program that checks if a position is winning. \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", FontColor->RGBColor[0, 0, 1], CellTags->"c:104"], Cell[CellGroupData[{ Cell["Part a", "Subsubsection", CellTags->"c:105"], Cell[TextData[{ "First, let's get rid of the smokescreen. We are actually looking for a \ sequence of pairs of numbers ", Cell[BoxData[ \(TraditionalForm\`\((a, b)\)\)]], " where \n\[Bullet] the initial pair is ", Cell[BoxData[ \(TraditionalForm\`\((1, 1)\)\)]], ",\n\[Bullet] ", Cell[BoxData[ \(TraditionalForm\`1\ \[LessEqual] \ a \[LessEqual] \ 12\)]], " and ", Cell[BoxData[ \(TraditionalForm\`1\ \[LessEqual] \ b\ \[LessEqual] \ N\_a\)]], " where ", Cell[BoxData[ \(TraditionalForm\`N\_a\)]], " is the number of days in month ", Cell[BoxData[ \(TraditionalForm\`a\)]], ",\n\[Bullet] the next pair ", Cell[BoxData[ \(TraditionalForm\`\((c, d)\)\)]], " satisfies ", Cell[BoxData[ \(TraditionalForm\`a = c\)]], " and ", Cell[BoxData[ \(TraditionalForm\`b\ < \ d\)]], " or ", Cell[BoxData[ \(TraditionalForm\`a < c\)]], " and ", Cell[BoxData[ \(TraditionalForm\`b = d\)]], ". \n\nThe first player to reach ", Cell[BoxData[ \(TraditionalForm\`\((12, 31)\)\)]], " wins. \n\nNow for some reverse engineering. If player I can get to ", Cell[BoxData[ \(TraditionalForm\`\((11, 30)\)\)]], " she's done, right? \nBut then she is also done if he can get to ", Cell[BoxData[ \(TraditionalForm\`\((10, 29)\)\)]], ": every move of II either leads directly to a win for I, or leads to ", Cell[BoxData[ \(TraditionalForm\`\((11, 30)\)\)]], ". By threading backward, ", Cell[BoxData[ \(TraditionalForm\`\((1, 20)\)\)]], " is the right choice for the first move. " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part b", "Subsubsection", CellTags->"c:106"], Cell["\<\ We can represent positions as pairs of numbers in the proper \ range. The first step is to write a function, that on input a position \ determines all possible next positions (all possible moves if you will). This \ is easy, except that the number of days in a month is not constant.\ \>", \ "Text"], Cell["\<\ Clear[next,month] month = {31,28,31,30,31,30,31,31,30,31,30,31}; next[{x_,y_}] := Join[ Table[ {x,i}, {i,y+1,month[[x]]} ], \t\tTable[ {i,y}, {i,x+1,12} ] ];\ \>", "Input"], Cell["next[{8,20}]", "Input"], Cell["next[{12,31}]", "Input"], Cell[TextData[{ "Now a function that check is a position is winning. We have to be careful \ about what it means that a position ", Cell[BoxData[ \(TraditionalForm\`\((a, b)\)\)]], " is winning: the player who is supposed to make the next move can \ ultimately win by using the proper strategy. In this sense, ", Cell[BoxData[ \(TraditionalForm\`\((12, 31)\)\)]], " is lost, since the next player cannot move at all. \nThe crucial idea is \ to use recursion:\n\n\t", Cell[BoxData[ \(TraditionalForm\`\((a, b)\)\)]], " is winning iff ", Cell[BoxData[ \(TraditionalForm\`\[Exists] \ \ \((c, d)\)\ \[Element] \ \(next[\((a, b)\)]\ : \ \ \((c, d)\)\ is\ \(\(lost\)\(.\)\)\)\)]], "\n\t\nMake sure you understand the following code. It uses hashing to \ avoid recomputation (a bit easier that in C/C++ where you have to manage the \ hash table yourself)." }], "Text"], Cell["\<\ Clear[winning,lost] winning[{12,31}] = False; winning[{x_,y_}] := winning[{x,y}] = \tSelect[ next[{x,y}], lost ]=!={}; \t lost[{x_,y_}] := \tlost[{x,y}] = Not[ winning[{x,y}] ]; \ \>", "Input"], Cell["winning[{12,15}] ", "Input"], Cell["winning[{1,20}]", "Input"], Cell["winning[{1,21}]", "Input"], Cell["Select[ CartesianProduct[12,31], lost ] ", "Input"], Cell[TextData[{ "Thus, starting at ", Cell[BoxData[ \(TraditionalForm\`\((1, 1)\)\)]], ", there is only one proper move for player I: ", Cell[BoxData[ \(TraditionalForm\`\((1, 20)\)\)]], ". Player II is now in a lost position, and cannot win. Make sure you \ understand precisely how I would counter any possible move by II. " }], "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Tautology Testing", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:107"], Cell[CellGroupData[{ Cell["Background", "Subsubsection", CellTags->"c:108"], Cell["\<\ As pointed out in class, testing whether a propositional formula is \ a tautology is trivial in principle (just build the truth table) but very \ hard when it comes to efficiency. All known algorithms for the decision \ problem Tautology are catastrophically slow on some inputs. A fast, general \ algorithm would be a major breakthrough in CS -- but, there are good reasons \ to believe that really fast algorithms do not exist. At any rate, sometimes the test is easy, most notably when the formula is in \ CNF (conjunctive normal form). \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:109"], Cell["\<\ a) Explain exactly why Tautology is easy if the input is in CNF. \ \ \>", "Text"], Cell["\<\ b) Fred Hacker (who went to MIT) now has the following bright \ idea. We know that every formula can be transformed into an equivalent one \ in CNF. So, to crack Tautology for an arbitrary formula, Fred proposes a \ 2-step algorithm: \t\[Bullet] First translate the given formula into CNF. \t\[Bullet] Then use the very fast algorithm from part a). Fred really would like to patent this idea. What will he hear from the \ patent office? Why?\ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", CellTags->"c:110"], Cell[CellGroupData[{ Cell["Part a", "Subsubsection", CellTags->"c:111"], Cell[TextData[{ "In order for a formula in CNF to be a tautology, every single clause must \ be a tautology. \nBut a clause is a tautology only if it contains a literal \ ", Cell[BoxData[ \(TraditionalForm\`x\)]], " and its negation ", Cell[BoxData[ \(TraditionalForm\`\[Not] x\)]], ": otherwise one can always construct a truth assignment that will make the \ given clause false. " }], "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Part b", "Subsubsection", CellTags->"c:112"], Cell[TextData[{ "The problem with Fred's bright idea is that transforming a formula into \ CNF has a computational cost. In fact, when we push an OR's down past an \ AND, the size of the formula more or less doubles:\n\n\t", Cell[BoxData[ \(TraditionalForm\`p\ \[Or] \ \((q\ \[And] \ r)\)\ \[LongRightArrow]\ \ \((p\ \[Or] \ q)\)\ \[And] \ \((p\ \[Or] \ r)\)\)]], ".\n\t\nThis can lead to catastrophic computation time for the conversion \ -- though, once we have the equivalent CNF, it would indeed be easy to check \ for tautology. \n\nThe patent office will add Fred to it's list of Circle \ Squarers and other assorted crackpots. " }], "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Normal Forms", "Section", Evaluatable->False, AspectRatioFixed->True, CellTags->"c:113"], Cell[CellGroupData[{ Cell["Task", "Subsubsection", CellTags->"c:114"], Cell["\<\ Convert each of the following formulae into NNF (negation normal \ form), CNF (conjuntive normal form) and DNF (disjunctive normal form). Make \ sure to simplify whenever possible, so the expressions remain short. Also, in \ your solution, show some intermediate steps, not just the final result.\ \>", \ "Text"], Cell[TextData[{ "(a) ", Cell[BoxData[ \(TraditionalForm\`\[Not] \((\((p \[Or] q)\) \[And] \ \((r \[Or] s \[Or] t)\))\)\)]] }], "Text"], Cell[TextData[{ "(b) ", Cell[BoxData[ \(TraditionalForm\`\[Not] \((\((p \[And] q)\) \[Or] \[Not] \ \((r \[And] s \[And] t)\))\)\)]] }], "Text"], Cell[TextData[{ "(c) ", Cell[BoxData[ \(TraditionalForm\`\((\((p \[Or] s)\) \[Or] \((q \[Implies] p)\))\)\ \[And] \ \((p \[Implies] \((q\ \[Implies] s)\))\)\)]] }], "Text"], Cell[TextData[{ "(d) ", Cell[BoxData[ \(TraditionalForm\`\[Not] \ \((p \[And] q\ \[And] \ \((\((\[Not] \ \((p \[And] r \[And] t)\)\ )\) \[Or] s \[Or] p)\))\)\)]] }], "Text"], Cell["\<\ To simplify typing, you can use \t&\tfor \[And] \t|\tfor \[Or] \t!\tfor \[Not], just like the bitwise operators in C and C++. \ \>", "Text"] }, Closed]], Cell[CellGroupData[{ Cell["Solution", "Subsection", CellTags->"c:115"], Cell["A little conversion and pretty-printing routine:", "Text"], Cell[BoxData[ \(nforms[ fml_]\ := \ \[IndentingNewLine]Module[\ {nnf, cnf, dnf}, \ \[IndentingNewLine]\t\tnnf\ = \ NNF[fml]; \[IndentingNewLine]\t\tcnf\ = \ ToCNF[nnf]; \[IndentingNewLine]\t\tdnf\ = \ ToDNF[nnf]; \[IndentingNewLine]\t\t\({{"\", fml}, {"\", nnf}, {"\", cnf}, {"\", dnf}}\ \ // \ TableForm\)\ // \ TraditionalForm\[IndentingNewLine]]\)], "Input"], Cell[CellGroupData[{ Cell["Part a", "Subsubsection", CellTags->"c:116"], Cell["The NNF is already DNF, but CNF is long.", "Text"], Cell[BoxData[ \(nforms[\(! And[Or[p, q], Or[r, s, t]]\)]\)], "Input"] }, Closed]], Cell[CellGroupData[{ Cell["Part b", "Subsubsection", CellTags->"c:117"], Cell[BoxData[ \(nforms[\(! Or[And[p, q], \(! And[r, s, t]\)]\)]\)], "Input"] }, Closed]], Cell[CellGroupData[{ Cell["Part c", "Subsubsection", CellTags->"c:118"], Cell[BoxData[ \(nforms[\((p || s || Implies[q, p])\) && Implies[p, Implies[q, s]]]\)], "Input"] }, Closed]], Cell[CellGroupData[{ Cell["Part d", "Subsubsection", CellTags->"c:119"], Cell[BoxData[ \(nforms[\(! And[p, q, Or[p, r, s, Not[And[p, r, t]]]]\)]\)], "Input"] }, Closed]] }, Closed]] }, Closed]] }, Open ]] }, FrontEndVersion->"5.0 for X", ScreenRectangle->{{0, 1280}, {0, 1024}}, WindowSize->{1012, 768}, WindowMargins->{{Automatic, 1}, {Automatic, 0}}, PrintingStartingPageNumber->111, Magnification->1.5, StyleDefinitions -> "Default.nb" ] (******************************************************************* Cached data follows. If you edit this Notebook file directly, not using Mathematica, you must remove the line containing CacheID at the top of the file. The cache data will then be recreated when you save this file from within Mathematica. *******************************************************************) (*CellTagsOutline CellTagsIndex->{ "c:1"->{ Cell[1822, 55, 41, 1, 145, "Title", CellTags->"c:1"]}, "c:2"->{ Cell[1888, 60, 97, 3, 111, "Section", Evaluatable->False, CellTags->"c:2"]}, "c:3"->{ Cell[2010, 67, 97, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:3"]}, "c:4"->{ Cell[2667, 91, 136, 5, 69, "Subsection", Evaluatable->False, CellTags->"c:4"]}, "c:5"->{ Cell[4376, 154, 98, 3, 64, "Section", Evaluatable->False, CellTags->"c:5"]}, "c:6"->{ Cell[4499, 161, 48, 1, 39, "Subsubsection", CellTags->"c:6"]}, "c:7"->{ Cell[5035, 180, 49, 1, 58, "Subsection", CellTags->"c:7"]}, "c:8"->{ Cell[5109, 185, 50, 1, 39, "Subsubsection", CellTags->"c:8"]}, "c:9"->{ Cell[5887, 212, 50, 1, 28, "Subsubsection", CellTags->"c:9"]}, "c:10"->{ Cell[7082, 251, 92, 3, 64, "Section", Evaluatable->False, CellTags->"c:10"]}, "c:11"->{ Cell[7199, 258, 55, 1, 39, "Subsubsection", CellTags->"c:11"]}, "c:12"->{ Cell[7797, 278, 49, 1, 39, "Subsubsection", CellTags->"c:12"]}, "c:13"->{ Cell[8147, 292, 137, 5, 69, "Subsection", Evaluatable->False, CellTags->"c:13"]}, "c:14"->{ Cell[9500, 340, 56, 1, 64, "Section", CellTags->"c:14"]}, "c:15"->{ Cell[9581, 345, 55, 1, 39, "Subsubsection", CellTags->"c:15"]}, "c:16"->{ Cell[10193, 363, 49, 1, 39, "Subsubsection", CellTags->"c:16"]}, "c:17"->{ Cell[11543, 405, 49, 1, 39, "Subsubsection", CellTags->"c:17"]}, "c:18"->{ Cell[12183, 430, 53, 1, 39, "Subsubsection", CellTags->"c:18"]}, "c:19"->{ Cell[18672, 679, 97, 3, 64, "Section", Evaluatable->False, CellTags->"c:19"]}, "c:20"->{ Cell[18794, 686, 55, 1, 39, "Subsubsection", CellTags->"c:20"]}, "c:21"->{ Cell[19708, 713, 49, 1, 28, "Subsubsection", CellTags->"c:21"]}, "c:22"->{ Cell[20740, 751, 137, 5, 55, "Subsection", Evaluatable->False, CellTags->"c:22"]}, "c:23"->{ Cell[23274, 845, 106, 3, 64, "Section", Evaluatable->False, CellTags->"c:23"]}, "c:24"->{ Cell[23405, 852, 49, 1, 70, "Subsubsection", CellTags->"c:24"]}, "c:25"->{ Cell[24385, 882, 50, 1, 70, "Subsection", CellTags->"c:25"]}, "c:26"->{ Cell[26136, 955, 103, 3, 64, "Section", Evaluatable->False, CellTags->"c:26"]}, "c:27"->{ Cell[26264, 962, 55, 1, 70, "Subsubsection", CellTags->"c:27"]}, "c:28"->{ Cell[27444, 992, 49, 1, 70, "Subsubsection", CellTags->"c:28"]}, "c:29"->{ Cell[27675, 1003, 50, 1, 70, "Subsection", CellTags->"c:29"]}, "c:30"->{ Cell[28266, 1023, 103, 3, 64, "Section", Evaluatable->False, CellTags->"c:30"]}, "c:31"->{ Cell[28394, 1030, 103, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:31"]}, "c:32"->{ Cell[29423, 1056, 97, 3, 28, "Subsubsection", Evaluatable->False, CellTags->"c:32"]}, "c:33"->{ Cell[29753, 1070, 97, 3, 28, "Subsubsection", Evaluatable->False, CellTags->"c:33"]}, "c:34"->{ Cell[30057, 1084, 98, 3, 44, "Subsection", Evaluatable->False, CellTags->"c:34"]}, "c:35"->{ Cell[35216, 1222, 98, 3, 44, "Subsection", Evaluatable->False, CellTags->"c:35"]}, "c:36"->{ Cell[38174, 1330, 102, 3, 64, "Section", Evaluatable->False, CellTags->"c:36"]}, "c:37"->{ Cell[38301, 1337, 82, 1, 39, "Subsubsection", CellTags->"c:37"]}, "c:38"->{ Cell[39961, 1374, 103, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:38"]}, "c:39"->{ Cell[42179, 1442, 97, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:39"]}, "c:40"->{ Cell[42857, 1465, 49, 1, 28, "Subsubsection", CellTags->"c:40"]}, "c:41"->{ Cell[43267, 1485, 100, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:41"]}, "c:42"->{ Cell[43929, 1508, 137, 5, 55, "Subsection", Evaluatable->False, CellTags->"c:42"]}, "c:43"->{ Cell[44091, 1517, 51, 1, 39, "Subsubsection", CellTags->"c:43"]}, "c:44"->{ Cell[45325, 1559, 51, 1, 28, "Subsubsection", CellTags->"c:44"]}, "c:45"->{ Cell[46394, 1595, 51, 1, 28, "Subsubsection", CellTags->"c:45"]}, "c:46"->{ Cell[49092, 1691, 135, 4, 64, "Section", Evaluatable->False, PageBreakAbove->True, CellTags->"c:46"]}, "c:47"->{ Cell[49252, 1699, 55, 1, 39, "Subsubsection", CellTags->"c:47"]}, "c:48"->{ Cell[50141, 1721, 49, 1, 28, "Subsubsection", CellTags->"c:48"]}, "c:49"->{ Cell[50329, 1732, 82, 2, 44, "Subsection", CellTags->"c:49"]}, "c:50"->{ Cell[50436, 1738, 56, 1, 39, "Subsubsection", CellTags->"c:50"]}, "c:51"->{ Cell[55355, 1893, 56, 1, 39, "Subsubsection", CellTags->"c:51"]}, "c:52"->{ Cell[56845, 1938, 50, 1, 39, "Subsubsection", CellTags->"c:52"]}, "c:53"->{ Cell[58698, 1990, 104, 3, 64, "Section", Evaluatable->False, CellTags->"c:53"]}, "c:54"->{ Cell[58827, 1997, 55, 1, 70, "Subsubsection", CellTags->"c:54"]}, "c:55"->{ Cell[59176, 2011, 49, 1, 70, "Subsubsection", CellTags->"c:55"]}, "c:56"->{ Cell[60467, 2047, 53, 1, 70, "Subsubsection", CellTags->"c:56"]}, "c:57"->{ Cell[62817, 2112, 50, 1, 70, "Subsection", CellTags->"c:57"]}, "c:58"->{ Cell[62892, 2117, 51, 1, 70, "Subsubsection", CellTags->"c:58"]}, "c:59"->{ Cell[64208, 2153, 51, 1, 70, "Subsubsection", CellTags->"c:59"]}, "c:60"->{ Cell[64837, 2173, 51, 1, 70, "Subsubsection", CellTags->"c:60"]}, "c:61"->{ Cell[67293, 2235, 51, 1, 70, "Subsubsection", CellTags->"c:61"]}, "c:62"->{ Cell[68750, 2272, 51, 1, 70, "Subsubsection", CellTags->"c:62"]}, "c:63"->{ Cell[69323, 2291, 51, 1, 70, "Subsubsection", CellTags->"c:63"]}, "c:64"->{ Cell[69874, 2309, 104, 3, 64, "Section", Evaluatable->False, CellTags->"c:64"]}, "c:65"->{ Cell[70003, 2316, 55, 1, 70, "Subsubsection", CellTags->"c:65"]}, "c:66"->{ Cell[71034, 2340, 49, 1, 70, "Subsubsection", CellTags->"c:66"]}, "c:67"->{ Cell[72504, 2388, 50, 1, 70, "Subsection", CellTags->"c:67"]}, "c:68"->{ Cell[77426, 2534, 98, 3, 64, "Section", Evaluatable->False, CellTags->"c:68"]}, "c:69"->{ Cell[77549, 2541, 49, 1, 70, "Subsubsection", CellTags->"c:69"]}, "c:70"->{ Cell[78451, 2570, 137, 5, 70, "Subsection", Evaluatable->False, CellTags->"c:70"]}, "c:71"->{ Cell[78613, 2579, 51, 1, 70, "Subsubsection", CellTags->"c:71"]}, "c:72"->{ Cell[79069, 2597, 51, 1, 70, "Subsubsection", CellTags->"c:72"]}, "c:73"->{ Cell[79636, 2622, 51, 1, 70, "Subsubsection", CellTags->"c:73"]}, "c:74"->{ Cell[80134, 2642, 113, 3, 64, "Section", Evaluatable->False, CellTags->"c:74"]}, "c:75"->{ Cell[80272, 2649, 49, 1, 70, "Subsubsection", CellTags->"c:75"]}, "c:76"->{ Cell[81213, 2676, 137, 5, 70, "Subsection", Evaluatable->False, CellTags->"c:76"]}, "c:77"->{ Cell[81681, 2693, 73, 1, 70, "Subsubsection", CellTags->"c:77"]}, "c:78"->{ Cell[82601, 2715, 78, 1, 70, "Subsubsection", CellTags->"c:78"]}, "c:79"->{ Cell[83121, 2733, 54, 1, 70, "Subsubsection", CellTags->"c:79"]}, "c:81"->{ Cell[86741, 2836, 112, 3, 64, "Section", Evaluatable->False, CellTags->"c:81"]}, "c:82"->{ Cell[86878, 2843, 55, 1, 70, "Subsubsection", CellTags->"c:82"]}, "c:83"->{ Cell[87793, 2876, 49, 1, 70, "Subsubsection", CellTags->"c:83"]}, "c:84"->{ Cell[89132, 2923, 137, 5, 70, "Subsection", Evaluatable->False, CellTags->"c:84"]}, "c:85"->{ Cell[89294, 2932, 60, 1, 70, "Subsubsection", CellTags->"c:85"]}, "c:86"->{ Cell[90255, 2960, 60, 1, 70, "Subsubsection", CellTags->"c:86"]}, "c:87"->{ Cell[91303, 2983, 60, 1, 70, "Subsubsection", CellTags->"c:87"]}, "c:88"->{ Cell[91749, 3000, 154, 4, 64, "Section", Evaluatable->False, CellTags->"c:88"]}, "c:89"->{ Cell[91928, 3008, 49, 1, 39, "Subsubsection", CellTags->"c:89"]}, "c:90"->{ Cell[93367, 3051, 137, 5, 69, "Subsection", Evaluatable->False, CellTags->"c:90"]}, "c:91"->{ Cell[93529, 3060, 51, 1, 39, "Subsubsection", CellTags->"c:91"]}, "c:92"->{ Cell[93684, 3068, 51, 1, 28, "Subsubsection", CellTags->"c:92"]}, "c:93"->{ Cell[93920, 3079, 51, 1, 28, "Subsubsection", CellTags->"c:93"]}, "c:94"->{ Cell[94109, 3090, 51, 1, 28, "Subsubsection", CellTags->"c:94"]}, "c:95"->{ Cell[94624, 3112, 99, 3, 64, "Section", Evaluatable->False, CellTags->"c:95"]}, "c:96"->{ Cell[94748, 3119, 103, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:96"]}, "c:97"->{ Cell[98399, 3234, 49, 1, 39, "Subsubsection", CellTags->"c:97"]}, "c:98"->{ Cell[99278, 3260, 137, 5, 69, "Subsection", Evaluatable->False, CellTags->"c:98"]}, "c:99"->{ Cell[99440, 3269, 51, 1, 39, "Subsubsection", CellTags->"c:99"]}, "c:100"->{ Cell[100877, 3321, 52, 1, 39, "Subsubsection", CellTags->"c:100"]}, "c:101"->{ Cell[102651, 3393, 121, 4, 64, "Section", Evaluatable->False, PageBreakAbove->True, CellTags->"c:101"]}, "c:102"->{ Cell[102797, 3401, 56, 1, 39, "Subsubsection", CellTags->"c:102"]}, "c:103"->{ Cell[103308, 3418, 50, 1, 28, "Subsubsection", CellTags->"c:103"]}, "c:104"->{ Cell[103536, 3430, 83, 2, 44, "Subsection", CellTags->"c:104"]}, "c:105"->{ Cell[103644, 3436, 52, 1, 39, "Subsubsection", CellTags->"c:105"]}, "c:106"->{ Cell[105382, 3495, 52, 1, 28, "Subsubsection", CellTags->"c:106"]}, "c:107"->{ Cell[107745, 3578, 105, 3, 64, "Section", Evaluatable->False, CellTags->"c:107"]}, "c:108"->{ Cell[107875, 3585, 56, 1, 39, "Subsubsection", CellTags->"c:108"]}, "c:109"->{ Cell[108538, 3603, 50, 1, 39, "Subsubsection", CellTags->"c:109"]}, "c:110"->{ Cell[109197, 3627, 51, 1, 58, "Subsection", CellTags->"c:110"]}, "c:111"->{ Cell[109273, 3632, 52, 1, 39, "Subsubsection", CellTags->"c:111"]}, "c:112"->{ Cell[109781, 3651, 52, 1, 39, "Subsubsection", CellTags->"c:112"]}, "c:113"->{ Cell[110597, 3673, 100, 3, 64, "Section", Evaluatable->False, CellTags->"c:113"]}, "c:114"->{ Cell[110722, 3680, 50, 1, 39, "Subsubsection", CellTags->"c:114"]}, "c:115"->{ Cell[112077, 3732, 51, 1, 44, "Subsection", CellTags->"c:115"]}, "c:116"->{ Cell[112719, 3750, 52, 1, 39, "Subsubsection", CellTags->"c:116"]}, "c:117"->{ Cell[112943, 3761, 52, 1, 39, "Subsubsection", CellTags->"c:117"]}, "c:118"->{ Cell[113115, 3770, 52, 1, 39, "Subsubsection", CellTags->"c:118"]}, "c:119"->{ Cell[113315, 3780, 52, 1, 28, "Subsubsection", CellTags->"c:119"]} } *) (*CellTagsIndex CellTagsIndex->{ {"c:1", 114170, 3808}, {"c:2", 114246, 3811}, {"c:3", 114350, 3815}, {"c:4", 114459, 3819}, {"c:5", 114566, 3823}, {"c:6", 114670, 3827}, {"c:7", 114754, 3830}, {"c:8", 114835, 3833}, {"c:9", 114919, 3836}, {"c:10", 115004, 3839}, {"c:11", 115110, 3843}, {"c:12", 115196, 3846}, {"c:13", 115282, 3849}, {"c:14", 115392, 3853}, {"c:15", 115472, 3856}, {"c:16", 115558, 3859}, {"c:17", 115645, 3862}, {"c:18", 115732, 3865}, {"c:19", 115819, 3868}, {"c:20", 115926, 3872}, {"c:21", 116013, 3875}, {"c:22", 116100, 3878}, {"c:23", 116211, 3882}, {"c:24", 116319, 3886}, {"c:25", 116406, 3889}, {"c:26", 116490, 3892}, {"c:27", 116598, 3896}, {"c:28", 116685, 3899}, {"c:29", 116772, 3902}, {"c:30", 116857, 3905}, {"c:31", 116966, 3909}, {"c:32", 117081, 3913}, {"c:33", 117195, 3917}, {"c:34", 117309, 3921}, {"c:35", 117420, 3925}, {"c:36", 117531, 3929}, {"c:37", 117640, 3933}, {"c:38", 117728, 3936}, {"c:39", 117843, 3940}, {"c:40", 117957, 3944}, {"c:41", 118045, 3947}, {"c:42", 118160, 3951}, {"c:43", 118272, 3955}, {"c:44", 118360, 3958}, {"c:45", 118448, 3961}, {"c:46", 118536, 3964}, {"c:47", 118673, 3969}, {"c:48", 118761, 3972}, {"c:49", 118849, 3975}, {"c:50", 118934, 3978}, {"c:51", 119022, 3981}, {"c:52", 119110, 3984}, {"c:53", 119198, 3987}, {"c:54", 119307, 3991}, {"c:55", 119395, 3994}, {"c:56", 119483, 3997}, {"c:57", 119571, 4000}, {"c:58", 119656, 4003}, {"c:59", 119744, 4006}, {"c:60", 119832, 4009}, {"c:61", 119920, 4012}, {"c:62", 120008, 4015}, {"c:63", 120096, 4018}, {"c:64", 120184, 4021}, {"c:65", 120293, 4025}, {"c:66", 120381, 4028}, {"c:67", 120469, 4031}, {"c:68", 120554, 4034}, {"c:69", 120662, 4038}, {"c:70", 120750, 4041}, {"c:71", 120862, 4045}, {"c:72", 120950, 4048}, {"c:73", 121038, 4051}, {"c:74", 121126, 4054}, {"c:75", 121235, 4058}, {"c:76", 121323, 4061}, {"c:77", 121435, 4065}, {"c:78", 121523, 4068}, {"c:79", 121611, 4071}, {"c:81", 121699, 4074}, {"c:82", 121808, 4078}, {"c:83", 121896, 4081}, {"c:84", 121984, 4084}, {"c:85", 122096, 4088}, {"c:86", 122184, 4091}, {"c:87", 122272, 4094}, {"c:88", 122360, 4097}, {"c:89", 122469, 4101}, {"c:90", 122557, 4104}, {"c:91", 122669, 4108}, {"c:92", 122757, 4111}, {"c:93", 122845, 4114}, {"c:94", 122933, 4117}, {"c:95", 123021, 4120}, {"c:96", 123129, 4124}, {"c:97", 123244, 4128}, {"c:98", 123332, 4131}, {"c:99", 123444, 4135}, {"c:100", 123533, 4138}, {"c:101", 123624, 4141}, {"c:102", 123764, 4146}, {"c:103", 123855, 4149}, {"c:104", 123946, 4152}, {"c:105", 124034, 4155}, {"c:106", 124125, 4158}, {"c:107", 124216, 4161}, {"c:108", 124328, 4165}, {"c:109", 124419, 4168}, {"c:110", 124510, 4171}, {"c:111", 124598, 4174}, {"c:112", 124689, 4177}, {"c:113", 124780, 4180}, {"c:114", 124892, 4184}, {"c:115", 124983, 4187}, {"c:116", 125071, 4190}, {"c:117", 125162, 4193}, {"c:118", 125253, 4196}, {"c:119", 125344, 4199} } *) (*NotebookFileOutline Notebook[{ Cell[1754, 51, 43, 0, 46, "Text"], Cell[CellGroupData[{ Cell[1822, 55, 41, 1, 145, "Title", CellTags->"c:1"], Cell[CellGroupData[{ Cell[1888, 60, 97, 3, 111, "Section", Evaluatable->False, CellTags->"c:2"], Cell[CellGroupData[{ Cell[2010, 67, 97, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:3"], Cell[2110, 72, 520, 14, 196, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[2667, 91, 136, 5, 69, "Subsection", Evaluatable->False, CellTags->"c:4"], Cell[2806, 98, 399, 12, 96, "Text", Evaluatable->False], Cell[3208, 112, 535, 17, 96, "Text", Evaluatable->False], Cell[3746, 131, 581, 17, 96, "Text", Evaluatable->False] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[4376, 154, 98, 3, 64, "Section", Evaluatable->False, CellTags->"c:5"], Cell[CellGroupData[{ Cell[4499, 161, 48, 1, 39, "Subsubsection", CellTags->"c:6"], Cell[4550, 164, 448, 11, 171, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[5035, 180, 49, 1, 58, "Subsection", CellTags->"c:7"], Cell[CellGroupData[{ Cell[5109, 185, 50, 1, 39, "Subsubsection", CellTags->"c:8"], Cell[5162, 188, 688, 19, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[5887, 212, 50, 1, 28, "Subsubsection", CellTags->"c:9"], Cell[5940, 215, 1081, 29, 70, "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[7082, 251, 92, 3, 64, "Section", Evaluatable->False, CellTags->"c:10"], Cell[CellGroupData[{ Cell[7199, 258, 55, 1, 39, "Subsubsection", CellTags->"c:11"], Cell[7257, 261, 503, 12, 246, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[7797, 278, 49, 1, 39, "Subsubsection", CellTags->"c:12"], Cell[7849, 281, 261, 6, 121, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[8147, 292, 137, 5, 69, "Subsection", Evaluatable->False, CellTags->"c:13"], Cell[8287, 299, 558, 11, 196, "Text"], Cell[8848, 312, 194, 5, 46, "Text"], Cell[9045, 319, 101, 3, 58, "Input"], Cell[9149, 324, 138, 3, 58, "Input"], Cell[9290, 329, 111, 3, 58, "Input"], Cell[9404, 334, 47, 0, 38, "Input"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[9500, 340, 56, 1, 64, "Section", CellTags->"c:14"], Cell[CellGroupData[{ Cell[9581, 345, 55, 1, 39, "Subsubsection", CellTags->"c:15"], Cell[9639, 348, 517, 10, 171, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[10193, 363, 49, 1, 39, "Subsubsection", CellTags->"c:16"], Cell[10245, 366, 1261, 34, 371, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[11543, 405, 49, 1, 39, "Subsubsection", CellTags->"c:17"], Cell[11595, 408, 551, 17, 171, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[12183, 430, 53, 1, 39, "Subsubsection", CellTags->"c:18"], Cell[12239, 433, 65, 0, 46, "Text"], Cell[12307, 435, 777, 25, 146, "Text"], Cell[13087, 462, 224, 5, 62, "Input"], Cell[13314, 469, 152, 5, 46, "Text"], Cell[13469, 476, 28, 0, 38, "Input"], Cell[13500, 478, 103, 3, 46, "Text"], Cell[13606, 483, 46, 3, 58, "Input"], Cell[13655, 488, 1382, 41, 221, "Text"], Cell[15040, 531, 85, 1, 39, "Input"], Cell[15128, 534, 112, 2, 62, "Input"], Cell[15243, 538, 639, 18, 146, "Text"], Cell[15885, 558, 86, 1, 39, "Input"], Cell[15974, 561, 77, 3, 58, "Input"], Cell[16054, 566, 49, 0, 46, "Text"], Cell[16106, 568, 50, 3, 58, "Input"], Cell[16159, 573, 564, 16, 146, "Text"], Cell[16726, 591, 169, 3, 85, "Input"], Cell[16898, 596, 161, 5, 96, "Text"], Cell[17062, 603, 29, 0, 38, "Input"], Cell[17094, 605, 25, 0, 38, "Input"], Cell[17122, 607, 37, 0, 38, "Input"], Cell[17162, 609, 585, 20, 71, "Text"], Cell[17750, 631, 82, 3, 58, "Input"], Cell[17835, 636, 214, 8, 46, "Text"], Cell[18052, 646, 66, 4, 78, "Input"], Cell[18121, 652, 178, 8, 46, "Text"], Cell[18302, 662, 85, 1, 39, "Input"], Cell[18390, 665, 233, 8, 96, "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[18672, 679, 97, 3, 64, "Section", Evaluatable->False, CellTags->"c:19"], Cell[CellGroupData[{ Cell[18794, 686, 55, 1, 39, "Subsubsection", CellTags->"c:20"], Cell[18852, 689, 819, 19, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[19708, 713, 49, 1, 28, "Subsubsection", CellTags->"c:21"], Cell[19760, 716, 943, 30, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[20740, 751, 137, 5, 55, "Subsection", Evaluatable->False, CellTags->"c:22"], Cell[20880, 758, 1364, 38, 70, "Text"], Cell[22247, 798, 215, 6, 70, "Text"], Cell[22465, 806, 184, 10, 70, "Input"], Cell[22652, 818, 220, 5, 70, "Text"], Cell[22875, 825, 38, 0, 70, "Input"], Cell[22916, 827, 140, 5, 70, "Text"], Cell[23059, 834, 29, 0, 70, "Input"], Cell[23091, 836, 134, 3, 70, "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[23274, 845, 106, 3, 64, "Section", Evaluatable->False, CellTags->"c:23"], Cell[CellGroupData[{ Cell[23405, 852, 49, 1, 70, "Subsubsection", CellTags->"c:24"], Cell[23457, 855, 891, 22, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[24385, 882, 50, 1, 70, "Subsection", CellTags->"c:25"], Cell[24438, 885, 872, 26, 70, "Text"], Cell[25313, 913, 121, 4, 70, "Input"], Cell[25437, 919, 188, 4, 70, "Text"], Cell[25628, 925, 68, 0, 70, "Input"], Cell[25699, 927, 31, 0, 70, "Text"], Cell[25733, 929, 91, 3, 70, "Input"], Cell[25827, 934, 61, 3, 70, "Text"], Cell[25891, 939, 91, 3, 70, "Input"], Cell[25985, 944, 102, 5, 70, "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[26136, 955, 103, 3, 64, "Section", Evaluatable->False, CellTags->"c:26"], Cell[CellGroupData[{ Cell[26264, 962, 55, 1, 70, "Subsubsection", CellTags->"c:27"], Cell[26322, 965, 1085, 22, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[27444, 992, 49, 1, 70, "Subsubsection", CellTags->"c:28"], Cell[27496, 995, 142, 3, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[27675, 1003, 50, 1, 70, "Subsection", CellTags->"c:29"], Cell[27728, 1006, 489, 11, 70, "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[28266, 1023, 103, 3, 64, "Section", Evaluatable->False, CellTags->"c:30"], Cell[CellGroupData[{ Cell[28394, 1030, 103, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:31"], Cell[28500, 1035, 886, 16, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[29423, 1056, 97, 3, 28, "Subsubsection", Evaluatable->False, CellTags->"c:32"], Cell[29523, 1061, 193, 4, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[29753, 1070, 97, 3, 28, "Subsubsection", Evaluatable->False, CellTags->"c:33"], Cell[29853, 1075, 167, 4, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[30057, 1084, 98, 3, 44, "Subsection", Evaluatable->False, CellTags->"c:34"], Cell[30158, 1089, 3679, 96, 946, "Text", Evaluatable->False], Cell[33840, 1187, 1339, 30, 548, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[35216, 1222, 98, 3, 44, "Subsection", Evaluatable->False, CellTags->"c:35"], Cell[35317, 1227, 111, 2, 62, "Input"], Cell[35431, 1231, 247, 5, 62, "Input"], Cell[35681, 1238, 59, 1, 39, "Input"], Cell[35743, 1241, 58, 1, 39, "Input"], Cell[35804, 1244, 387, 7, 177, "Input"], Cell[36194, 1253, 93, 1, 39, "Input"], Cell[36290, 1256, 77, 1, 39, "Input"], Cell[36370, 1259, 46, 1, 39, "Input"], Cell[36419, 1262, 60, 1, 39, "Input"], Cell[36482, 1265, 133, 3, 85, "Input"], Cell[36618, 1270, 60, 0, 46, "Text"], Cell[36681, 1272, 73, 1, 39, "Input"], Cell[36757, 1275, 60, 1, 39, "Input"], Cell[36820, 1278, 78, 1, 39, "Input"], Cell[36901, 1281, 132, 3, 39, "Input"], Cell[37036, 1286, 53, 0, 46, "Text"], Cell[37092, 1288, 82, 1, 39, "Input"], Cell[37177, 1291, 69, 1, 39, "Input"], Cell[37249, 1294, 176, 4, 62, "Input"], Cell[37428, 1300, 63, 1, 39, "Input"], Cell[37494, 1303, 74, 2, 62, "Input"], Cell[37571, 1307, 75, 1, 39, "Input"], Cell[37649, 1310, 82, 1, 39, "Input"], Cell[37734, 1313, 74, 2, 62, "Input"], Cell[37811, 1317, 314, 7, 171, "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[38174, 1330, 102, 3, 64, "Section", Evaluatable->False, CellTags->"c:36"], Cell[CellGroupData[{ Cell[38301, 1337, 82, 1, 39, "Subsubsection", CellTags->"c:37"], Cell[38386, 1340, 1538, 29, 567, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[39961, 1374, 103, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:38"], Cell[40067, 1379, 1355, 23, 471, "Text", Evaluatable->False], Cell[41425, 1404, 88, 4, 78, "Input"], Cell[41516, 1410, 125, 4, 71, "Text"], Cell[41644, 1416, 84, 4, 78, "Input"], Cell[41731, 1422, 57, 0, 46, "Text"], Cell[41791, 1424, 84, 4, 78, "Input"], Cell[41878, 1430, 264, 7, 71, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[42179, 1442, 97, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:39"], Cell[42279, 1447, 541, 13, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[42857, 1465, 49, 1, 28, "Subsubsection", CellTags->"c:40"], Cell[42909, 1468, 225, 7, 96, "Text", Evaluatable->False], Cell[43137, 1477, 93, 3, 58, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[43267, 1485, 100, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:41"], Cell[43370, 1490, 522, 13, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[43929, 1508, 137, 5, 55, "Subsection", Evaluatable->False, CellTags->"c:42"], Cell[CellGroupData[{ Cell[44091, 1517, 51, 1, 39, "Subsubsection", CellTags->"c:43"], Cell[44145, 1520, 1143, 34, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[45325, 1559, 51, 1, 28, "Subsubsection", CellTags->"c:44"], Cell[45379, 1562, 978, 28, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[46394, 1595, 51, 1, 28, "Subsubsection", CellTags->"c:45"], Cell[46448, 1598, 1575, 42, 271, "Text", Evaluatable->False], Cell[48026, 1642, 167, 6, 118, "Input"], Cell[48196, 1650, 322, 10, 71, "Text", Evaluatable->False], Cell[48521, 1662, 167, 6, 118, "Input"], Cell[48691, 1670, 196, 7, 46, "Text", Evaluatable->False], Cell[48890, 1679, 141, 5, 98, "Input"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[49092, 1691, 135, 4, 64, "Section", Evaluatable->False, PageBreakAbove->True, CellTags->"c:46"], Cell[CellGroupData[{ Cell[49252, 1699, 55, 1, 39, "Subsubsection", CellTags->"c:47"], Cell[49310, 1702, 794, 14, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[50141, 1721, 49, 1, 28, "Subsubsection", CellTags->"c:48"], Cell[50193, 1724, 99, 3, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[50329, 1732, 82, 2, 44, "Subsection", CellTags->"c:49"], Cell[CellGroupData[{ Cell[50436, 1738, 56, 1, 39, "Subsubsection", CellTags->"c:50"], Cell[50495, 1741, 2341, 58, 646, "Text"], Cell[52839, 1801, 422, 7, 154, "Input"], Cell[53264, 1810, 23, 0, 46, "Text"], Cell[53290, 1812, 56, 3, 58, "Input"], Cell[53349, 1817, 383, 8, 96, "Text"], Cell[53735, 1827, 343, 7, 131, "Input"], Cell[54081, 1836, 37, 0, 46, "Text"], Cell[54121, 1838, 77, 6, 118, "Input"], Cell[54201, 1846, 224, 6, 121, "Text"], Cell[54428, 1854, 86, 1, 39, "Input"], Cell[54517, 1857, 44, 0, 46, "Text"], Cell[54564, 1859, 72, 1, 39, "Input"], Cell[54639, 1862, 34, 0, 46, "Text"], Cell[54676, 1864, 55, 0, 38, "Input"], Cell[54734, 1866, 33, 0, 38, "Input"], Cell[54770, 1868, 148, 3, 71, "Text"], Cell[54921, 1873, 113, 2, 39, "Input"], Cell[55037, 1877, 48, 1, 39, "Input"], Cell[55088, 1880, 75, 1, 39, "Input"], Cell[55166, 1883, 72, 0, 46, "Text"], Cell[55241, 1885, 77, 3, 58, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[55355, 1893, 56, 1, 39, "Subsubsection", CellTags->"c:51"], Cell[55414, 1896, 264, 7, 71, "Text"], Cell[55681, 1905, 201, 4, 108, "Input"], Cell[55885, 1911, 134, 3, 46, "Text"], Cell[56022, 1916, 137, 2, 39, "Input"], Cell[56162, 1920, 646, 13, 271, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[56845, 1938, 50, 1, 39, "Subsubsection", CellTags->"c:52"], Cell[56898, 1941, 1739, 42, 70, "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[58698, 1990, 104, 3, 64, "Section", Evaluatable->False, CellTags->"c:53"], Cell[CellGroupData[{ Cell[58827, 1997, 55, 1, 70, "Subsubsection", CellTags->"c:54"], Cell[58885, 2000, 254, 6, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[59176, 2011, 49, 1, 70, "Subsubsection", CellTags->"c:55"], Cell[59228, 2014, 1202, 28, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[60467, 2047, 53, 1, 70, "Subsubsection", CellTags->"c:56"], Cell[60523, 2050, 1670, 45, 70, "Text"], Cell[62196, 2097, 584, 10, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[62817, 2112, 50, 1, 70, "Subsection", CellTags->"c:57"], Cell[CellGroupData[{ Cell[62892, 2117, 51, 1, 70, "Subsubsection", CellTags->"c:58"], Cell[62946, 2120, 1225, 28, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[64208, 2153, 51, 1, 70, "Subsubsection", CellTags->"c:59"], Cell[64262, 2156, 538, 12, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[64837, 2173, 51, 1, 70, "Subsubsection", CellTags->"c:60"], Cell[64891, 2176, 2365, 54, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[67293, 2235, 51, 1, 70, "Subsubsection", CellTags->"c:61"], Cell[67347, 2238, 1366, 29, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[68750, 2272, 51, 1, 70, "Subsubsection", CellTags->"c:62"], Cell[68804, 2275, 482, 11, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[69323, 2291, 51, 1, 70, "Subsubsection", CellTags->"c:63"], Cell[69377, 2294, 436, 8, 70, "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[69874, 2309, 104, 3, 64, "Section", Evaluatable->False, CellTags->"c:64"], Cell[CellGroupData[{ Cell[70003, 2316, 55, 1, 70, "Subsubsection", CellTags->"c:65"], Cell[70061, 2319, 936, 16, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[71034, 2340, 49, 1, 70, "Subsubsection", CellTags->"c:66"], Cell[71086, 2343, 720, 14, 70, "Text"], Cell[71809, 2359, 658, 24, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[72504, 2388, 50, 1, 70, "Subsection", CellTags->"c:67"], Cell[72557, 2391, 211, 4, 70, "Text"], Cell[72771, 2397, 4318, 122, 70, "Text"], Cell[77092, 2521, 285, 7, 70, "Text"] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[77426, 2534, 98, 3, 64, "Section", Evaluatable->False, CellTags->"c:68"], Cell[CellGroupData[{ Cell[77549, 2541, 49, 1, 70, "Subsubsection", CellTags->"c:69"], Cell[77601, 2544, 813, 21, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[78451, 2570, 137, 5, 70, "Subsection", Evaluatable->False, CellTags->"c:70"], Cell[CellGroupData[{ Cell[78613, 2579, 51, 1, 70, "Subsubsection", CellTags->"c:71"], Cell[78667, 2582, 365, 10, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[79069, 2597, 51, 1, 70, "Subsubsection", CellTags->"c:72"], Cell[79123, 2600, 476, 17, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[79636, 2622, 51, 1, 70, "Subsubsection", CellTags->"c:73"], Cell[79690, 2625, 383, 10, 70, "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[80134, 2642, 113, 3, 64, "Section", Evaluatable->False, CellTags->"c:74"], Cell[CellGroupData[{ Cell[80272, 2649, 49, 1, 70, "Subsubsection", CellTags->"c:75"], Cell[80324, 2652, 852, 19, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[81213, 2676, 137, 5, 70, "Subsection", Evaluatable->False, CellTags->"c:76"], Cell[81353, 2683, 303, 6, 70, "Text"], Cell[CellGroupData[{ Cell[81681, 2693, 73, 1, 70, "Subsubsection", CellTags->"c:77"], Cell[81757, 2696, 807, 14, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[82601, 2715, 78, 1, 70, "Subsubsection", CellTags->"c:78"], Cell[82682, 2718, 402, 10, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[83121, 2733, 54, 1, 70, "Subsubsection", CellTags->"c:79"], Cell[83178, 2736, 1518, 37, 70, "Text"], Cell[84699, 2775, 300, 11, 70, "Text"], Cell[85002, 2788, 267, 10, 70, "Text"], Cell[85272, 2800, 1408, 29, 70, "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[86741, 2836, 112, 3, 64, "Section", Evaluatable->False, CellTags->"c:81"], Cell[CellGroupData[{ Cell[86878, 2843, 55, 1, 70, "Subsubsection", CellTags->"c:82"], Cell[86936, 2846, 820, 25, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[87793, 2876, 49, 1, 70, "Subsubsection", CellTags->"c:83"], Cell[87845, 2879, 953, 29, 70, "Text", Evaluatable->False], Cell[88801, 2910, 294, 8, 70, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[89132, 2923, 137, 5, 70, "Subsection", Evaluatable->False, CellTags->"c:84"], Cell[CellGroupData[{ Cell[89294, 2932, 60, 1, 70, "Subsubsection", CellTags->"c:85"], Cell[89357, 2935, 861, 20, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[90255, 2960, 60, 1, 70, "Subsubsection", CellTags->"c:86"], Cell[90318, 2963, 948, 15, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[91303, 2983, 60, 1, 70, "Subsubsection", CellTags->"c:87"], Cell[91366, 2986, 322, 7, 70, "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[91749, 3000, 154, 4, 64, "Section", Evaluatable->False, CellTags->"c:88"], Cell[CellGroupData[{ Cell[91928, 3008, 49, 1, 39, "Subsubsection", CellTags->"c:89"], Cell[91980, 3011, 1306, 33, 221, "Text", Evaluatable->False], Cell[93289, 3046, 41, 0, 38, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[93367, 3051, 137, 5, 69, "Subsection", Evaluatable->False, CellTags->"c:90"], Cell[CellGroupData[{ Cell[93529, 3060, 51, 1, 39, "Subsubsection", CellTags->"c:91"], Cell[93583, 3063, 64, 0, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[93684, 3068, 51, 1, 28, "Subsubsection", CellTags->"c:92"], Cell[93738, 3071, 145, 3, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[93920, 3079, 51, 1, 28, "Subsubsection", CellTags->"c:93"], Cell[93974, 3082, 98, 3, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[94109, 3090, 51, 1, 28, "Subsubsection", CellTags->"c:94"], Cell[94163, 3093, 280, 8, 71, "Text"], Cell[94446, 3103, 117, 2, 39, "Input"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[94624, 3112, 99, 3, 64, "Section", Evaluatable->False, CellTags->"c:95"], Cell[CellGroupData[{ Cell[94748, 3119, 103, 3, 39, "Subsubsection", Evaluatable->False, CellTags->"c:96"], Cell[94854, 3124, 183, 4, 71, "Text"], Cell[95040, 3130, 359, 7, 257, "Program"], Cell[95402, 3139, 1243, 26, 321, "Text"], Cell[96648, 3167, 626, 17, 171, "Text"], Cell[97277, 3186, 562, 21, 153, "Text"], Cell[97842, 3209, 520, 20, 153, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[98399, 3234, 49, 1, 39, "Subsubsection", CellTags->"c:97"], Cell[98451, 3237, 790, 18, 171, "Text", Evaluatable->False] }, Closed]], Cell[CellGroupData[{ Cell[99278, 3260, 137, 5, 69, "Subsection", Evaluatable->False, CellTags->"c:98"], Cell[CellGroupData[{ Cell[99440, 3269, 51, 1, 39, "Subsubsection", CellTags->"c:99"], Cell[99494, 3272, 1111, 39, 397, "Text"], Cell[100608, 3313, 232, 3, 62, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[100877, 3321, 52, 1, 39, "Subsubsection", CellTags->"c:100"], Cell[100932, 3324, 376, 10, 46, "Text", Evaluatable->False], Cell[101311, 3336, 694, 25, 184, "Text", Evaluatable->False], Cell[102008, 3363, 582, 23, 190, "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[102651, 3393, 121, 4, 64, "Section", Evaluatable->False, PageBreakAbove->True, CellTags->"c:101"], Cell[CellGroupData[{ Cell[102797, 3401, 56, 1, 39, "Subsubsection", CellTags->"c:102"], Cell[102856, 3404, 415, 9, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[103308, 3418, 50, 1, 28, "Subsubsection", CellTags->"c:103"], Cell[103361, 3421, 138, 4, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[103536, 3430, 83, 2, 44, "Subsection", CellTags->"c:104"], Cell[CellGroupData[{ Cell[103644, 3436, 52, 1, 39, "Subsubsection", CellTags->"c:105"], Cell[103699, 3439, 1646, 51, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[105382, 3495, 52, 1, 28, "Subsubsection", CellTags->"c:106"], Cell[105437, 3498, 311, 6, 96, "Text"], Cell[105751, 3506, 184, 6, 118, "Input"], Cell[105938, 3514, 29, 0, 38, "Input"], Cell[105970, 3516, 30, 0, 38, "Input"], Cell[106003, 3518, 941, 21, 246, "Text"], Cell[106947, 3541, 206, 11, 218, "Input"], Cell[107156, 3554, 34, 0, 38, "Input"], Cell[107193, 3556, 32, 0, 38, "Input"], Cell[107228, 3558, 32, 0, 38, "Input"], Cell[107263, 3560, 57, 0, 38, "Input"], Cell[107323, 3562, 361, 9, 71, "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[107745, 3578, 105, 3, 64, "Section", Evaluatable->False, CellTags->"c:107"], Cell[CellGroupData[{ Cell[107875, 3585, 56, 1, 39, "Subsubsection", CellTags->"c:108"], Cell[107934, 3588, 567, 10, 171, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[108538, 3603, 50, 1, 39, "Subsubsection", CellTags->"c:109"], Cell[108591, 3606, 92, 3, 46, "Text"], Cell[108686, 3611, 474, 11, 221, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[109197, 3627, 51, 1, 58, "Subsection", CellTags->"c:110"], Cell[CellGroupData[{ Cell[109273, 3632, 52, 1, 39, "Subsubsection", CellTags->"c:111"], Cell[109328, 3635, 416, 11, 96, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[109781, 3651, 52, 1, 39, "Subsubsection", CellTags->"c:112"], Cell[109836, 3654, 700, 12, 246, "Text"] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell[110597, 3673, 100, 3, 64, "Section", Evaluatable->False, CellTags->"c:113"], Cell[CellGroupData[{ Cell[110722, 3680, 50, 1, 39, "Subsubsection", CellTags->"c:114"], Cell[110775, 3683, 323, 6, 70, "Text"], Cell[111101, 3691, 164, 5, 70, "Text"], Cell[111268, 3698, 173, 5, 70, "Text"], Cell[111444, 3705, 221, 6, 70, "Text"], Cell[111668, 3713, 217, 6, 70, "Text"], Cell[111888, 3721, 152, 6, 70, "Text"] }, Closed]], Cell[CellGroupData[{ Cell[112077, 3732, 51, 1, 44, "Subsection", CellTags->"c:115"], Cell[112131, 3735, 64, 0, 46, "Text"], Cell[112198, 3737, 496, 9, 200, "Input"], Cell[CellGroupData[{ Cell[112719, 3750, 52, 1, 39, "Subsubsection", CellTags->"c:116"], Cell[112774, 3753, 56, 0, 46, "Text"], Cell[112833, 3755, 73, 1, 39, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[112943, 3761, 52, 1, 39, "Subsubsection", CellTags->"c:117"], Cell[112998, 3764, 80, 1, 39, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[113115, 3770, 52, 1, 39, "Subsubsection", CellTags->"c:118"], Cell[113170, 3773, 108, 2, 70, "Input"] }, Closed]], Cell[CellGroupData[{ Cell[113315, 3780, 52, 1, 28, "Subsubsection", CellTags->"c:119"], Cell[113370, 3783, 88, 1, 70, "Input"] }, Closed]] }, Closed]] }, Closed]] }, Open ]] } ] *) (******************************************************************* End of Mathematica Notebook file. *******************************************************************)