3a done. 3b partially

5 files changed, 489 insertions, 3 deletions

diff --git a/logic/logic_a.in b/logic/logic_a.in
new file mode 100644
index 0000000..625351d
--- /dev/null
+++ b/logic/logic_a.in
@@ -0,0 +1,9 @@
+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.
diff --git a/logic/logic_a.out b/logic/logic_a.out
new file mode 100644
index 0000000..828d77f
--- /dev/null
+++ b/logic/logic_a.out
@@ -0,0 +1,157 @@
+============================== Prover9 ===============================
+Prover9 (64) version 2009-11A, November 2009.
+Process 7784 was started by koen on vdheijden-arch,
+Sat Jan 14 16:51:59 2017
+The command was "prover9 -f logic_a.in".
+============================== end of head ===========================
+
+============================== INPUT =================================
+
+% Reading from file logic_a.in
+
+
+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 of input ==========================
+
+============================== PROCESS NON-CLAUSAL FORMULAS ==========
+
+% Formulas that are not ordinary clauses:
+1 (all p all q a(p,a(q,a(p,a(q,a(p,a(q,p)))))) = a(p,q)) # label(non_clause) # label(goal).  [goal].
+
+============================== end of process non-clausal formulas ===
+
+============================== PROCESS INITIAL CLAUSES ===============
+
+% Clauses before input processing:
+
+formulas(usable).
+end_of_list.
+
+formulas(sos).
+a(x,x) = x.  [assumption].
+a(x,y) = a(y,x).  [assumption].
+a(x,a(y,z)) = a(a(x,y),z).  [assumption].
+a(c1,a(c2,a(c1,a(c2,a(c1,a(c2,c1)))))) != a(c1,c2).  [deny(1)].
+end_of_list.
+
+formulas(demodulators).
+end_of_list.
+
+============================== PREDICATE ELIMINATION =================
+
+No predicates eliminated.
+
+============================== end predicate elimination =============
+
+Auto_denials:  (no changes).
+
+Term ordering decisions:
+Predicate symbol precedence:  predicate_order([ = ]).
+Function symbol precedence:  function_order([ c1, c2, a ]).
+After inverse_order:  (no changes).
+Unfolding symbols: (none).
+
+Auto_inference settings:
+  % set(paramodulation).  % (positive equality literals)
+
+Auto_process settings:  (no changes).
+
+kept:      2 a(x,x) = x.  [assumption].
+
+% Operation a is commutative; C redundancy checks enabled.
+kept:      3 a(x,y) = a(y,x).  [assumption].
+           4 a(x,a(y,z)) = a(a(x,y),z).  [assumption].
+kept:      5 a(a(x,y),z) = a(x,a(y,z)).  [copy(4),flip(a)].
+           6 a(c1,a(c2,a(c1,a(c2,a(c1,a(c2,c1)))))) != a(c1,c2).  [deny(1)].
+kept:      7 a(c1,a(c2,a(c1,a(c2,a(c1,a(c1,c2)))))) != a(c1,c2).  [copy(6),rewrite([3(8)])].
+
+============================== end of process initial clauses ========
+
+============================== CLAUSES FOR SEARCH ====================
+
+% Clauses after input processing:
+
+formulas(usable).
+end_of_list.
+
+formulas(sos).
+2 a(x,x) = x.  [assumption].
+3 a(x,y) = a(y,x).  [assumption].
+5 a(a(x,y),z) = a(x,a(y,z)).  [copy(4),flip(a)].
+7 a(c1,a(c2,a(c1,a(c2,a(c1,a(c1,c2)))))) != a(c1,c2).  [copy(6),rewrite([3(8)])].
+end_of_list.
+
+formulas(demodulators).
+2 a(x,x) = x.  [assumption].
+3 a(x,y) = a(y,x).  [assumption].
+        % (lex-dep)
+5 a(a(x,y),z) = a(x,a(y,z)).  [copy(4),flip(a)].
+end_of_list.
+
+============================== end of clauses for search =============
+
+============================== SEARCH ================================
+
+% Starting search at 0.02 seconds.
+
+given #1 (I,wt=5): 2 a(x,x) = x.  [assumption].
+
+given #2 (I,wt=7): 3 a(x,y) = a(y,x).  [assumption].
+
+given #3 (I,wt=11): 5 a(a(x,y),z) = a(x,a(y,z)).  [copy(4),flip(a)].
+
+% Operation a is associative-commutative; CAC redundancy checks enabled.
+
+============================== PROOF =================================
+
+% Proof 1 at 0.02 (+ 0.00) seconds.
+% Length of proof is 10.
+% Level of proof is 3.
+% Maximum clause weight is 17.000.
+% Given clauses 3.
+
+1 (all p all q a(p,a(q,a(p,a(q,a(p,a(q,p)))))) = a(p,q)) # label(non_clause) # label(goal).  [goal].
+2 a(x,x) = x.  [assumption].
+3 a(x,y) = a(y,x).  [assumption].
+4 a(x,a(y,z)) = a(a(x,y),z).  [assumption].
+5 a(a(x,y),z) = a(x,a(y,z)).  [copy(4),flip(a)].
+6 a(c1,a(c2,a(c1,a(c2,a(c1,a(c2,c1)))))) != a(c1,c2).  [deny(1)].
+7 a(c1,a(c2,a(c1,a(c2,a(c1,a(c1,c2)))))) != a(c1,c2).  [copy(6),rewrite([3(8)])].
+9 a(x,a(x,y)) = a(x,y).  [para(2(a,1),5(a,1,1)),flip(a)].
+10 a(x,a(y,x)) = a(y,x).  [para(2(a,1),5(a,2,2)),rewrite([3(2)])].
+13 $F.  [back_rewrite(7),rewrite([9(9),10(8),9(7),10(6),9(5)]),xx(a)].
+
+============================== end of proof ==========================
+
+============================== STATISTICS ============================
+
+Given=3. Generated=27. Kept=9. proofs=1.
+Usable=3. Sos=1. Demods=8. Limbo=4, Disabled=5. Hints=0.
+Kept_by_rule=0, Deleted_by_rule=0.
+Forward_subsumed=17. Back_subsumed=0.
+Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
+New_demodulators=8 (3 lex), Back_demodulated=1. Back_unit_deleted=0.
+Demod_attempts=222. Demod_rewrites=33.
+Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
+Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
+Megabytes=0.05.
+User_CPU=0.02, System_CPU=0.00, Wall_clock=0.
+
+============================== end of statistics =====================
+
+============================== end of search =========================
+
+THEOREM PROVED
+
+Exiting with 1 proof.
+
+Process 7784 exit (max_proofs) Sat Jan 14 16:51:59 2017
diff --git a/logic/logic_b.in b/logic/logic_b.in
new file mode 100644
index 0000000..6e087e7
--- /dev/null
+++ b/logic/logic_b.in
@@ -0,0 +1,12 @@
+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.
diff --git a/logic/logic_b.out b/logic/logic_b.out
new file mode 100644
index 0000000..da9e9b0
--- /dev/null
+++ b/logic/logic_b.out
@@ -0,0 +1,273 @@
+============================== Prover9 ===============================
+Prover9 (64) version 2009-11A, November 2009.
+Process 13543 was started by koen on vdheijden-arch,
+Sat Jan 14 20:02:31 2017
+The command was "prover9 -f logic_b.in".
+============================== end of head ===========================
+
+============================== INPUT =================================
+
+% Reading from file logic_b.in
+
+
+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 of input ==========================
+
+============================== PROCESS NON-CLAUSAL FORMULAS ==========
+
+% Formulas that are not ordinary clauses:
+1 (all x I * x = x) # label(non_clause) # label(goal).  [goal].
+2 (all x inv(inv(x)) = x) # label(non_clause) # label(goal).  [goal].
+3 (all x inv(x) * x = I) # label(non_clause) # label(goal).  [goal].
+4 (all x all y x * y = y * x) # label(non_clause) # label(goal).  [goal].
+
+============================== end of process non-clausal formulas ===
+
+============================== PROCESS INITIAL CLAUSES ===============
+
+% Clauses before input processing:
+
+formulas(usable).
+end_of_list.
+
+formulas(sos).
+x * (y * z) = (x * y) * z.  [assumption].
+x * I = x.  [assumption].
+x * inv(x) = I.  [assumption].
+I * c1 != c1.  [deny(1)].
+inv(inv(c2)) != c2.  [deny(2)].
+inv(c3) * c3 != I.  [deny(3)].
+c5 * c4 != c4 * c5.  [deny(4)].
+end_of_list.
+
+formulas(demodulators).
+end_of_list.
+
+============================== PREDICATE ELIMINATION =================
+
+No predicates eliminated.
+
+============================== end predicate elimination =============
+
+Auto_denials:
+  % assign(max_proofs, 4).  % (Horn set with more than one neg. clause)
+
+WARNING, because some of the denials share constants,
+some of the denials or their descendents may be subsumed,
+preventing the target number of proofs from being found.
+The shared constants are:  I.
+
+Term ordering decisions:
+Predicate symbol precedence:  predicate_order([ = ]).
+Function symbol precedence:  function_order([ I, c1, c2, c3, c4, c5, *, inv ]).
+After inverse_order: Function symbol precedence:  function_order([ I, c1, c2, c3, c4, c5, *, inv ]).
+Unfolding symbols: (none).
+
+Auto_inference settings:
+  % set(paramodulation).  % (positive equality literals)
+
+Auto_process settings:  (no changes).
+
+           5 x * (y * z) = (x * y) * z.  [assumption].
+kept:      6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
+kept:      7 x * I = x.  [assumption].
+kept:      8 x * inv(x) = I.  [assumption].
+kept:      9 I * c1 != c1.  [deny(1)].
+kept:      10 inv(inv(c2)) != c2.  [deny(2)].
+kept:      11 inv(c3) * c3 != I.  [deny(3)].
+kept:      12 c5 * c4 != c4 * c5.  [deny(4)].
+
+============================== end of process initial clauses ========
+
+============================== CLAUSES FOR SEARCH ====================
+
+% Clauses after input processing:
+
+formulas(usable).
+end_of_list.
+
+formulas(sos).
+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)].
+10 inv(inv(c2)) != c2.  [deny(2)].
+11 inv(c3) * c3 != I.  [deny(3)].
+12 c5 * c4 != c4 * c5.  [deny(4)].
+end_of_list.
+
+formulas(demodulators).
+6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
+7 x * I = x.  [assumption].
+8 x * inv(x) = I.  [assumption].
+end_of_list.
+
+============================== end of clauses for search =============
+
+============================== SEARCH ================================
+
+% Starting search at 0.02 seconds.
+
+given #1 (I,wt=11): 6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
+
+given #2 (I,wt=5): 7 x * I = x.  [assumption].
+
+given #3 (I,wt=6): 8 x * inv(x) = I.  [assumption].
+
+given #4 (I,wt=5): 9 I * c1 != c1.  [deny(1)].
+
+given #5 (I,wt=5): 10 inv(inv(c2)) != c2.  [deny(2)].
+
+given #6 (I,wt=6): 11 inv(c3) * c3 != I.  [deny(3)].
+
+given #7 (I,wt=7): 12 c5 * c4 != c4 * c5.  [deny(4)].
+
+given #8 (A,wt=9): 13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
+
+given #9 (T,wt=6): 16 x * inv(I) = x.  [para(8(a,1),13(a,1,2)),rewrite([7(2)]),flip(a)].
+
+given #10 (T,wt=10): 14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
+
+given #11 (T,wt=7): 19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
+
+============================== PROOF =================================
+
+% Proof 1 at 0.02 (+ 0.00) seconds.
+% Length of proof is 12.
+% Level of proof is 6.
+% Maximum clause weight is 11.000.
+% Given clauses 11.
+
+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 of proof ==========================
+% Redundant proof: 27 $F.  [back_rewrite(9),rewrite([22(3)]),xx(a)].
+
+% Disable descendants (x means already disabled):
+ 9x
+
+given #12 (T,wt=5): 22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
+
+given #13 (A,wt=10): 15 x * (y * inv(x * y)) = I.  [para(8(a,1),6(a,1)),flip(a)].
+
+given #14 (T,wt=4): 28 inv(I) = I.  [para(22(a,1),8(a,1))].
+
+given #15 (T,wt=8): 26 x * (inv(x) * y) = y.  [back_rewrite(14),rewrite([22(5)])].
+
+============================== PROOF =================================
+
+% Proof 2 at 0.02 (+ 0.00) seconds.
+% Length of proof is 14.
+% Level of proof is 8.
+% Maximum clause weight is 11.000.
+% Given clauses 15.
+
+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 of proof ==========================
+% Redundant proof: 33 $F.  [back_rewrite(10),rewrite([30(3)]),xx(a)].
+
+% Disable descendants (x means already disabled):
+ 10x
+
+given #16 (T,wt=5): 30 inv(inv(x)) = x.  [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)].
+
+============================== PROOF =================================
+
+% Proof 3 at 0.02 (+ 0.00) seconds.
+% Length of proof is 15.
+% Level of proof is 9.
+% Maximum clause weight is 11.000.
+% Given clauses 16.
+
+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 of proof ==========================
+% Redundant proof: 37 $F.  [back_rewrite(11),rewrite([34(4)]),xx(a)].
+
+% Disable descendants (x means already disabled):
+ 11x
+
+given #17 (T,wt=6): 34 inv(x) * x = I.  [para(30(a,1),8(a,1,2))].
+
+given #18 (A,wt=12): 25 x * (y * (inv(x * y) * z)) = z.  [back_rewrite(18),rewrite([22(7)])].
+
+given #19 (T,wt=8): 36 inv(x) * (x * y) = y.  [para(30(a,1),26(a,1,2,1))].
+
+given #20 (T,wt=9): 42 x * inv(y * x) = inv(y).  [para(15(a,1),36(a,1,2)),rewrite([7(3)]),flip(a)].
+
+given #21 (T,wt=10): 47 inv(x * y) = inv(y) * inv(x).  [para(42(a,1),36(a,1,2)),flip(a)].
+
+============================== STATISTICS ============================
+
+Given=21. Generated=238. Kept=36. proofs=3.
+Usable=11. Sos=0. Demods=10. Limbo=0, Disabled=32. Hints=0.
+Kept_by_rule=0, Deleted_by_rule=0.
+Forward_subsumed=199. Back_subsumed=0.
+Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
+New_demodulators=32 (0 lex), Back_demodulated=25. Back_unit_deleted=0.
+Demod_attempts=1855. Demod_rewrites=422.
+Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
+Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
+Megabytes=0.09.
+User_CPU=0.02, System_CPU=0.00, Wall_clock=0.
+
+============================== end of statistics =====================
+
+============================== end of search =========================
+
+SEARCH FAILED
+
+Exiting with 3 proofs.
+
+Process 13543 exit (sos_empty) Sat Jan 14 20:02:31 2017
diff --git a/part2.tex b/part2.tex
index 50296f2..6959fd3 100644
--- a/part2.tex
+++ b/part2.tex
@@ -1,16 +1,16 @@
 \documentclass[12pt]{article}
 \usepackage{a4wide}
 \usepackage{latexsym}
