part 3 done

4 files changed, 311 insertions, 6 deletions

diff --git a/logic/logic_a.in.aux b/logic/logic_a.in.aux
new file mode 100644
index 0000000..e467de7
--- /dev/null
+++ b/logic/logic_a.in.aux
@@ -0,0 +1,28 @@
+\relax 
+\providecommand\hyper@newdestlabel[2]{}
+\@setckpt{logic/logic_a.in}{
+\setcounter{page}{7}
+\setcounter{equation}{8}
+\setcounter{enumi}{9}
+\setcounter{enumii}{0}
+\setcounter{enumiii}{0}
+\setcounter{enumiv}{0}
+\setcounter{footnote}{0}
+\setcounter{mpfootnote}{0}
+\setcounter{part}{0}
+\setcounter{section}{0}
+\setcounter{subsection}{0}
+\setcounter{subsubsection}{0}
+\setcounter{paragraph}{0}
+\setcounter{subparagraph}{0}
+\setcounter{figure}{0}
+\setcounter{table}{1}
+\setcounter{parentequation}{0}
+\setcounter{lstnumber}{10}
+\setcounter{Item}{9}
+\setcounter{Hfootnote}{0}
+\setcounter{bookmark@seq@number}{0}
+\setcounter{float@type}{8}
+\setcounter{lstlisting}{2}
+\setcounter{section@level}{0}
+}
diff --git a/logic/logic_b.m4.in b/logic/logic_b.m4.in
new file mode 100644
index 0000000..8cc7b75
--- /dev/null
+++ b/logic/logic_b.m4.in
@@ -0,0 +1,9 @@
+formulas(sos).
+	(x*(y*z)=(x*y)*z).
+	(x*I=x).
+	(x*inv(x)=I).
+end_of_list.
+
+formulas(goals).
+	all x all y (x*y=y*x).
+end_of_list.
diff --git a/logic/logic_b.m4.out b/logic/logic_b.m4.out
new file mode 100644
index 0000000..43b07fd
--- /dev/null
+++ b/logic/logic_b.m4.out
@@ -0,0 +1,143 @@
+============================== Mace4 =================================
+Mace4 (64) version 2009-11A, November 2009.
+Process 3232 was started by koen on vdheijden-arch,
+Sun Jan 15 16:43:42 2017
+The command was "mace4 -f logic_b.m4.in".
+============================== end of head ===========================
+
+============================== INPUT =================================
+
+% Reading from file logic_b.m4.in
+
+
+formulas(sos).
+x * (y * z) = (x * y) * z.
+x * I = x.
+x * inv(x) = I.
+end_of_list.
+
+formulas(goals).
+(all x all y x * y = y * x).
+end_of_list.
+
+============================== end of input ==========================
+
+============================== PROCESS NON-CLAUSAL FORMULAS ==========
+
+% Formulas that are not ordinary clauses:
+1 (all x all y x * y = y * x) # label(non_clause) # label(goal).  [goal].
+
+============================== end of process non-clausal formulas ===
+
+============================== CLAUSES FOR SEARCH ====================
+
+formulas(mace4_clauses).
+x * (y * z) = (x * y) * z.
+x * I = x.
+x * inv(x) = I.
+c2 * c1 != c1 * c2.
+end_of_list.
+
+============================== end of clauses for search =============
+
+% There are no natural numbers in the input.
+
+============================== DOMAIN SIZE 2 =========================
+
+============================== STATISTICS ============================
+
+For domain size 2.
+
+Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
+Ground clauses: seen=13, kept=13.
+Selections=4, assignments=7, propagations=6, current_models=0.
+Rewrite_terms=62, rewrite_bools=16, indexes=8.
+Rules_from_neg_clauses=2, cross_offs=2.
+
+============================== end of statistics =====================
+
+============================== DOMAIN SIZE 3 =========================
+
+============================== STATISTICS ============================
+
+For domain size 3.
+
+Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
+Ground clauses: seen=34, kept=34.
+Selections=7, assignments=17, propagations=30, current_models=0.
+Rewrite_terms=298, rewrite_bools=71, indexes=52.
+Rules_from_neg_clauses=8, cross_offs=24.
+
+============================== end of statistics =====================
+
+============================== DOMAIN SIZE 4 =========================
+
+============================== STATISTICS ============================
+
+For domain size 4.
+
+Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
+Ground clauses: seen=73, kept=73.
+Selections=14, assignments=45, propagations=110, current_models=0.
+Rewrite_terms=1132, rewrite_bools=232, indexes=206.
+Rules_from_neg_clauses=18, cross_offs=98.
+
+============================== end of statistics =====================
+
+============================== DOMAIN SIZE 5 =========================
+
+============================== STATISTICS ============================
+
+For domain size 5.
+
+Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
+Ground clauses: seen=136, kept=136.
+Selections=24, assignments=91, propagations=201, current_models=0.
+Rewrite_terms=2416, rewrite_bools=472, indexes=582.
+Rules_from_neg_clauses=31, cross_offs=228.
+
+============================== end of statistics =====================
+
+============================== DOMAIN SIZE 6 =========================
+
+============================== MODEL =================================
+
+interpretation( 6, [number=1, seconds=0], [
+
+        function(I, [ 0 ]),
+
+        function(c1, [ 1 ]),
+
+        function(c2, [ 2 ]),
+
+        function(inv(_), [ 0, 1, 2, 4, 3, 5 ]),
+
+        function(*(_,_), [
+			   0, 1, 2, 3, 4, 5,
+			   1, 0, 3, 2, 5, 4,
+			   2, 4, 0, 5, 1, 3,
+			   3, 5, 1, 4, 0, 2,
+			   4, 2, 5, 0, 3, 1,
+			   5, 3, 4, 1, 2, 0 ])
+]).
+
+============================== end of model ==========================
+
+============================== STATISTICS ============================
+
+For domain size 6.
+
+Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
+Ground clauses: seen=229, kept=229.
+Selections=14, assignments=44, propagations=94, current_models=1.
+Rewrite_terms=1566, rewrite_bools=339, indexes=370.
+Rules_from_neg_clauses=8, cross_offs=138.
+
+============================== end of statistics =====================
+
+User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
+
+Exiting with 1 model.
+
+Process 3232 exit (max_models) Sun Jan 15 16:43:42 2017
+The process finished Sun Jan 15 16:43:42 2017
diff --git a/part2.tex b/part2.tex
index 6959fd3..e6b11e9 100644
--- a/part2.tex
+++ b/part2.tex
@@ -317,8 +317,6 @@ the smallest finite group for which it does not hold.
 
 \subsection*{Solution:}
 \subsubsection*{(a)}
