pvs results

tex/usecase.tex

@@ -105,17 +105,17 @@ Given that the same practice is used in few other systems (if any), searching fo
 We have tried the first two approaches regarding theory parameters -- i.e. the simple and covariant treatments -- to both inter- and intra-library view finding problems. Concretely, we have used a simple theory of Monoids in the Math-in-the-Middle foundation and the theory of Monoids in the NASA library as domains with the whole NASA library as target. The results are summarized in Figure \ref{fig:pvsresults}.
 
 \begin{figure}[ht]\centering
-  \begin{tabular}{l | l || c | c}
-  	\textbf{Domain} & \textbf{Normalization} & \textbf{Simple Morphisms} & \textbf{Aggregated} \\\hline
+  \begin{tabular}{l | c || c | c}
+  	\textbf{Domain} & \textbf{Normalization} & \textbf{Simple Morphisms} & \textbf{Aggregated} \\\hline\hline
   	NASA/monoid & simple & 388 & 154 \\
   	MitM/monoid & simple & 32 & 17 \\\hline
   	NASA/monoid & covariant & 1077 & 542 \\
-  	MitM/monoid & covariant & & \\
+  	MitM/monoid & covariant & 23 & 6 \\
   \end{tabular}
 \caption{Results of Inter- and Intra-Library View Finding in the PVS NASA Library}\label{fig:pvsresults}
 \end{figure}
 
-Most of the results in the simple MitM$\to$NASA case are artifacts of the theory parameter treatments -- in fact only two of the 17 results seem accurate. In the covariant case, the first $n$ results look meaningful, the rest are spurious small morphisms that can easily be automatically identified as such.
+Most of the results in the simple MitM$\to$NASA case are artifacts of the theory parameter treatments -- in fact only two of the 17 results are meaningful (to operations on sets and the theory of numberfields). In the covariant case, the more requirements of each simple morphism lead to fuller (one total) and less spurious morphisms.
 
 With a theory from the NASA library as domain, the results are already too many to be properly evaluated by hand.