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 19 x * (inv(x) * y) = y.     [back_rewrite(8),rewrite([16(5)])].
  35 22 inv(inv(x)) = x.          [para(5(a,1),19(a,1,2)),rewrite([4(2)]),flip(a)].
  36 23 \$F.                      [resolve(22,a,6,a)].
  37                 \end{lstlisting}
  38
  39                 As found by \textsc{prover9} a proof for $x*inv(x)=I$.
  40                 \begin{lstlisting}
  41 24 inv(x) * x = I.           [para(22(a,1),5(a,1,2))].
  42 25 \$F.                      [resolve(24,a,6,a)].
  43 \end{lstlisting}
  44
  45                 \textsc{prover9} fails to find a proof for $x*y=y*x$.
  46                 Running the same file with \textsc{mace4} gives the smallest
  47                 counterexample listed in Table~\ref{tab:s3a}.
  48
  49                 \begin{table}[h]
  50                         \centering
  51                         \begin{tabular}{llll}
  52                                 $G=\{0,1,2,3,4,5\}$ & $I=0$ &
  53                                 $inv(x)=\left\{\begin{array}{ll}
  54                                         x=3 & 4\\
  55                                         x=4 & 3\\
  56                                         \text{else} & x
  57                                 \end{array}\right.$ &
  58                                 $x*y=\left\{\begin{array}{ll|llllll}
  59                                         & & \multicolumn{6}{c}{x}\\
  60                                          & & 0& 1 & 2 & 3 & 4 & 5\\
  61                                         \hline
  62                                         \multirow{6}{*}{y}& 1 & 0 & 1 & 2 & 3 & 4 & 5\\
  63                                         & 1 & 1 & 0 & 3 & 2 & 5 & 4\\
  64                                         & 2 & 2 & 4 & 0 & 5 & 1 & 3\\
  65                                         & 3 & 3 & 5 & 1 & 4 & 0 & 2\\
  66                                         & 4 & 4 & 2 & 5 & 0 & 3 & 1\\
  67                                         & 5 & 5 & 3 & 4 & 1 & 2 & 0
  68                                 \end{array}\right.$
  69                         \end{tabular}
  70                         \caption{Smallest counterexample for problem 3a}\label{tab:s3a}
  71                 \end{table}
  72                 \newpage
  73         \item\emph{A term rewrite system consists of the single rule
  74                 $$a(x,a(y,a(z,u)))\rightarrow a(y,a(z,a(x,u))),$$
  75                 in which $a$ is a binary symbol and $x,y,z,u$ are variables.
  76                 Moreover, there are constants $b,c,d,e,f,g$. Determine whether
  77                 $c$ and $d$ may swapped in $a(b,a(c,a(d,a(e,a(f,a(b,g))))))$ by
  78                 rewriting, that is, $a(b,a(c,a(d,a(e,a(f,a(b,g))))))$ rewrites
  79                 in a finite number of steps to
  80                 $a(b,a(d,a(c,a(e,a(f,a(b,g))))))$.}\\
  81
  82                 When inspecting the rewrite rule more closely we see that the
  83                 entire structure of the formula stays the same and that only
  84                 the variables $x,y,z$ are changed in order. Thus we can simplify the
  85                 rule and question to
  86                 $$x,y,z\rightarrow y,z,x\text{ and }
  87                 b,c,d,e,f,b\overset{*?}{\rightarrow}b,d,c,e,f,b$$
  88
  89                 Applying these changes changes the problem into a model checking
  90                 problem. For every position $i\in\{0\ldots5\}$ a variable $p_i$ of the
  91                 enumeration type $\{b,c,d,e,f\}$ is defined. To keep track of the moves
  92                 a move $m\in\{0\ldots4\}$ variable that indicates the location of the
  93                 first variable or $0$ for the initial value is defined. The initial
  94                 values of the position variables are
  95                 $$p_0=b\wedge p_1=c\wedge p_2=d\wedge p_3=e\wedge p_4=f\wedge p_5=b
  96                 \wedge m=0$$
  97                 There are four possible transitions as shown below.
  98                 $$\begin{array}{rrl}
  99                         & (next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
 100                                 \wedge next(p_2)=p_0 \wedge\\
 101                         & & next(p_3)=p_3 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5)\\
 102                         \vee & (next(m)=2 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_2
 103                                 \wedge next(p_2)=p_3 \wedge\\
 104                         & & next(p_3)=p_1 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5)\\
 105                         \vee & (next(m)=3 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
 106                                 \wedge next(p_2)=p_3 \wedge\\
 107                         & & next(p_3)=p_4 \wedge next(p_4)=p_2 \wedge next(p_5)=p_5)\\
 108                         \vee & (next(m)=4 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
 109                                 \wedge next(p_2)=p_2 \wedge\\
 110                         & & next(p_3)=p_4 \wedge next(p_4)=p_5 \wedge next(p_5)=p_3)
 111                 \end{array}$$
 112
 113                 With the following goal the solution below is
 114                 found by \textsc{NuSMV} within $0.01$ seconds.
 115                 $$\mathcal{G} \neg(p_0=b\wedge p_1=d\wedge p_2=c\wedge
 116                 p_3=e\wedge p_4=f\wedge p_5=b)$$
 117                 $$\begin{array}{rl}
 118                         \overline{b,c,d},e,f,b
 119                                 & \rightarrow c,d,\overline{b,e,f},b\\
 120                                 & \rightarrow c,d,e,\overline{f,b,b}\\
 121                                 & \rightarrow c,d,e,\overline{b,b,f}\\
 122                                 & \rightarrow c,\overline{d,e,b},f,b\\
 123                                 & \rightarrow c,\overline{e,b,d},f,b\\
 124                                 & \rightarrow \overline{c,b,d},e,f,b\\
 125                                 & \rightarrow b,\overline{d,c,e},f,b\\
 126                                 & \rightarrow b,c,e,d,f,b\\
 127                 \end{array}$$
 128 \end{enumerate}