@@ -23,7 +23,7 @@ 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 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 $S'$ 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'(S')$ as properties of $O$.

\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 $S'$ would make useful properties to establish about $O$, since they allow pushing out $v$ over $\iota$ to a view $v':S'\rightsquigarrow T'$(where $T'$ extends $T$ by the newly imported properties) and gain $v'(S')$ 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.