Commit 50d3776c authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

better explanation of the folklore

parent 6563def3
......@@ -23,8 +23,8 @@ Additionally, \emph{surjective} partial views would inform her, that her theory
%
\item \textbf{Theory Generalization:} If we additionally consider views into and out of the theories found, this can make theory discovery even 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.
%
\item \textbf{Folklore-based Conjecture:} If we were to keep book on our transformations during preprocessing and normalization, we could use the found 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 view finder.
\item \textbf{Folklore-based Conjecturing:} If we have theory $T$ describing (the properties of) a class $O$ of objects under consideration and a view $v:S\rightsquigarrow T$, then we can use extensions of $S'$ in $\cL$ with $\iota: S\hookrightarrow S'$ for making conjectures about $O$: The $v$-images of the local axioms of $T'$ would make useful properties to establish about $O$, since they allow pushing out $v$ over $\iota$ to a view $v':S'\rightsquigarrow T'$ and gain $v'(T')$ as properties of $O$.
Note that we would need to keep book on our transformations during preprocessing and normalization, so that we could use the found views for translating both into the codomain as well as back from there into our starting theory.
A useful interface might specifically prioritize views into theories on top of which there are many theorems and definitions that have been discovered.
\end{compactitem}
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 aggregate and evaluate the resulting (partial) views (see Sections \ref{sec:algparams}, \ref{sec:normalizeintra} and \ref{sec:normalizeinter}).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment