diff options
Diffstat (limited to 'contrib/ML4PG/doc')
23 files changed, 0 insertions, 880 deletions
diff --git a/contrib/ML4PG/doc/ml4pg.v b/contrib/ML4PG/doc/ml4pg.v deleted file mode 100644 index ced9f9a4..00000000 --- a/contrib/ML4PG/doc/ml4pg.v +++ /dev/null @@ -1,659 +0,0 @@ -Inductive nat : Set := - | O : nat - | S : nat -> nat. - -Delimit Scope nat_scope with nat. - - -Fixpoint plus (n m:nat) : nat := - match n with - | O => m - | S p => S (p + m) - end - -where "n + m" := (plus n m) : nat_scope. - -Fixpoint mult (n m:nat) : nat := - match n with - | O => O - | S p => m + p * m - end - -where "n * m" := (mult n m) : nat_scope. - -Fixpoint minus (n m:nat) : nat := - match n, m with - | O, _ => n - | S k, O => n - | S k, S l => k - l - end - -where "n - m" := (minus n m) : nat_scope. - - -Require Import Coq.Lists.List. - -Variable A: Type. - -Local Notation "[ ]" := nil : list_scope. -Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope. - -Set Implicit Arguments. -Open Scope nat. - - -(*********************************************************************************************) -(* Exported theorems *) -(*********************************************************************************************) - -(*-------------------------------------------------------------------------------------------*) -(* Layer 0 : Fundamental lemmas *) -(*-------------------------------------------------------------------------------------------*) - -(*1.*) -Lemma app_nil_l : forall l:list A, [] ++ l = l. -intro l. -case l. -simpl; trivial. -intros a0 l0. -simpl; trivial. -Qed. - -(*2.*) -Theorem app_nil_l_shorter : forall l:list A, [] ++ l = l. -intro l. -simpl; trivial. -Qed. - - -(*3. alternativeApp_nil_l*) -Theorem app_nil_l_shorter' : forall l:list A, [] ++ l = l. -intro l. -simpl. -trivial. -Qed. - -(* 4 *) -Theorem app_nil_l2 : forall l: list A, l ++ [] = l. -intro l. - induction l. - simpl; trivial. - simpl. - rewrite IHl. - trivial. -Qed. - - - -(* 5 *) -Theorem app_nil_l2' : forall l: list A, l ++ [] = l. -induction l. -simpl; trivial. -simpl. -rewrite IHl. -trivial. -Qed. - -(*6.*) -Lemma mult_n_O : forall n:nat, O = n * O. -induction n. -simpl; trivial. -simpl; trivial. -Qed. - -(*7.*) -Lemma mult_O_n : forall n: nat, O = O * n. -intro. -simpl. -trivial. -Qed. - -(*8.*) - -Lemma M15_c : forall a: nat, a = S O -> (S O - a) * a = O. -intros. -rewrite H. -simpl. -trivial. -Qed. - -(*9.*) -Lemma O_minus : forall m, O-m = O. -intro. simpl. trivial. -Qed. - -(*10.*) -Lemma minus_O : forall m, m-O = m. -induction m. - trivial. -simpl; trivial. -Qed. - -(*11.*) -Lemma plus_n_O : forall n:nat, n = n + O. -induction n. - simpl; trivial. -simpl; trivial. -rewrite <- IHn. -trivial. -Qed. - -(*12.*) -Lemma plus_0_n : forall n:nat, n = O + n. -simpl; trivial. -Qed. - -(*13.*) -Lemma addSn : forall m n, S m + n = S (m + n). -trivial. -Qed. - -(*14.*) -Lemma mulSn : forall m n, S m * n = n + m * n. -trivial. Qed. - -(*15.*) -Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. -induction n. - simpl; trivial. -simpl. -intro m. -rewrite <- IHn. -trivial. -Qed. - -(*16.*) -Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). -induction n. - simpl; trivial. -simpl; trivial. -Qed. - -(*17.*) -Lemma aux10 : forall a, (S a - a) = S O. -induction a. - simpl; trivial. -simpl; trivial. -Qed. - -(*18.*) -Lemma aux12 : forall n, (n * S O) = n. -induction n. - simpl; trivial. -simpl. -rewrite IHn. -trivial. -Qed. - -(*-------------------------------------------------------------------------------------------*) -(* Layer 1 : Lemmas which use layer 0 lemmas *) -(*-------------------------------------------------------------------------------------------*) - -(*19.*) -Lemma addnS : forall m n, m + S n = S (m + n). -induction m. - trivial. -intro n. -rewrite addSn. -rewrite addSn. -rewrite IHm. -trivial. -Qed. - -(*20.*) -Lemma addnCA : forall m n k, m + (n + k) = n + (m + k). -intros m n k. -induction m. - trivial. -rewrite plus_Sn_m. -rewrite plus_Sn_m. -rewrite <- plus_n_Sm. -rewrite IHm. -trivial. -Qed. - - - -(*21.L1M*) -Lemma M1_corrected : forall l: list A, l= [] - -> tl (tl (tl l) ++ nil) = nil. -intro l. -intro H. -rewrite H. -rewrite app_nil_l2. -simpl; trivial. -Qed. - -(*22. L1Mbutwithintros *) -Lemma L1Mbutwithintros : forall l: list A, l= [] - -> tl (tl (tl l) ++ nil) = nil. -intros l H. -rewrite H. -rewrite app_nil_l2. -simpl; trivial. -Qed. - -(*23.*) -Lemma M2 : forall a: A, -tl (tl (tl ([a] ++ []))) = []. -intro. -rewrite app_nil_l2. -simpl. -trivial. -Qed. - -(*24. L31Mintroal*) -Lemma M3_1: forall (a: nat) (l :list nat), (hd O (a :: l)) * O = O. -intro a. -intro l. -rewrite <- mult_n_O. -trivial. -Qed. - -(* 25. L31M*) -Lemma L31M : forall (a: nat) (l :list nat), (hd O (a :: l)) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - -(* 26. L31Mextrasimpl *) -Lemma L31Mextrasimpl : forall (a: nat) (l :list nat), (hd O (a :: l)) * O = O. -intros. -simpl. -rewrite <- mult_n_O. -trivial. -Qed. - -(*Many profs below follow that exact scheme with reduction of *, but it would be completely different strategies if reduction was first made in lists...*) - -(*27. L32M*) -Lemma M3_2 : forall (a: nat) (l :list nat), l= [a] -> (hd O [a]) * O = O. -intro a. -intro l. -intro H. -rewrite <- mult_n_O. -trivial. -Qed. - -(*28. L32Mlessintro *) -Lemma L32Mlessintro : forall (a: nat) (l :list nat), l= [a] -> (hd O [a]) * O = O. -intro a. -intro l. -rewrite <- mult_n_O. -trivial. -Qed. - - -(* 29. L32Mintros *) -Lemma L32Mintros : forall (a: nat) (l :list nat), l= [a] -> (hd O [a]) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - - -Definition hdn (l:list nat) := - match l with - | nil => O - | cons x _ => x - end. - -(*30*) -Lemma M3_3: forall (a: nat) (l :list nat), l= [a] -> (hdn [a]) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - -(*31*) -Lemma M3_4: forall a: nat, (hd O ([a] ++ [])) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - - -(*32*) -Lemma M4: forall a: nat, hd O ([a] ++ [a]) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - - -(*33*) -Lemma M8: forall (a b : nat), hd O [a] * O * b = O. -(* This alone does not work: intros; simpl; auto.*) -intros. -rewrite <- mult_n_O. -trivial. -Qed. - - -(*34*) -Lemma M16: forall a: nat, (S a - a) * O = O. -intros. rewrite <- mult_n_O. trivial. -Qed. - -(*35*) -Lemma M10: forall a: nat, a * S O * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - -(*36*) -Lemma M13: forall a b : nat, a * hd O [b] * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - -(*37*) -Lemma M14 : forall a: nat, (hd O [a] + O) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - -(*38*) -Lemma M17 : forall a b: nat, (S a - b) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - -(*39*) -Lemma M18 : forall (a b :nat), ((hd O [a]) - b) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - -(*40*) -Lemma M18' : forall (a: list nat)(b:nat), (hd O a - b) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - -(*41*) -Lemma M19 : forall a:nat, (O - hd O [a]) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - -(*42*) -Lemma M20 : forall a b:nat, (O - hd O [a]) * b =O. -intros. rewrite O_minus. trivial. -Qed. - -(*43*) -Lemma M21 : forall (a :nat) (b: list nat), (a - hd O b) * O = O. -intros. -rewrite <- mult_n_O. -trivial. -Qed. - -(*44*) -Lemma M22 : forall a: nat, a * O * S O = O. -intros. -rewrite <- mult_n_O. -rewrite <- mult_O_n. -trivial. -Qed. - -(*45*) -Lemma M24 : forall a: nat, (O - a) * S O = O. -intro. -rewrite O_minus. -rewrite <- mult_O_n. -trivial. -Qed. - -(*46*) -Lemma M25 : forall a:nat, -(O - a) * S a = O. -intro. -rewrite O_minus. -rewrite <- mult_O_n. -trivial. -Qed. - -(*47*) -Lemma M26 : forall a b: nat, (O - a) * S b = O. -intros. -rewrite O_minus. -rewrite <- mult_O_n. -trivial. -Qed. - -(*48*) -Lemma aux7 : forall a:nat, a-a = O. -induction a. -rewrite O_minus. -trivial. -rewrite <- IHa. -trivial. -Qed. - - -(*49*) -Lemma M31 : forall a b, hd O a * (b * O) = O. -intros. -rewrite <- mult_n_O. -rewrite <- mult_n_O. -trivial. -Qed. - - - -(*50*) -Lemma M32 : forall a b, hd O a * (O - b) = O. -intros. -rewrite O_minus. -rewrite <- mult_n_O. -trivial. -Qed. - - -(*51.*) -Lemma aux11 : forall n, (S O * n) = n. -induction n. - simpl; trivial. -simpl. -rewrite <- plus_n_O. -trivial. -Qed. - -(*52*) -Lemma M36 : forall a, a * S (a * O) = a. -intro. rewrite <- mult_n_O. -rewrite aux12. trivial. -Qed. - -(*53*) -Lemma M37 : forall a b, a * S (b * O) = a. -intros. rewrite <- mult_n_O. -rewrite aux12. trivial. -Qed. - -(*54*) -Lemma M38 : forall a, a * S (O - a) = a. -intro. rewrite O_minus. -rewrite aux12. -trivial. -Qed. - -(*55*) -Lemma M39 : forall a, a * S (a - a) = a. -intro. rewrite aux7. rewrite aux12. trivial. -Qed. - -(*56*) -Lemma M40 : forall a, a * (S a - a) = a. -intro. rewrite aux10. -rewrite aux12. trivial. -Qed. - -(*57*) -Lemma M41 : forall a b, a * (O - hd O b) = O. -intros. rewrite O_minus. -rewrite <- mult_n_O. trivial. -Qed. - -(*58*) -Lemma M42 : forall a, hd O a * O + O = O. -intro. rewrite <- plus_n_O. -rewrite <- mult_n_O. trivial. -Qed. - -(*59*) -Lemma M43 : forall a b, hd O a * O + b = b. -intros. -rewrite <- mult_n_O. -simpl; trivial. -Qed. - -(*60*) -Lemma M44 : forall a, a * S O + O = a. -intro. rewrite aux12. -rewrite <- plus_n_O. trivial. -Qed. - -(*-------------------------------------------------------------------------------------------*) -(* Layer 2 : Lemmas which use layer 1 lemmas *) -(*-------------------------------------------------------------------------------------------*) - - - - -(*61*) -Lemma mulnS : forall n m, n * S m = n + n * m. -induction n. - trivial. intro m. -rewrite mulSn. rewrite mulSn. rewrite addSn. rewrite addSn. rewrite addnCA. -rewrite IHn. trivial. -Qed. - -(*62*) -Lemma M27 : forall a, (a - a) * S O = O. -(*intros; simpl; auto. will not work *) -intro. -rewrite aux7. -rewrite <- mult_O_n. -trivial. -Qed. - -(*63*) - (*Same proof*) -Lemma M28 : forall a, (a - a) * S a = O. -intro. -rewrite aux7. -rewrite <- mult_O_n. -trivial. -Qed. - -(*64*) -Lemma M29 : forall a b, (a - a) * S b = O. -intros. -rewrite aux7. -rewrite <- mult_O_n. -trivial. -Qed. - -(*65*) -Lemma M30 : forall a b, (a - a) * hd O b = O. -intros. -rewrite aux7. -rewrite <- mult_O_n. -trivial. -Qed. - -(*66*) -Lemma M33 : forall a b, hd O a * (b - b) = O. -intros. -rewrite aux7. -rewrite <- mult_n_O. -trivial. -Qed. - -(*67*) -Lemma M34 : forall a:nat, (S a - a) * a = a. -intro. rewrite aux10. -rewrite aux11. trivial. -Qed. - -(*68*) -Lemma M35 : forall a b, (S a - a) * b = b. -intros. rewrite aux10. -rewrite aux11. trivial. -Qed. - - -(*-------------------------------------------------------------------------------------------*) -(* Layer 3 : Lemmas which use layer 1 lemmas *) -(*-------------------------------------------------------------------------------------------*) - - -(*69*) -Lemma M23 : forall a: nat, (a + O) * S O = a. -intro. -rewrite <- plus_n_O. -rewrite mulnS. -rewrite <- mult_n_O. -rewrite <- plus_n_O. -trivial. -Qed. - -(*********************************************************************************************) -(*********************************************************************************************) -(*********************************************************************************************) - - -(*-------------------------------------------------------------------------------------------*) - (* Lemmas to look for similarities *) -(*-------------------------------------------------------------------------------------------*) - - - -Definition hdb (l:list bool) := - match l with - | nil => false - | cons x _ => x - end. - -(*58*) - -Lemma andb_false_r : forall (a : bool) , false = andb a false. -Proof. -intros. -case a. - simpl; trivial. -simpl; trivial. -Qed. - -Lemma M3_3b: forall (a: bool) (l :list bool), l= [a] -> andb (hdb [a]) false = false. -Proof. -intros. -rewrite <- andb_false_r. - - - - - - - -Lemma aux7_bis: forall a:nat, a-a = O. -Proof. -induction a. - simpl; trivial. - - - - - - - diff --git a/contrib/ML4PG/doc/ml4pg_manual.pdf b/contrib/ML4PG/doc/ml4pg_manual.pdf Binary files differdeleted file mode 100644 index c13f6801..00000000 --- a/contrib/ML4PG/doc/ml4pg_manual.pdf +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/algorithm1.png b/contrib/ML4PG/doc/src/images/algorithm1.png Binary files differdeleted file mode 100644 index 8c8f47b5..00000000 --- a/contrib/ML4PG/doc/src/images/algorithm1.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/algorithm2.png b/contrib/ML4PG/doc/src/images/algorithm2.png Binary files differdeleted file mode 100644 index 6b5e0835..00000000 --- a/contrib/ML4PG/doc/src/images/algorithm2.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/clusters1.png b/contrib/ML4PG/doc/src/images/clusters1.png Binary files differdeleted file mode 100644 index ca4ef219..00000000 --- a/contrib/ML4PG/doc/src/images/clusters1.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/clusters1pg.png b/contrib/ML4PG/doc/src/images/clusters1pg.png Binary files differdeleted file mode 100644 index b39d409f..00000000 --- a/contrib/ML4PG/doc/src/images/clusters1pg.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/clusters2.png b/contrib/ML4PG/doc/src/images/clusters2.png Binary files differdeleted file mode 100644 index f091abbe..00000000 --- a/contrib/ML4PG/doc/src/images/clusters2.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/clusters2pg.png b/contrib/ML4PG/doc/src/images/clusters2pg.png Binary files differdeleted file mode 100644 index 6ba6dcb4..00000000 --- a/contrib/ML4PG/doc/src/images/clusters2pg.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/export.png b/contrib/ML4PG/doc/src/images/export.png Binary files differdeleted file mode 100644 index de048b47..00000000 --- a/contrib/ML4PG/doc/src/images/export.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/fig1.png b/contrib/ML4PG/doc/src/images/fig1.png Binary files differdeleted file mode 100644 index 955fd048..00000000 --- a/contrib/ML4PG/doc/src/images/fig1.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/fig1pg.png b/contrib/ML4PG/doc/src/images/fig1pg.png Binary files differdeleted file mode 100644 index d4a0df9f..00000000 --- a/contrib/ML4PG/doc/src/images/fig1pg.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/fig2.png b/contrib/ML4PG/doc/src/images/fig2.png Binary files differdeleted file mode 100644 index ed8c399e..00000000 --- a/contrib/ML4PG/doc/src/images/fig2.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/fig3.png b/contrib/ML4PG/doc/src/images/fig3.png Binary files differdeleted file mode 100644 index f3741a0e..00000000 --- a/contrib/ML4PG/doc/src/images/fig3.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/fig4.png b/contrib/ML4PG/doc/src/images/fig4.png Binary files differdeleted file mode 100644 index 9df097bd..00000000 --- a/contrib/ML4PG/doc/src/images/fig4.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/fig5.png b/contrib/ML4PG/doc/src/images/fig5.png Binary files differdeleted file mode 100644 index 733a3d22..00000000 --- a/contrib/ML4PG/doc/src/images/fig5.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/frequencies.png b/contrib/ML4PG/doc/src/images/frequencies.png Binary files differdeleted file mode 100644 index 4f90b5fc..00000000 --- a/contrib/ML4PG/doc/src/images/frequencies.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/granularity.png b/contrib/ML4PG/doc/src/images/granularity.png Binary files differdeleted file mode 100644 index 385b3972..00000000 --- a/contrib/ML4PG/doc/src/images/granularity.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/levels.png b/contrib/ML4PG/doc/src/images/levels.png Binary files differdeleted file mode 100644 index 48e02db7..00000000 --- a/contrib/ML4PG/doc/src/images/levels.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/ml_system1.png b/contrib/ML4PG/doc/src/images/ml_system1.png Binary files differdeleted file mode 100644 index f11cebf1..00000000 --- a/contrib/ML4PG/doc/src/images/ml_system1.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/images/ml_system2.png b/contrib/ML4PG/doc/src/images/ml_system2.png Binary files differdeleted file mode 100644 index 792c423d..00000000 --- a/contrib/ML4PG/doc/src/images/ml_system2.png +++ /dev/null diff --git a/contrib/ML4PG/doc/src/ml4pg_manual.bib b/contrib/ML4PG/doc/src/ml4pg_manual.bib deleted file mode 100644 index 07dcb4ba..00000000 --- a/contrib/ML4PG/doc/src/ml4pg_manual.bib +++ /dev/null @@ -1,12 +0,0 @@ -@Article{KHG12, - author = {E. Komendantskaya and J. Heras and G. Grov}, - title = {Machine Learning in Proof General: interfacing interfaces}, - year = {2012}, -} - - -@Article{HK13, - author = {J. Heras and E. Komendantskaya}, - title = {ML4PG Case studies}, - year = {2013}, -}
\ No newline at end of file diff --git a/contrib/ML4PG/doc/src/ml4pg_manual.pdf b/contrib/ML4PG/doc/src/ml4pg_manual.pdf Binary files differdeleted file mode 100644 index c13f6801..00000000 --- a/contrib/ML4PG/doc/src/ml4pg_manual.pdf +++ /dev/null diff --git a/contrib/ML4PG/doc/src/ml4pg_manual.tex b/contrib/ML4PG/doc/src/ml4pg_manual.tex deleted file mode 100644 index 2eb92b7e..00000000 --- a/contrib/ML4PG/doc/src/ml4pg_manual.tex +++ /dev/null @@ -1,209 +0,0 @@ -\documentclass[10pt]{article} - - -\usepackage[utf8]{inputenc} - -\usepackage{hyperref} -\usepackage{graphicx} -\usepackage{amssymb} -\usepackage{color} -\usepackage{listings} -\usepackage{tikz} -\usepackage{verbatim} -\usepackage{theorem} - - - -\begin{document} - -\title{ML4PG: Machine learning for Proof General} -\author{J\'onathan Heras and Ekaterina Komendantskaya\\ -\{jonathanheras,katya\}@computing.dundee.ac.uk} - \maketitle - - - -\tableofcontents - - -\section{Using ML4PG} - - -To illustrate the use of ML4PG, we will use the file \verb"ml4pg.v" which can be find in the same folder of this manual. -This file contains various lemmas about natural numbers and lists. - -\subsection{Getting started} - -Open the file \verb"ml4pg.v" using emacs. The Proof General interface is the usual one, but it includes a new option in the Coq menu -called ML4PG. - -\begin{figure} - \centering - \includegraphics[scale=0.4]{images/fig1pg.png} - \caption{Proof General with the ML4PG option.}\label{fig1} -\end{figure} - -If you select this option, the interface asks you if you are developing your proofs using the plain Coq style or the SSReflect style, in this case we select the Coq mode (c). -Subsequently, the interface asks you if you want to extract the information associated with the lemmas which have been previously developed in this library. In this case, -we select no (c). Once that this is done, the Proof General interface is extended with a new menu called \emph{Statistics} and two buttons, see Figure~\ref{fig3}. - -\begin{figure} - \centering - \includegraphics[scale=0.4]{images/fig3.png} - \caption{ML4PG interface with all the options active.}\label{fig3} -\end{figure} - - -\subsection{Extracting feature vectors} - -Feature vectors can be extracted in two different ways: - -\begin{itemize} - \item During the development of the proofs. To this aim, you have to use the shortcut Ctrl-C Ctrl-M to process the next proof command. - \item Several proofs at the same time. If you want to extract the feature vectors of several proofs, go to the last proof and use the shortcut Ctrl-C Space. - You can also use the \emph{Extract info up to point} option of the statistics menu. -\end{itemize} - -Go to the end of \verb"emacs ml4pg.v" file; there, you can see two unfinished proofs: \verb"M3_3b" and \verb"aux7_bis". Put the cursor at the end of -the proof of Lemma \verb"andb_false_r" and use the shortcut Ctrl-C Space or the \emph{Extract info up to point} option of the statistics menu. In this -way the information associated with each proof will be extracted and you will be able to use it to obtain proof clusters (groups of similar proofs). - -Now, let us explain the functionality of the options included in the Statistics menu. - -\subsection{Configuration menu} - -The different options to configure the Machine-learning environments were detailed in~\cite{KHG12}. All those options can be accessed from the Configuration -submenu of the Statistics menu, see Figure~\ref{fig3}. - - - -\paragraph{Algorithms:} - -The user can select different algorithms to obtain proof similarities (all of them behave similar, see~\cite{HK13}). -ML4PG offers different algorithms, see Figure~\ref{algorithms}. - -In the case of MATLAB; there are three algorithms available: K-means and Gaussian. In the case of Weka, the algorithms -which are available are: K-means, EM and FarthestFirst. - -\begin{figure} - \centering - \includegraphics[scale=0.4]{images/algorithm2.png} - \caption{The ML algorithms menu.}\label{algorithms} -\end{figure} - -\paragraph{Granularity:} - -In the machine learning literature, there exists a number of heuristics to determine this optimal number of clusters. -We used them as an inspiration to formulate our own algorithm for ML4PG, tailored -to the interactive proofs. It takes into consideration the size of the proof library and an auxiliary parameter - -- called granularity. This parameter is used to calculate the optimal number of -proof clusters, the process to calculate this optimal number was described in~\cite{KHG12}. The user decides the -granularity in ML4PG menu (see Figure~\ref{granularity}), by selecting a value between 1 and 5, where 1 stands for a -low granularity (producing big and general clusters) and 5 stands for a high granularity (producing small -and precise clusters). - - -\begin{figure} - \centering - \includegraphics[scale=0.4]{images/granularity.png} - \caption{ML4PG granularity menu.}\label{granularity} -\end{figure} - - - -\paragraph{Frequencies:} - -Clustering techniques divide data into n groups of similar objects (called clusters), where the value of -n is a ``learning'' parameter provided by the user together with other inputs to the clustering algorithms. -Increasing the value of n means that the algorithm will try to separate objects into more classes, and, as a -consequence, each cluster will contain examples with higher correlation. The frequencies of clusters can -serve for analysis of their reliability. Results of one run of a clustering algorithm may differ from another, -even on the same data set. This is due to the fact that clustering algorithms randomly choose examples -to start from, and then, form clusters relative to those examples. However, it may happen that certain -clusters are found repeatedly – and frequently – in different runs; then, we can use these frequencies to -determine the reliable clusters. The frequencies can be determined using the threshold presented in Figure~\ref{frequencies}, -a detailed description of this parameter was given in~\cite{KHG12}. - - -\begin{figure} - \centering - \includegraphics[scale=0.4]{images/frequencies.png} - \caption{ML4PG frequencies menu.}\label{frequencies} -\end{figure} - - -\subsection{Show clusters} - -The option \emph{Show Clusters} of the Statistics menu shows clusters when a library is clustered -irrespective of the current proof goal. An example using the \verb"ml4pg.v" library with the options: - -\begin{itemize} - \item Algorithm: K-means, - \item Granularity: 3, - \item Frequencies: 1. -\end{itemize} - -\noindent is shown in Figure~\ref{clusters1}. - -\begin{figure} - \centering - \includegraphics[scale=0.23]{images/clusters1pg.png} - \caption{Clusters for the ml4pg library. The Proof General window has been split into two windows positioned side by -side: the left one keeps the current proof script, and the right one shows the clusters. If the user clicks -on the name of a theorem showed in the right screen, such a window is split horizontally and a brief description of the selected -theorem is shown.}\label{clusters1} -\end{figure} - -This functionality can also invoked using the second right most button of the Proof General toolbar. - -\subsection{Show similar theorems} - -The example above shows one mode of working with ML4PG: that is, when a library is clustered -irrespective of the current proof goal. However, it may be useful to use this technology to aid the interactive -proof development. In which case, we can cluster libraries relative to a few initial proof steps for the -current proof goal. An example using the \verb"ml4pg.v" library with the options: - -\begin{itemize} - \item Algorithm: FarthestFirst, - \item Granularity: 2, - \item Frequencies: 2. -\end{itemize} - -\noindent and with the few steps included about the proof of \verb"M3_3b" is shown in Figure~\ref{clusters2}. - - -\begin{figure} - \centering - \includegraphics[scale=0.23]{images/clusters2pg.png} - \caption{On the right side, several suggestions provided by ML4PG. If the user clicks on the name of one of the -suggested lemmas, a brief description about it is shown.}\label{clusters2} -\end{figure} - -This functionality can also invoked using the right most button of the Proof General toolbar. - -\subsection{Export Library} - -Using the Export library option, the user can export the library for further use (see Figure~\ref{export}) with the -Available libraries for clustering option. - - -\begin{figure} - \centering - \includegraphics[scale=0.4]{images/export.png} - \caption{ML4PG export menu.}\label{export} -\end{figure} - - - - - - - - - - -\bibliographystyle{plain} -\bibliography{ml4pg_manual} - - -\end{document} |