-\usepackage{amssymb}
+\usepackage{amsmath, amssymb}
 \usepackage{epic}
 \usepackage{graphicx}
 \usepackage{gensymb}
 \usepackage[table]{xcolor}
 \usepackage{listings}
 \usepackage{tikz}
-\usepackage{amsmath}
 \usepackage{hyperref}
 \usepackage{float}
+\usepackage{enumitem}
 %\pagestyle{empty}
 \newcommand{\tr}{\mbox{\sf true}}
 \newcommand{\fa}{\mbox{\sf false}}
@@ -317,9 +317,44 @@ 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)$.
 
-\subsubsection*{(b)}
+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)$
+\end{enumerate}
+Using the assumptions
+\begin{enumerate}[resume]
+  \item \label{itm:logic_a_2} $a(x, x) = x$
+  \item \label{itm:logic_a_3} $a(x, y) = a(y, x)$
+  \item \label{itm:logic_a_4} $a(x, a(y, z)) = a(a(x, y), z)$
+\end{enumerate}
+We do this by finding a counterexample
+\begin{enumerate}[resume]
+  \item \label{itm:logic_a_5} $\exists c1, c2 : a(c1, a(c2, a(c1, a(c2, a(c1, a(c2, c1)))))) \neq a(c1, c2)$
+\end{enumerate}
+First, apply \ref{itm:logic_a_3} to \ref{itm:logic_a_5}
+\begin{enumerate}[resume]
+  \item \label{itm:logic_a_6} $\exists c1, c2 : a(c1, a(c2, a(c1, a(c2, a(c1, a(c1, c2)))))) \neq a(c1, c2)$
+\end{enumerate}
+Then, apply \ref{itm:logic_a_2} to \ref{itm:logic_a_4}, where $x \gets x, y \gets x, z \gets y$
+\begin{enumerate}[resume]
+  \item \label{itm:logic_a_7} $a(x, a(x, y)) = a(x, y)$
+\end{enumerate}
+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$
+\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$.
+\\
+This proves that $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ indeed rewrites to $a(p, q)$.
 
+\subsubsection*{(b)}
+The first 3 properties hold for every group. The fourth property does not hold for all groups though.
 
 \section*{Problem: }
 Give a precise description of a non-trivial problem of your own choice, and