a2/3.tex

   1 \section{Problem 3}
   2 \emph{The goal of this problem is to exploit the power of the recommended
   3 tools rather than elaborating the questions by hand.}
   4 \begin{enumerate}[a.]
   5         \item\emph{In mathematics, a \emph{group} is defined to be a set $G$
   6                 with an element $I\in G$, a binary operator $∗$ and a unary
   7                 operator inv satisfying.
   8                 $$x*(y*z)=(x*y)*z, x*I=x\text{ and }x*inv(x)=I,$$
   9                 for all $x,y,z\in G$. Determine whether in every group each of
  10                 the four properties
  11                 $$I*x=x, inv(inv(x))=x, inv(x)*x=I\text{ and } x*y=y*x$$
  12                 holds for all $x,y\in G$. If a property does not hold,
  13                 determine the size of the smallest finite group for which it
  14                 does not hold.}\\
  15
  16                 As found by \textsc{prover9} a proof for $I*x=x$.
  17                 \begin{lstlisting}
  18 1  I * x = x.                [goal].
  19 2  x * (y * z) = (x * y) * z.[assumption].
  20 3  (x * y) * z = x * (y * z).[copy(2),flip(a)].
  21 4  x * I = x.                [assumption].
  22 5  x * inv(x) = I.           [assumption].
  23 6  I * c1 != c1.             [deny(1)].
  24 7  x * (I * y) = x * y.      [para(4(a,1),3(a,1,1)),flip(a)].
  25 8  x * (inv(x) * y) = I * y. [para(5(a,1),3(a,1,1)),flip(a)].
  26 13 I * inv(inv(x)) = x.      [para(5(a,1),8(a,1,2)),rewrite([4(2)]),flip(a)].
  27 15 x * inv(inv(y)) = x * y.  [para(13(a,1),3(a,2,2)),rewrite([4(2)])].
  28 16 I * x = x.                [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])].
  29 17 \$F.                      [resolve(16,a,6,a)].
  30                 \end{lstlisting}
  31
  32                 As found by \textsc{prover9} a proof for $inv(inv(x))=x$.
  33                 \begin{lstlisting}
  34 1  inv(inv(x)) = x.          [goal].
  35 2  x * (y * z) = (x * y) * z.[assumption].
  36 3  (x * y) * z = x * (y * z).[copy(2),flip(a)].
  37 4  x * I = x.                [assumption]
  38 5  x * inv(x) = I.           [assumption].
  39 6  inv(inv(c1)) != c1.       [deny(1)].
  40 7  x * (I * y) = x * y.      [para(4(a,1),3(a,1,1)),flip(a)].
  41 8  x * (inv(x) * y) = I * y. [para(5(a,1),3(a,1,1)),flip(a)].
  42 13 I * inv(inv(x)) = x.      [para(5(a,1),8(a,1,2)),rewrite([4(2)]),flip(a)].
  43 15 x * inv(inv(y)) = x * y.  [para(13(a,1),3(a,2,2)),rewrite([4(2)])].
  44 16 I * x = x.                [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])].
  45 19 x * (inv(x) * y) = y.     [back_rewrite(8),rewrite([16(5)])].
  46 22 inv(inv(x)) = x.          [para(5(a,1),19(a,1,2)),rewrite([4(2)]),flip(a)].
  47 23 \$F.                      [resolve(22,a,6,a)].
  48                 \end{lstlisting}
  49
  50                 As found by \textsc{prover9} a proof for $x*inv(x)=I$.
  51                 \begin{lstlisting}
  52 1  inv(x) * x = I.           [goal].
  53 2  x * (y * z) = (x * y) * z.[assumption].
  54 3  (x * y) * z = x * (y * z).[copy(2),flip(a)].
  55 4  x * I = x.                [assumption].
  56 5  x * inv(x) = I.           [assumption].
  57 6  inv(c1) * c1 != I.        [deny(1)].
  58 7  x * (I * y) = x * y.      [para(4(a,1),3(a,1,1)),flip(a)].
  59 8  x * (inv(x) * y) = I * y. [para(5(a,1),3(a,1,1)),flip(a)].
  60 13 I * inv(inv(x)) = x.      [para(5(a,1),8(a,1,2)),rewrite([4(2)]),flip(a)].
  61 15 x * inv(inv(y)) = x * y.  [para(13(a,1),3(a,2,2)),rewrite([4(2)])].
  62 16 I * x = x.                [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])].
  63 19 x * (inv(x) * y) = y.     [back_rewrite(8),rewrite([16(5)])].
  64 22 inv(inv(x)) = x.          [para(5(a,1),19(a,1,2)),rewrite([4(2)]),flip(a)].
  65 24 inv(x) * x = I.           [para(22(a,1),5(a,1,2))].
  66 25 \$F.                      [resolve(24,a,6,a)].
  67 \end{lstlisting}
  68
  69                 \textsc{prover9} fails to find a proof for $x*y=y*x$.
  70                 Running the same file with \textsc{mace4} gives the following
  71                 counterexample.
  72
  73
  74
  75         \item\emph{A term rewrite system consists of the single rule
  76                 $$a(x,a(y,a(z,u)))\rightarrow a(y,a(z,a(x,u))),$$
  77                 in which $a$ is a binary symbol and $x,y,z,u$ are variables.
  78                 Moreover, there are constants $b,c,d,e,f,g$. Determine whether
  79                 $c$ and $d$ may swapped in $a(b,a(c,a(d,a(e,a(f,a(b,g))))))$ by
  80                 rewriting, that is, $a(b,a(c,a(d,a(e,a(f,a(b,g))))))$ rewrites
  81                 in a finite number of steps to
  82                 $a(b,a(d,a(c,a(e,a(f,a(b,g))))))$.}\\
  83
  84                 When inspecting the rewrite rule more closely we see that the
  85                 entire structure of the formula stays the same and that only
  86                 the variables $x,y,z$ are changed in order. Because of this we
  87                 can simplify the rule to
  88                 $$x,y,z\rightarrow y,z,x$$
  89                 and we can simplify the question to asking whether
  90                 $b,c,d,e,f,b$ rewrites to $b,d,c,e,f,b$.\\
  91
  92                 Because of this the nature of the rewritten problem becomes
  93                 solvable by a symbolic model checker. We define for every
  94                 position $i\in\{0\ldots5\}$ a variable $p_i$ of the enumeration
  95                 type $\{b,c,d,e,f\}$. To keep track of the moves we define a
  96                 move $m\in\{0\ldots4\}$ variable that indicates the location of
  97                 the first variable or $0$ for the initial value.  The initial
  98                 values of the position variables is
  99                 $$p_0=b,p_1=c,p_2=d,p_3=e,p_4=f,p_5=b$$
 100                 There are four possible transitions and they are put in a
 101                 disjunction and shown below:
 102                 $$\begin{array}{rl}
 103                         next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
 104                                 \wedge next(p_2)=p_0 \wedge\\
 105                         & next(p_3)=p_3 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5\\
 106
 107                         next(m)=2 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_2
 108                                 \wedge next(p_2)=p_3 \wedge\\
 109                         & next(p_3)=p_1 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5\\
 110
 111                         next(m)=3 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
 112                                 \wedge next(p_2)=p_3 \wedge\\
 113                         & next(p_3)=p_4 \wedge next(p_4)=p_2 \wedge next(p_5)=p_5\\
 114                         next(m)=4 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
 115                                 \wedge next(p_2)=p_2 \wedge\\
 116                         & next(p_3)=p_4 \wedge next(p_4)=p_5 \wedge next(p_5)=p_3
 117                 \end{array}$$
 118
 119                 The LTL logic goal state would then be
 120                 $$\mathcal{G} \neg(p_0=b\wedge p_1=d\wedge p_2=c\wedge
 121                 p_3=e\wedge p_4=f\wedge p_5=b)$$
 122
 123                 The solution described below is found by
 124                 \textsc{NuSMV} within $0.01$ seconds. Overlined triples are the
 125                 ones changed in the next.
 126                 $$\begin{array}{rl}
 127                         \overline{b,c,d},e,f,b
 128                                 & \rightarrow c,d,\overline{b,e,f},b\\
 129                                 & \rightarrow c,d,e,\overline{f,b,b}\\
 130                                 & \rightarrow c,d,e,\overline{b,b,f}\\
 131                                 & \rightarrow c,\overline{d,e,b},f,b\\
 132                                 & \rightarrow c,\overline{e,b,d},f,b\\
 133                                 & \rightarrow \overline{c,b,d},e,f,b\\
 134                                 & \rightarrow b,\overline{d,c,e},f,b\\
 135                                 & \rightarrow b,c,e,d,f,b\\
 136                 \end{array}$$
 137 \end{enumerate}