Clean up file structure and add overview file

source/casestudies/2023-cade/MMT prover output/$Predicate$Example.ax

@@ -10,5 +10,5 @@ thf(c_2_tp_ax, axiom, (((a_rel @ $false) @ t_c_2) @ t_c_2)).
 thf(ax0_ax, axiom, (! [V_X:t_a]: (((((a_rel @ $true) @ V_X) @ V_X) => (((a_rel @ $true) @ V_X) @ t_c_0))))).
 thf(p_type, type, t_p: (t_a > $o)).
 thf(p_tp_ax, axiom, (! [V_X:t_a,V_X_PRIME:t_a]: (((((a_rel @ $false) @ V_X) @ V_X_PRIME) => ((t_p @ V_X) = (t_p @ V_X_PRIME)))))).
-thf(ax1_ax, axiom, t_p(t_c_1)).
-thf(ax2_ax, axiom, (~ (t_p(t_c_2)))).
+thf(ax1_ax, axiom, (t_p @ t_c_1)).
+thf(ax2_ax, axiom, (~ ((t_p @ t_c_2)))).

source/casestudies/2023-cade/MMT prover output/$Predicate$Example.p

@@ -10,6 +10,6 @@ thf(c_2_tp_ax, axiom, (((a_rel @ $false) @ t_c_2) @ t_c_2)).
 thf(ax0_ax, axiom, (! [V_X:t_a]: (((((a_rel @ $true) @ V_X) @ V_X) => (((a_rel @ $true) @ V_X) @ t_c_0))))).
 thf(p_type, type, t_p: (t_a > $o)).
 thf(p_tp_ax, axiom, (! [V_X:t_a,V_X_PRIME:t_a]: (((((a_rel @ $false) @ V_X) @ V_X_PRIME) => ((t_p @ V_X) = (t_p @ V_X_PRIME)))))).
-thf(ax1_ax, axiom, t_p(t_c_1)).
-thf(ax2_ax, axiom, (~ (t_p(t_c_2)))).
-thf(conjecture, conjecture, $false).
\ No newline at end of file
+thf(ax1_ax, axiom, (t_p @ t_c_1)).
+thf(ax2_ax, axiom, (~ ((t_p @ t_c_2)))).
+thf(conjecture, conjecture, (t_p @ t_c_2)).
\ No newline at end of file

source/casestudies/2023-cade/MMT_example_problems/predicate_exam.mmt

@@ -17,7 +17,7 @@ theory PredicateExample : latin:/?DHOL =
     	(f @ c_0 =ͭ g @ c_0) ⇒ͩ [p] f =ͭ g ❙
  
     /T The following should NOT be provable❙
-    conj: ⊦ false ❘ = PROVE ❙
+    // conj: ⊦ false ❘ = PROVE ❙
 		/T Or equivalently: ❙
-    // conj2: ⊦ p @ c_2 ❘ = PROVE ❙
+    conj2: ⊦ p @ c_2 ❘ = PROVE ❙
 ❚

source/casestudies/2023-cade/overview.txt

+At the moment there are 13 positive and one negative example (a false conjecture) for the translation based DHOL hammer.
+Some of the examples are in TPTP DHOL, some are written in MMT.
+  
+There are 6 positive examples in TPTP DHOL, 5 of them in the file DHOL_TPTP_example_problems/category-theory-lemmas.p and one in the file DHOL_TPTP_example_problems/function-composition-lemma.p. For the translations of the 5 category theory lemmas we give detailed test results for 13 different HOL ATPs in the file test-results-category-theory-lemmas.txt.
+
+There are 7 positive examples in MMT DHOL, 6 of them in the file MMT_example_problems/functions.mmt and one in the file MMT_example_problems/cat.mmt. For the translations of the 6 function composition lemmas we give detailed test results for the same 13 HOL ATPs in the file test-results-function-composition-lemmas.txt.
+There is also a false conjecture in the file MMT_example_problems/predicate_exam.mmt whoose translation indeed cannot be solved by any of the 13 HOL ATPs. 
+
+Out of the 11 different (two lemmas are given in both TPTP DHOL and MMT DHOL) positive examples only one has a translation that cannot be proven by some ATP. One of the ATPs (Vampire) proved 9 out of 11 of these lemmas. This indicates that our translation could be quite useful in practise.