Commit de2023d3 authored by Dennis Müller's avatar Dennis Müller
Browse files

reread

parent a7bd448b
......@@ -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 $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$.
\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$.
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}
......
......@@ -10,7 +10,7 @@ As an example, we present a large case study where we find view from the MitM li
PVS~\cite{pvs} is a proof assistant under active development based on a higher-order logic with a number of advanced features.
In addition to the \emph{Prelude} library, which contains the most common domains of mathematical discourse and is shipped with PVS itself, there is a large library of formal mathematics developed and maintained by NASA~\cite{PVSlibraries:on}.
In \cite{KMOR:pvs:17}, we represent PVS as a meta-theory in MMT and implemented a translator that transforms both libraries into MMT format. we use a meta-view that embeds MitM's higher-order logic into PVS's higher-order logic and make sure that we normalize PVS-formulas in the same way as MitM-formulas.
In \cite{KMOR:pvs:17}, we represent PVS as a meta-theory in MMT and implemented a translator that transforms both libraries into MMT format. We use a meta-view that embeds MitM's higher-order logic into PVS's higher-order logic and make sure that we normalize PVS-formulas in the same way as MitM-formulas.
%\begin{oldpart}{MK: this sounds like a left-over from the time we had a PVS->HOL-Light use case. I think this can just be eft out. or reduce to the last sentence and leave out the paragrpah}
%\paragraph{Formula Normalization}
......
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