applications.tex 3.49 KB
Newer Older
Dennis Müller's avatar
Dennis Müller committed
1
2
3
\begin{newpart}{DM}
We have seen how a viewfinder can be used for theory \emph{discovery} and finding constants with specific desired properties, but many other potential use cases are imaginable. The main problems to solve with respect to these is less about the algorithm or software design challenges, but user interfaces.

Dennis Müller's avatar
Dennis Müller committed
4
The theory discovery use case described in Sec. \ref{sec:usecase} is mostly desirable in a setting where a user is actively writing or editing a theory, so the integration in jEdit is sensible. However, the across-library use case in Sec. \ref{sec:pvs} already would be a lot more useful in a theory exploration setting, such as when browsing available archives on MathHub~\cite{mathhub} or in the graph viewer integrated in \mmt ~\cite{RupKohMue:fitgv17}. Additional specialized user interfaces would enable or improve the following use cases:
Dennis Müller's avatar
Dennis Müller committed
5
\end{newpart}
Dennis Müller's avatar
Update    
Dennis Müller committed
6
\begin{itemize}
Dennis Müller's avatar
Dennis Müller committed
7
	\item \textbf{Model-/Countermodel Finding:} If the codomain of a view is a theory representing a specific model, it would tell her that those
Dennis Müller's avatar
Update    
Dennis Müller committed
8
9
10
11
12
		are \emph{examples} of her abstract theory.
		
		Furthermore, partial views -- especially those that are total on some included theory -- could
		be insightful \emph{counterexamples}.
	
Dennis Müller's avatar
Dennis Müller committed
13
	\item \textbf{Library Refactoring:} Given that the Viewfinder looks for \emph{partial} views, we can use it to find natural
Dennis Müller's avatar
Update    
Dennis Müller committed
14
15
16
17
18
19
20
21
		extensions of a starting theory. Imagine Jane removing the last of her axioms for ``beautiful sets'' --
		the other axioms (disregarding finitude of her sets) would allow her to find e.g. both Matroids and
		\emph{Ideals}, which would suggest to her to refactor her library accordingly.
		
		Additionally, \emph{surjective} partial views would inform her, that her theory would probably better
		be refactored as an extension of the codomain, which would allow her to use all theorems and definitions
		therein.
		
Dennis Müller's avatar
Dennis Müller committed
22
	\item \textbf{Theory Generalization:} If we additionally consider views into and out of the theories found, this can make theory discovery even 
Dennis Müller's avatar
Update    
Dennis Müller committed
23
24
25
		more attractive. For example, a view from a theory of vector spaces intro matroids could inform Jane additionally, 
		that her beautiful sets, being matroids, form a generalization of the notion of linear independence in linear algebra.
		
Dennis Müller's avatar
Dennis Müller committed
26
	\item \textbf{Folklore-based Conjecture:} If we were to keep book on our transfomations during preprocessing and normalization, we could use the found
Dennis Müller's avatar
Update    
Dennis Müller committed
27
28
29
30
31
32
33
		views for translating both into the codomain as well as back from there into our starting theory.
		
		This would allow for e.g. discovering and importing theorems and useful definitions from some other library -- 
		which on the basis of our encodings can be done directly by the viewfinder.
		
		A useful interface might specifically prioritize views into theories on top of which there are many
		theorems and definitions that have been discovered.
Michael Kohlhase's avatar
Michael Kohlhase committed
34
\end{itemize}
Dennis Müller's avatar
Dennis Müller committed
35
For some of these use cases it would be advantageous to look for views \emph{into} our working theory instead. 
Dennis Müller's avatar
Update    
Dennis Müller committed
36
			
Michael Kohlhase's avatar
merge    
Michael Kohlhase committed
37
38
Note that even though the algorithm is in principle symmetric, some aspects often depend on the direction -- e.g. how we preprocess the theories,	which constants we use as starting points or how we treat and evaluate the resulting (partial) views (see Sections \ref{sec:algparams}, \ref{sec:normalizeintra} and \ref{sec:normalizeinter}).

Michael Kohlhase's avatar
Michael Kohlhase committed
39
40
%%% Local Variables:
%%% mode: latex
41
%%% eval: (visual-line-mode) (set-fill-column 5000)
Michael Kohlhase's avatar
Michael Kohlhase committed
42
43
%%% TeX-master: "paper"
%%% End:
44
45
46

%  LocalWords:  emph specialized generalization transfomations normalization prioritize
%  LocalWords:  sec:usecase