-Using prover9, we found that $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ indeed rewrites to $a(p, q)$.
-
 We want to prove that
 \begin{enumerate}
   \item \label{itm:logic_a_1} $\forall p \forall q : a(p, a(q, a(p, a(q, a(p, a(q, p)))))) = a(p, q)$
@@ -345,16 +343,143 @@ On \ref{itm:logic_a_7}, we can then apply \ref{itm:logic_a_3} twice
 \begin{enumerate}[resume]
   \item \label{itm:logic_a_8} $a(x, a(y, x)) = a(y, x)$
 \end{enumerate}
-Finally, we can recursively apply \ref{itm:logic_a_7} and \ref{itm:logic_a_8} to \ref{itm:logic_a_6}, where $c1 \gets x$ and $c2 \gets y$
+Finally, we can recursively apply \ref{itm:logic_a_3}, \ref{itm:logic_a_7} and \ref{itm:logic_a_8} to \ref{itm:logic_a_6}, where $c1 \gets x$ and $c2 \gets y$
 \begin{enumerate}[resume]
   \item \label{itm:logic_a_9} $a(x, a(y, a(x, a(y, a(x, a(y, x)))))) \neq a(x, a(y, a(x, a(y, a(x, a(y, x))))))$
 \end{enumerate}
-which evaluates to $FALSE$.
+which evaluates to $FALSE$.\\
+Therefore, we found that no counterexample exists, which proves that $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ indeed rewrites to $a(p, q)$.
 \\
-This proves that $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ indeed rewrites to $a(p, q)$.
+We derived this proof with \textit{prover9}, using the following input:
+\begin{lstlisting}
+formulas(sos).
+	a(x,x)=x.
+	a(x,y)=a(y,x).
+	a(x,a(y,z))=a(a(x,y),z).
+end_of_list.
+
+formulas(goals).
+	all p all q (a(p,a(q,a(p,a(q,a(p,a(q,p))))))=a(p,q)).
+end_of_list.
+\end{lstlisting}
 
 \subsubsection*{(b)}
