From eb0899b974b937b8a0dbd496d6b99c6e9c6a1d44 Mon Sep 17 00:00:00 2001 From: Koen van der Heijden Date: Sun, 15 Jan 2017 18:59:40 +0100 Subject: part 3 done --- part2.tex | 137 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 131 insertions(+), 6 deletions(-) (limited to 'part2.tex') 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 -- cgit v1.2.1