Commit f1b1b4b1 by Michael Kohlhase

### Merge branch 'master' of gl.kwarc.info:oaf/alignment-finder

parents 69c78a03 fbbf0795
 ... @@ -23,7 +23,7 @@ Additionally, \emph{surjective} partial views would inform her, that her theory ... @@ -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{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'$ (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. 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. 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} \end{compactitem} ... ...
 ... @@ -10,7 +10,7 @@ As an example, we present a large case study where we find view from the MitM li ... @@ -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. 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 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} %\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} %\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!