update, table

[ar1516.git] / a2 / 3.tex

diff --git a/a2/3.tex b/a2/3.tex
index 7d59e59..c2c610f 100644 (file)
--- a/a2/3.tex
+++ b/a2/3.tex
@@ -1,5 +1,5 @@
 \section{Problem 3}
-\emph{The goal of this problem is to exploit the power of the recom mended
+\emph{The goal of this problem is to exploit the power of the recommended
 tools rather than elaborating the questions by hand.}
 \begin{enumerate}[a.]
        \item\emph{In mathematics, a \emph{group} is defined to be a set $G$
@@ -67,10 +67,12 @@ tools rather than elaborating the questions by hand.}
 \end{lstlisting}
 
                \textsc{prover9} fails to find a proof for $x*y=y*x$.
+               Running the same file with \textsc{mace4} gives the following
+               counterexample.
 
 
 
-       \item\emph{A term rewrite sysetm consists of the single rule
+       \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.
                Moreover, there are constants $b,c,d,e,f,g$. Determine whether
@@ -96,7 +98,7 @@ tools rather than elaborating the questions by hand.}
                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
-               disjuction and shown below:
+               disjunction and shown below:
                $$\begin{array}{rl}
                        next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
                                \wedge next(p_2)=p_0 \wedge\\
@@ -119,7 +121,7 @@ tools rather than elaborating the questions by hand.}
                p_3=e\wedge p_4=f\wedge p_5=b)$$
 
                The solution described below is found by
-               \textsc{NuSMV} within $0.01$ seconds. Overline triples are the
+               \textsc{NuSMV} within $0.01$ seconds. Overlined triples are the
                ones changed in the next.
                $$\begin{array}{rl}
                        \overline{b,c,d},e,f,b 
@@ -132,7 +134,4 @@ tools rather than elaborating the questions by hand.}
                                & \rightarrow b,\overline{d,c,e},f,b\\
                                & \rightarrow b,c,e,d,f,b\\
                \end{array}$$
-
-               
-
 \end{enumerate}