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 --- logic/logic_a.in.aux | 28 ++++++++++ logic/logic_b.m4.in | 9 ++++ logic/logic_b.m4.out | 143 +++++++++++++++++++++++++++++++++++++++++++++++++++ part2.tex | 137 +++++++++++++++++++++++++++++++++++++++++++++--- 4 files changed, 311 insertions(+), 6 deletions(-) create mode 100644 logic/logic_a.in.aux create mode 100644 logic/logic_b.m4.in create mode 100644 logic/logic_b.m4.out 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 -- cgit v1.2.1