-The first 3 properties hold for every group. The fourth property does not hold for all groups though.
+We want to prove 4 things:
+\begin{enumerate}
+  \item \label{itm:logic_b_1} $\forall x : I * x = x$
+  \item \label{itm:logic_b_2} $\forall x : inv(inv(x)) = x$
+  \item \label{itm:logic_b_3} $\forall x : inv(x) * x = I$
+  \item \label{itm:logic_b_4} $\forall x \forall y : x * y = y * x$
+\end{enumerate}
+Using the assumptions
+\begin{enumerate}[resume]
+ \item \label{itm:logic_b_5} $x * (y * z) = (x * y) * z$
+ \item \label{itm:logic_b_6} $x * I = x$
+ \item \label{itm:logic_b_7} $x * inv(x) = I$
+\end{enumerate}
+
+To prove \ref{itm:logic_b_1}, \ref{itm:logic_b_2}, \ref{itm:logic_b_3} and \ref{itm:logic_b_4}, we created the following input:
+\begin{lstlisting}
+formulas(sos).
+	(x*(y*z)=(x*y)*z).
+	(x*I=x).
+	(x*inv(x)=I).
+end_of_list.
+
+formulas(goals).
+	all x (I*x=x).
+	all x (inv(inv(x))=x).
+	all x (inv(x)*x=I).
+	all x all y (x*y=y*x).
+end_of_list.
+\end{lstlisting}
+
+Running this input through \textit{prover9} generated the following proofs for \ref{itm:logic_b_1}, \ref{itm:logic_b_2} and \ref{itm:logic_b_3} respectively:
+\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_1}]
+1 (all x I * x = x) # label(non_clause) # label(goal).  [goal].
+5 x * (y * z) = (x * y) * z.  [assumption].
+6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
+7 x * I = x.  [assumption].
+8 x * inv(x) = I.  [assumption].
+9 I * c1 != c1.  [deny(1)].
+13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
+14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
+19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
+21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
+22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
+23 $F.  [resolve(22,a,9,a)].
+\end{lstlisting}
+
+\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_2}]
+2 (all x inv(inv(x)) = x) # label(non_clause) # label(goal).  [goal].
+5 x * (y * z) = (x * y) * z.  [assumption].
+6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
+7 x * I = x.  [assumption].
+8 x * inv(x) = I.  [assumption].
+10 inv(inv(c2)) != c2.  [deny(2)].
+13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
+14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
+19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
+21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
+22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
+26 x * (inv(x) * y) = y.  [back_rewrite(14),rewrite([22(5)])].
+30 inv(inv(x)) = x.  [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)].
+31 $F.  [resolve(30,a,10,a)].
+\end{lstlisting}
+
+\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_3}]
+3 (all x inv(x) * x = I) # label(non_clause) # label(goal).  [goal].
+5 x * (y * z) = (x * y) * z.  [assumption].
+6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
+7 x * I = x.  [assumption].
+8 x * inv(x) = I.  [assumption].
+11 inv(c3) * c3 != I.  [deny(3)].
+13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
+14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
+19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
+21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
+22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
+26 x * (inv(x) * y) = y.  [back_rewrite(14),rewrite([22(5)])].
+30 inv(inv(x)) = x.  [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)].
+34 inv(x) * x = I.  [para(30(a,1),8(a,1,2))].
+35 $F.  [resolve(34,a,11,a)].
+\end{lstlisting}
+
+\textit{prover9} was not able to prover that $x * y = y * x$ holds for all finite groups. Therefor, we ran \ref{itm:logic_b_4} through \textit{mace4} to find the smallest group $G(I, *, inv)$ for which $x * y \neq y * x$.
+The following input was used:
+\begin{verbatim}
+formulas(sos).
+	(x*(y*z)=(x*y)*z).
+	(x*I=x).
+	(x*inv(x)=I).
+end_of_list.
+
+formulas(goals).
+	all x all y (x*y=y*x).
+end_of_list.
+\end{verbatim}
+After running this input through \textit{mace4}, we retrieved the following finite group $G(I, *, inv)$:
+\begin{verbatim}
+ I: 0
+ 
+ *:    | 0 1 2 3 4 5
+     --*-------------
+     0 | 0 1 2 3 4 5 
+     1 | 1 0 3 2 5 4
+     2 | 2 4 0 5 1 3
+     3 | 3 5 1 4 0 2
+     4 | 4 2 5 0 3 1
+     5 | 5 3 4 1 2 0
+ 
+ inv: 0 -> 0 
+      1 -> 1
+      2 -> 2
+      3 -> 3
+      4 -> 4
+      5 -> 5
+\end{verbatim}
+We specify the row number in the $*$-operator table to be the left element, and the column number to be the right element.
+Let $x \gets 2$ and $y \gets 1$. Then, we know that $x * y = 2 * 1 = 4$. Also, $y * x = 1 * 2 = 3$. Since $4 \neq 3$, we know that $x * y \neq y * x$, which proves that the property $x * y = y * x$ indeed does not hold for this group.
 
 \section*{Problem: }
 Give a precise description of a non-trivial problem of your own choice, and