update, table

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}

diff --git a/a2/4.tex b/a2/4.tex
index 1147320..7fcece0 100644 (file)
--- a/a2/4.tex
+++ b/a2/4.tex
@@ -107,6 +107,11 @@ $$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right)
 
 \subsection{Solution}
 The conversion to SMT-Lib is trivial however on a $3.8Ghz$ processor running
-\textsc{yices} it takes about $4$ hours and $15$ minutes to find a solution.
+\textsc{yices} it takes about $4$ hours and $15$ minutes to find the solution
+listed in Table~\ref{tab:sol}.
 
+\begin{table}[H]
+       \centering
 \input{src/4/a4.tex}
+       \caption{Solution for \emph{English peg solitaire}}\label{tab:sol}
+\end{table}

diff --git a/a2/src/3a.prvr9 b/a2/src/3a.prvr9
index 8ee213c..812fdd4 100644 (file)
--- a/a2/src/3a.prvr9
+++ b/a2/src/3a.prvr9
@@ -1,11 +1,11 @@
 formulas(assumptions).
-x*(y*z)=(x*y)*z.
-x*I=x.
-x*inv(x)=I.
+all x all y all z (x*(y*z)=(x*y)*z).
+all x (x*I=x).
+all x (x*inv(x)=I).
 end_of_list.
 formulas(goals).
 %I*x=x.
 %inv(inv(x))=x.
 %inv(x)*x=I.
-x*y=y*x.
+all x all y (x*y=y*x).
 end_of_list.