As found by \textsc{prover9} a proof for $inv(inv(x))=x$.
\begin{lstlisting}
-1 inv(inv(x)) = x. [goal].
-2 x * (y * z) = (x * y) * z.[assumption].
-3 (x * y) * z = x * (y * z).[copy(2),flip(a)].
-4 x * I = x. [assumption]
-5 x * inv(x) = I. [assumption].
-6 inv(inv(c1)) != c1. [deny(1)].
-7 x * (I * y) = x * y. [para(4(a,1),3(a,1,1)),flip(a)].
-8 x * (inv(x) * y) = I * y. [para(5(a,1),3(a,1,1)),flip(a)].
-13 I * inv(inv(x)) = x. [para(5(a,1),8(a,1,2)),rewrite([4(2)]),flip(a)].
-15 x * inv(inv(y)) = x * y. [para(13(a,1),3(a,2,2)),rewrite([4(2)])].
-16 I * x = x. [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])].
19 x * (inv(x) * y) = y. [back_rewrite(8),rewrite([16(5)])].
22 inv(inv(x)) = x. [para(5(a,1),19(a,1,2)),rewrite([4(2)]),flip(a)].
23 \$F. [resolve(22,a,6,a)].
As found by \textsc{prover9} a proof for $x*inv(x)=I$.
\begin{lstlisting}
-1 inv(x) * x = I. [goal].
-2 x * (y * z) = (x * y) * z.[assumption].
-3 (x * y) * z = x * (y * z).[copy(2),flip(a)].
-4 x * I = x. [assumption].
-5 x * inv(x) = I. [assumption].
-6 inv(c1) * c1 != I. [deny(1)].
-7 x * (I * y) = x * y. [para(4(a,1),3(a,1,1)),flip(a)].
-8 x * (inv(x) * y) = I * y. [para(5(a,1),3(a,1,1)),flip(a)].
-13 I * inv(inv(x)) = x. [para(5(a,1),8(a,1,2)),rewrite([4(2)]),flip(a)].
-15 x * inv(inv(y)) = x * y. [para(13(a,1),3(a,2,2)),rewrite([4(2)])].
-16 I * x = x. [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])].
-19 x * (inv(x) * y) = y. [back_rewrite(8),rewrite([16(5)])].
-22 inv(inv(x)) = x. [para(5(a,1),19(a,1,2)),rewrite([4(2)]),flip(a)].
24 inv(x) * x = I. [para(22(a,1),5(a,1,2))].
25 \$F. [resolve(24,a,6,a)].
\end{lstlisting}
\textsc{prover9} fails to find a proof for $x*y=y*x$.
- Running the same file with \textsc{mace4} gives the following
+ Running the same file with \textsc{mace4} gives the smallest
counterexample listed in Table~\ref{tab:s3a}.
\begin{table}[H]
& 5 & 5 & 3 & 4 & 1 & 2 & 0
\end{array}\right.$
\end{tabular}
- \caption{Solution for problem 3a}\label{tab:s3a}
+ \caption{Smallest counterexample for problem 3a}\label{tab:s3a}
\end{table}
+ \newpage
\item\emph{A term rewrite system consists of the single rule
$$a(x,a(y,a(z,u)))\rightarrow a(y,a(z,a(x,u))),$$
in which $a$ is a binary symbol and $x,y,z,u$ are variables.
When inspecting the rewrite rule more closely we see that the
entire structure of the formula stays the same and that only
- the variables $x,y,z$ are changed in order. Because of this we
- can simplify the rule to
- $$x,y,z\rightarrow y,z,x$$
- and we can simplify the question to asking whether
- $b,c,d,e,f,b$ rewrites to $b,d,c,e,f,b$.\\
+ the variables $x,y,z$ are changed in order. Thus we can simplify the
+ rule and question to
+ $$x,y,z\rightarrow y,z,x\text{ and }
+ b,c,d,e,f,b\overset{*?}{\rightarrow}b,d,c,e,f,b$$
- Because of this the nature of the rewritten problem becomes
- solvable by a symbolic model checker. We define for every
- position $i\in\{0\ldots5\}$ a variable $p_i$ of the enumeration
- type $\{b,c,d,e,f\}$. To keep track of the moves we define a
- move $m\in\{0\ldots4\}$ variable that indicates the location of
- the first variable or $0$ for the initial value. The initial
- values of the position variables is
- $$p_0=b,p_1=c,p_2=d,p_3=e,p_4=f,p_5=b$$
- There are four possible transitions and they are put in a
- disjunction and shown below:
- $$\begin{array}{rl}
- next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
+ Applying these changes changes the problem into a model checking
+ problem. For every position $i\in\{0\ldots5\}$ a variable $p_i$ of the
+ enumeration type $\{b,c,d,e,f\}$ is defined. To keep track of the moves
+ a move $m\in\{0\ldots4\}$ variable that indicates the location of the
+ first variable or $0$ for the initial value is defined. The initial
+ values of the position variables are
+ $$p_0=b\wedge p_1=c\wedge p_2=d\wedge p_3=e\wedge p_4=f\wedge p_5=b
+ \wedge m=0$$
+ There are four possible transitions as shown below.
+ $$\begin{array}{rrl}
+ & (next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
\wedge next(p_2)=p_0 \wedge\\
- & next(p_3)=p_3 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5\\
-
- next(m)=2 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_2
+ & & next(p_3)=p_3 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5)\\
+ \vee & (next(m)=2 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_2
\wedge next(p_2)=p_3 \wedge\\
- & next(p_3)=p_1 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5\\
-
- next(m)=3 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
+ & & next(p_3)=p_1 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5)\\
+ \vee & (next(m)=3 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
\wedge next(p_2)=p_3 \wedge\\
- & next(p_3)=p_4 \wedge next(p_4)=p_2 \wedge next(p_5)=p_5\\
- next(m)=4 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
+ & & next(p_3)=p_4 \wedge next(p_4)=p_2 \wedge next(p_5)=p_5)\\
+ \vee & (next(m)=4 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
\wedge next(p_2)=p_2 \wedge\\
- & next(p_3)=p_4 \wedge next(p_4)=p_5 \wedge next(p_5)=p_3
+ & & next(p_3)=p_4 \wedge next(p_4)=p_5 \wedge next(p_5)=p_3)
\end{array}$$
- The LTL logic goal state would then be
+ With the following goal the solution below is
+ found by \textsc{NuSMV} within $0.01$ seconds.
$$\mathcal{G} \neg(p_0=b\wedge p_1=d\wedge p_2=c\wedge
p_3=e\wedge p_4=f\wedge p_5=b)$$
-
- The solution described below is found by
- \textsc{NuSMV} within $0.01$ seconds. Lined over triples are the
- ones changed in the next.
$$\begin{array}{rl}
\overline{b,c,d},e,f,b
& \rightarrow c,d,\overline{b,e,f},b\\
repositories / ar1516.git / blobdiff