diff --git a/tex/usecase.tex b/tex/usecase.tex index f9071ade1606e65b1a12ad55521409124840cc07..192ce91a96ab91d68fa19a029b417c6af85c5e3d 100644 --- a/tex/usecase.tex +++ b/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.