Skip to content
Snippets Groups Projects
Commit 36810378 authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

finishing my pass over the paper

parent 4b9cfd34
Branches
No related tags found
No related merge requests found
......@@ -99,7 +99,7 @@ We call $\overline{G}$ the \emph{induced theory graph}.
A key aspect of \mmt is that it's URI language is expressive enough to produce URIs for
the induced statements that are not only unique but also informative. Specifically, we
can compute the induced knowledge entities from the induced theory graph by their URI and
the original graph alone, and furthermore, we can generate explainations for the existence
the original graph alone, and furthermore, we can generate explanations for the existence
of each induced statement in terms of the original theory graph. We call this property of
\mmt URIs \emph{information completeness}.
......@@ -108,3 +108,5 @@ of each induced statement in terms of the original theory graph. We call this pr
%%% TeX-master: "paper"
%%% End:
% LocalWords: mmt RabKoh textbf emph cn rightarrow llquote llquote ldots itemize
......@@ -56,7 +56,7 @@ the realms. We regard these two systems as initial case studies that show what
literate MKM could look like only; more case studies are certainly needed and more forms
of induced knowledge need to be identified.
We will introduce the two forms of induced knoweldge in the next two sections: Section
We will introduce the two forms of induced knowledge in the next two sections: Section
\ref{sec:ind} interprets the knowledge space as a \mmt \cite {project:mmt,RabKoh:WSMSML13} theory graph, the induced
statements are computed by flattening (see Section~\ref{sec:flat}). The realms case study
is presented in Section~\ref{sec:realms}, where we discuss how realm faces (induced
......@@ -76,4 +76,4 @@ formalizations. Section~\ref{sec:concl} concludes the paper.
% LocalWords: palai11 ednote emph textbf concl inparaenum frac circ wrapfigure vspace
% LocalWords: tikzpicture lightgray footnotesize defemph flatsearch KohKoh sifemp09
% LocalWords: CarFarKoh rsckmt14
% LocalWords: CarFarKoh rsckmt14 recognizing monoid axiomatized formalizations
......@@ -22,14 +22,12 @@ $\mathsf{a}\kern-.1em/\kern-.2em\circ$.
Furthermore, morphisms can carry an assignment which maps symbols and axioms from the
source theory to terms in the target theory. We see this in the view $\mathsf{e}$ from
\textsf{Monoid} to \textsf{NatArith}, which assigns $\mathbf{N}$ to the base set $G$,
multiplication ($\cdot$) to $\circ$ and the number $1$ to the unit $e$. Due to the
theory morphism property, $\mathsf{e}$ also contains proofs for all \textsf{Monoid} axioms
in \textsf{NatArith}.
It is a special feature of {\mmt} that assignments can also map morphisms into the source
theory to morphisms into the target theory. We use this to specify the morphism
$\mathsf{c}$ modularly (in particular, this allows to re-use the proofs from $\mathsf{e}$
and $\mathsf{c}$).
multiplication ($\cdot$) to $\circ$ and the number $1$ to the unit $e$. To satisfy the
obligations of the theory morphism property, $\mathsf{e}$ also contains proofs for all
\textsf{Monoid} axioms in \textsf{NatArith}. It is a special feature of {\mmt} that
assignments can also map morphisms into the source theory to morphisms into the target
theory. We use this to specify the morphism $\mathsf{c}$ modularly (in particular, we can
re-use the proofs from $\mathsf{e}$ and $\mathsf{c}$).
Note that already in this small graph, there are a lot of induced statements. For
instance, the associativity axiom is inherited in seven times (via inclusions; twice into
......@@ -40,7 +38,7 @@ estimation), then we obtain a number of induced statements that is an order of m
higher.
Another crucial ingredient of {\mmt} for the endeavor of searching for induced statements
Another crucial ingredient of {\mmt} for the endeavour of searching for induced statements
is the fact that, as discussed in Section \ref{sec:ind}, {\mmt} URIs are expressive enough
to supply names for all induced statements. In fact, we can already access the induced
statements in Figure~\ref{fig:elal-graph} in \mmt. For example, if we take $u$ to be the URI of the theory graph, the
......@@ -51,8 +49,9 @@ have the induced statements explicitly represented.
\paragraph{Generating Induced Statements}
We already hinted in section \ref{sec:ind} that generating the induced statements is a \emph{theory graph operation}
i.e. it takes a theory graph as input and returns a different one, specifically the induced theory graph.
We already hinted in Section \ref{sec:ind} that generating the induced statements is a
\emph{theory graph operation} i.e. it takes a theory graph as input and returns a
different one, specifically the induced theory graph.
Below, we define theory graph flattening as an instance of such a generation procedure that produces those
statements induced by framing.
......@@ -71,7 +70,7 @@ Given a theory graph \cn{G} the flattening of a theory \cn{T} in \cn{G} is a the
\end{definition}
The URIs of the induced declarations are based on the definition of {\mmt} URIs from
section \ref{sec:ind} (see also the \cn{assoc} example above) and permit recovering the origin of
Section \ref{sec:ind} (see also the \cn{assoc} example above) and permit recovering the origin of
the induced declarations (i.e. are \emph{information complete} as defined in \ref{sec:ind}).
Specifically, symbol declarations from \cn{T} or imported in \cn{T} by
the meta or an include preserve their name. Meanwhile symbol declarations imported in \cn{T} by a
......@@ -79,17 +78,17 @@ structure or induced by a view are additionally qualified with the name of that
or view.
\begin{definition}
The flattening of theory graph \cn{G} is a theory graph \cn{\overline{\gamma}} with the
The flattening of theory graph \cn{G} is a theory graph \cn{\overline{G}} with the
same URI as \cn{G} containing the following module declarations :
\begin{itemize}
\item for every theory \cn{T} in \cn{G} the theory \cn{\overline{T}}
\item every view \cn{v : S \rightarrow T} in \cn{G}
\item for every view \cn{v : S \rightarrow T} in \cn{G}, there is a view
\cn{\overline{v} : \overline{S} \rightarrow \overline{T}}
\end{itemize}
\end{definition}
Note that, since theory flattening preserves theory URIs and doesn't add new axioms (only
new theorems) any view from \cn{S} to \cn{T} is also a view from \cn{\overline{S}} to
\cn{\overline{T}} so the views in \cn{\overline{\gamma}} are still valid.
new theorems) we can chose \cn{\overline{v}} with the same assignments as the
corresponding view \cn{v} from \cn{S} to \cn{T}.
% \begin{oldpart}{rewrite this}
% An important observation is that the flattening operation for theory graphs is not
......@@ -111,4 +110,5 @@ new theorems) any view from \cn{S} to \cn{T} is also a view from \cn{\overline{S
% LocalWords: textsf NatArith mathbf cdot IntArith rightarrow forall mathbb overline cn
% LocalWords: assoc oldpart CarFarKoh rsckmt14 realm-gr textbackslash mathit tikzpicture
% LocalWords: hline arr arr inv wrapfigure vspace lstlisting mathescape ldots vdots lst
% LocalWords: equivcyc realmspec groupspec compactenum sym defemph
% LocalWords: equivcyc realmspec groupspec compactenum sym defemph centering Monoid
% LocalWords: itemize
@MISC {flatsearch-demo,
title = {FlatSearch Demo},
howpublished = {\url{http://cds.omdoc.org:8181/search.html}}
}
In the case of the induced knowledge for realms described in section \ref{sec:realms} a natural application area is library integration.
Conceptually, integrating libraries means that we can make use of results in any of them to prove new theorems.
However, in practice, different libraries define core concepts (e.g. real numbers, functions, etc.) differently so, even after importing
them to a common foundation, libraries remain effectively segregated.
A natural application area for induced realms as described in Section \ref{sec:realms} the
integration of formal libraries, so that results in any of them can be used to prove new
theorems in any other. This is the aim of the \emph{Open Archive of Formalizations}
\cite{OAF:on} which integrates several, large, formal mathematical libraries. It use the
LATIN logic atlas \cite{CodHorKoh:palai11} as a logical basis and imports the
libraries as based on a dedicated LATIN meta-logic. Views between the base logics relate
the libraries themselves at the foundational level but at a higher level, the important
mathematical concepts remain unassociated.
This is the case of the OAF project \cite{OAF} which tries to integrate several, large, formal mathematical libraries.
It use the LATIN logic atlas as a logical basis and imports the libraries as based on a dedicated LATIN logic.
Views between the base logics relate the libraries themselves at the foundational level but at a higher level, the important mathematical concepts
remain unassociated.
Even though the underlying domains should form realms straddling the libraries, in
practice, different libraries define core concepts (e.g. real numbers, functions, etc.)
differently so, even after importing them to a common foundation, libraries remain
effectively segregated. To achieve genuine interoperability we need to associate the
equivalent concepts from each library with each other and establish a new library
containing the \emph{merged} concepts. This is a direct application of the ideas from
Section \ref{sec:realms}. First, we can associate concepts by declaring realms. Then, we
can generate the induced faces graph that provides the interface to the \emph{merged},
integrated library. The operation of opening a pillar described in Section
\ref{sec:op-pillar} allows access to the implementation details of each individual library
where needed. Finally, the resulting interface can be refined via alignments.
The different induced realm graphs in Figure~\ref{fig:realms-roles} can be seen as special
lenses that allow users with different roles to see the underlying archive according to
their preferences and needs. This is similar to how an experienced human would present the
materials if she were aware of the user role; therefore we can see the induced realms as a
form of mathematical literacy.
Therefore, to achieve genuine interoperability we need to associate the equivalent concepts from each library with each other and establish a new library
containing the \emph{merged} concepts.
This is a direct application of the ideas from section \ref{sec:realms}. First, we can associate concepts by declaring realms.
Then, we can generate the induced faces graph that provides the interface to the \emph{merged}, integrated library. The operation of
opening a pillar described in section \ref{sec:op-pillar} allows access to the implementation details of each individual library where needed.
Finally, the resulting interface can be refined via alignments.
Applying the above to the OAF project is still future work at the moment but the challenges encountered during the project provided the main motivation
for the work described in this paper.
Applying the above to the OAF is still future work but the challenges encountered during
the project provided the main motivation for the work described in this paper.
%
% An application for the realms flattening occurs in heterogeneous mathematical libraries that become unwieldy
......@@ -36,3 +45,10 @@ for the work described in this paper.
% access point, or interface, to the OAF library. Adding realms or alignments, as well as other archive imports will extend or improve this interface.
%
%
%%% Local Variables:
%%% mode: LaTeX
%%% TeX-master: "paper"
%%% End:
% LocalWords: emph Formalizations CodHorKoh Mizar cn Mizar
No preview for this file type
......@@ -12,8 +12,7 @@
\lstset{basicstyle=\sf,columns=fullflexible,aboveskip=0pt,belowskip=0pt}
%\usepackage{hyperref}
%\hypersetup{linkcolor=red,citecolor=blue,urlcolor=gray,colorlinks,breaklinks,bookmarksopen,bookmarksnumbered}
%\hypersetup{linkcolor=red,citecolor=blue,urlcolor=gray,colorlinks,breaklinks,bookmarksop%en,bookmarksnumbered}
\usepackage[linkcolor=black]{hyperref}
......@@ -25,7 +24,7 @@
\addbibresource{extpubs.bib}
\addbibresource{kwarccrossrefs.bib}
\addbibresource{extcrossrefs.bib}
\addbibresource{local.bib}
%\addbibresource{local.bib}
\usepackage{local}
\usepackage{bibtweaks}
......@@ -78,10 +77,11 @@
\section{Inducing Realm Faces/Flattening Realms}\label{sec:realms}
\input{realms}
\section{Searching the Knowledge Space of the LATIN library}\label{sec:searching}
\section{Searching the Knowledge Space of the LATIN Logic Atlas}\label{sec:searching}
\input{search}
\section{Realm Workflows}\label{sec:oaf}
\section{Future Work: Realm-Supported Workflows in the Open Archive of
Formalizations}\label{sec:oaf}
\input{oaf}
\section{Conclusion and Future Work}\label{sec:concl}
......@@ -98,4 +98,4 @@
%%% End:
% LocalWords: maketitle flatsearch mws prel concl conc printbibliography setcounter
% LocalWords: tocdepth tableofcontents newpage
% LocalWords: tocdepth tableofcontents newpage Formalizations
......@@ -25,7 +25,7 @@ all {\mmt} notions are fully abstract in the choice of the base language.
%\ednote{rephrase}
We will only give a brief introduction to {\mmt} here and then discuss the concepts using
examples in section \ref{sec:libraries}. We refer to \cite{RK:mmt:10} for further details.
examples in Section \ref{sec:libraries}. We refer to \cite{RK:mmt:10} for further details.
The central notion is that of a \textbf{theory graph} containing \emph{theories} and
\emph{views} (morphisms between theories). Note that {\mmt} libraries actually contain
......@@ -81,16 +81,16 @@ $v$?\llquote{symbol-name}.
The \mmt system provides an API to the {\mmt} data structures described above and the \mmt
implementation \cite{project:mmt,RK:mmt:10} provides a Scala-based \cite{scala} open
source implementation of the {\mmt} API. The \mmt system can also generate MWS harvests
from {\mmt} libraries so, from the perspective of {\mws}, it can be seen as a MWS
implementation \cite{project:mmt,RK:mmt:10} provides a Scala-based open source
implementation of the {\mmt} API. The \mmt system can also generate MWS harvests from
{\mmt} libraries so, from the perspective of {\mws}, it can be seen as a MWS
crawler. Therefore, with respect to {\mmt} our {\flatsearch} approach involves generating
the flattened version on a library and then exporting it as MWS harvests.
\subsection{{\latin}}\label{sec:latin}
The \latin project (\textbf{L}ogic \textbf{At}las and \textbf{In}tegrator)
\cite{project:latin,LATIN:url} aims at developing tools for interfacing logics and proof
\cite{CodHorKoh:palai11} aims at developing tools for interfacing logics and proof
systems. It focuses on developing a knowledge representation framework that is
foundationally unconstrained and thus allows for the representation of most meta-theoretic
foundations of mathematical knowledge in the same format.
......@@ -118,7 +118,7 @@ converted to MWS harvests.
%%% TeX-master: "paper"
%%% End:
% LocalWords: miancu mws mws KohPro MWSmanual emph mmt ednote textbf mapsto
% LocalWords: miancu mws mws KohPro MWSmanual emph mmt ednote textbf mapsto oldpart
% LocalWords: rightarrow llquote ldots odel-Gentzen identhy idenview ogic tptp
% LocalWords: tegrator CaslTCS03 pem06 Nipkow-Paulson-Wenzel htisdfp02
% LocalWords: Pfenning91 isabelle-isar
......@@ -215,9 +215,12 @@ realm from~\cite{CarFarKoh:rsckmt14} to the \mmt setting for intuitions.
%\begin{example}\label{ex:realm-gp} problems with
\noindent\stepcounter{example}\label{ex:realm-gp}\textit {Example \arabic{example}.}
Figure~\ref{fig:realm-gr} shows a realm with two pillars for the equivalent
group definitions based on composition $\circ$ and, respectively, division $\cn{/}$ in the
usual way. The corresponding realm specification is in Figure~\ref{fig:realm-gr}.
Figure~\ref{fig:realm-gr} shows a realm with two pillars for the equivalent group
definitions based on composition $\circ$ and, respectively, division $\cn{/}$ in the usual
way. The corresponding realm specification is in Figure~\ref{lst:groupspec}. We have added
the unit \cn{e} with its axiom $\cn{e_{ax_1}}, \cn{e_{ax_2}}$ to \cn{group_/} even though
it is mathematically redundant -- $\cn{e}=x/x$ for all $x$ in \cn{G} because that allows
us to show all aspects of the face generation algorithm below.
\begin{wrapfigure}r{4.5cm}\vspace*{-2em}
\begin{lstlisting}[mathescape]
......@@ -238,21 +241,21 @@ important concepts as primitive symbols and all their properties as axioms. We e
face was produced below.
\begin{definition}\label{def:realm-order}\rm
We define the following partial ordering on symbols in a realm \cn{r}. Let \cn{t} and \cn{s} be
symbols in theories \cn{T} and \cn{S} respectively such \cn{T} and \cn{S} are in different
pillars. If there is an assignment \cn{s := t} in one of the pillar equivalence views then
we write \cn{s \geq_r t}. If there is also an assignment \cn{t := s} in such a view then we
write. \cn{s =_r t}, otherwise \cn{s >_r t}. We call a symbol that is \cn{>_r}-maximal
\defemph{essential} in \cn{r}.
We define the following partial ordering on symbols in a realm \cn{r}. Let \cn{t} and
\cn{s} be symbols in theories \cn{T} and \cn{S} respectively such \cn{T} and \cn{S} are
in different pillars. If there is an assignment \cn{s := t} in one of the pillar
equivalence views then we write \cn{s \leq_r t}. If there is also an assignment \cn{t :=
s} in such a view then we write. \cn{s =_r t}, otherwise \cn{s <_r t}. We call a
symbol \defemph{essential} in \cn{r} if it is \cn{<_r}-minimal.
%Moreover, we write $s \parallel t$ if there is no order between $s$ and $t$ (i.e. no assignment).
\end{definition}
The intuition behind Definition \ref{def:realm-order} is that if there is an assignment
\cn{s := t} then there is an equivalence between \cn{s} and \cn{t} at the realm level and we need
to decide which should appear in the face. Then, the ordering captures the fact that \cn{s}
is a primitive concept in its realm while \cn{t} is derived, possibly only to give the
equivalence view. This is, for instance, the case of the symbols $\cn{inv}$ and $\circ$
from theory \cn{circ_/} in Figure \ref{fig:realm-gr}.
\cn{s := t} then there is an equivalence between \cn{s} and \cn{t} at the realm level and
we need to decide which should appear in the face. Then, the ordering captures the fact
that \cn{s} is a primitive concept in its realm while \cn{t} is derived, possibly only to
give the equivalence view. In Figure \ref{fig:realm-gr} the symbols $\cn{inv}$ and
$\circ$ from theory \cn{circ_/} are derived.
\begin{definition}\rm\label{def:facegen}
Let \cn{r} be a realm as specified in Figure~\ref{lst:realmspec}. Then, we generate a face
......@@ -317,11 +320,13 @@ theory group = {G : type, e : G, $\ldots$, / : G$\arr$G$\arr$G $\ldots$, inv_thm
\subsection{Opening a Pillar}\label{sec:op-pillar}
For the student/developer view described above we need the operation of \emph{opening a pillar} that
allows the developer to access the internals of the symbols and axioms in the face as
formalized in one of the pillars. We model this by creating a new theory for each pillar that combines
the symbol aggregation and name abstraction of the face theory with the implementation details of that pillar.
\begin{wrapfigure}r{4.3cm}\vspace*{-2em}
For the student/developer view described above we need the operation of \emph{opening a
pillar} that allows the developer to access the internals of the symbols and axioms in
the face as formalized in one of the pillars. We model this by creating a new theory for
each pillar that combines the symbol aggregation and name abstraction of the face theory
with the implementation details of that pillar.
\begin{wrapfigure}l{4.7cm}\vspace*{-2em}
\begin{tikzpicture}
\node[thy] (group1) at (-1.5,0) {\textsf{$\mathsf{group}_\circ$}};
\node[thy] (group2) at (1.5,0) {\textsf{$\cn{group}_/$}};
......@@ -357,10 +362,9 @@ the symbol aggregation and name abstraction of the face theory with the implemen
\draw[view, dotted] (face) to node[above, near start] {$\cn{f_/}$} (p2);
\draw[struct, dotted] (thy1) to node[right] {$\cn{s_\circ}$} (p1);
\draw[struct, dotted] (thy2) to node[left] {$\cn{s_/}$} (p2);
\end{tikzpicture}
\caption{Opening a Pillar}\label{fig:realm-op}
\end{tikzpicture}\vspace*{-.5em}
\caption{Opening a Pillar}\label{fig:realm-op}\vspace*{-1em}
\end{wrapfigure}
Concretely, given a realm \cn{r} and a pillar \cn{p} we induce a theory \cn{r/p} that is generated following the
same procedure as the face (i.e. from Definition \ref{def:facegen}) but without omitting the definitions.
For symbols in a different pillar we generate the definition by translating it over the view from
......@@ -375,12 +379,8 @@ with the renamings used in the face generation and,
for the face.
\end{inparaenum}
Listing \ref{lst:devview} shows the theory \cn{group/circ} representing the opening of pillar \cn{circ} in the realm of groups
above. It has the same symbols as the face but with all symbols that are non-primitive in \cn{circ} having a definition.
For the two symbols originating in the second pillar (\cn{/} and \cn{slash/inv\_thm}) their definition is obtained by translating
over \cn{v_\circ}.
\begin{lstlisting}[mathescape,label=lst:devview,caption=Developer View Example]
\begin{wrapfigure}r{7.3cm}\vspace*{-2em}
\begin{lstlisting}[mathescape]
theory group/circ = {
G : type, $\circ$ : G $\arr$ G $\arr$ G, e : G, inv : G $\arr$ G,
/ : G $\arr$ G $\arr$ G = $\lambda$a,b.a $\circ$ (inv b),
......@@ -389,12 +389,18 @@ theory group/circ = {
$\vdots$
}
\end{lstlisting}
The resulting theory graph is shown in \ref{fig:realm-op} where the content of each theory is omitted. Note that the theories
\cn{group}, \cn{group/circ}, \cn{group/slash} as well as the structures $\cn{s_\circ}$ and $\cn{s_/}$ and the views $\cn{i_\circ}, \cn{i_/}, \cn{f_\circ}$ and $\cn{f_/}$ are
all induced.
\caption{Developer View Example}\label{lst:devview}
\end{wrapfigure}
Listing \ref{lst:devview} shows the theory \cn{group/circ} representing the opening of pillar \cn{circ} in the realm of groups
above. It has the same symbols as the face but with all symbols that are non-primitive in \cn{circ} having a definition.
For the two symbols originating in the second pillar (\cn{/} and \cn{slash/inv\_thm}) their definition is obtained by translating
over \cn{v_\circ}.
The resulting theory graph is shown in Figure \ref{fig:realm-op} where the content of each
theory is omitted. Note that the theories \cn{group}, \cn{group/circ}, \cn{group/slash} as
well as the structures $\cn{s_\circ}$ and $\cn{s_/}$ and the views
$\cn{i_\circ}, \cn{i_/}, \cn{f_\circ}$ and $\cn{f_/}$ are all induced.
% We use the URI $G?r/p$ to refer to the opening of pillar $p$ in realm $r$. See Figure
% \ref{fig:realm-op} and \ref{lst:devview} for an example of the construction of the theories described
......@@ -417,4 +423,5 @@ all induced.
% LocalWords: textbf mmt realm-gr circ textbackslash mathit emph textsf mathsf hline
% LocalWords: arr arr inv assoc lstlisting ldots vdots equivcyc lst realmspec groupspec
% LocalWords: compactenum sym cdot newcommand mygray inparaenum thm vdash doteq facegen
% LocalWords: mathescape realm-gp noindent stepcounter textit geq KohRabSac fvip11
% LocalWords: mathescape realm-gp noindent stepcounter textit geq KohRabSac fvip11 leq
% LocalWords: centering graying mechanized formalizations formalized renamings devview
As a first application of the concepts described in this paper we build a system
for searching the knowledge space (i.e. flattened theory graph) of the highly modular
LATIN \cite{project:latin,LATIN:url} library.
As a first application of the concepts described in this paper we build a system for
searching the knowledge space (i.e. flattened theory graph) of the highly modular LATIN
\cite{CodHorKoh:palai11} library.
\paragraph{MathWebSearch} For searching, we use our {\mws} system~\cite{ProKoh:mwssofse12},
which is a content-oriented search engine for mathematical expressions.
that indexes formula-URL pairs and provides a web interface querying the formula index
via unification.
% The MWS system consists of three components:
% \begin{itemize}
% \item A \emph{crawler subsystem} collects data from a mathematical knowledge repository
% and converts the mathematical expressions into \emph{{\mws} harvests}. The harvests are
% files containing mathematical expressions encoded in a MWS-specific XML-based format
% (see \cite{KohPro:MWSmanual} for details).
% \item The \emph{core system} builds the search index from MWS harvests and processes
% search queries.
% \item The \emph{RESTful interface} provides a public HTTP API for interacting with the
% core system (i.e. submitting queries and receiving results).
% \end{itemize}
%
% Therefore, with respect to {\mws}, our {\flatsearch} approach involves providing a MWS crawler that generates
% MWS harvests from flattened {\mmt} libraries and a MWS frontend for submitting queries that will interact with
% the MWS RESTful interface.
This can be used for:
\paragraph{MathWebSearch} For searching, we use our {\mws}
system~\cite{ProKoh:mwssofse12}, which is a content-oriented search engine for
mathematical expressions. that indexes formula-URL pairs and provides a web interface
querying the formula index via unification. The implementation of a math-literate web
service that conducts such searches is very simple: instead of harvesting formulae from a
formal digital library directly as in~\cite{IKRU:mizar:11}, we flatten the library first,
and then harvest formulae. Conveniently, {\mmt} flattening gives the included constants
and axioms local names that are syntactically identical to the respective symbol paths in
{\mmt} URIs, so that the generation of {\mmt} URIs for the formula harvests is
trivial. Moreover, we can leverage the \mmt URIs to determine the origin of the induced
formulae. But first we need to replace the human-oriented search front-end of MWS,
i.e. the input of search queries and the presentation of search results. This can be used
for:
\begin{compactdesc}
\item[Instance Search] e.g. to find all instance of associativity we can issue the query
$\forall x,y,z : \qvar{S}.(x\qvar{op} y) \qvar{op} z = x \qvar{op} (y\qvar{op} z)$,
where the $\qvar{-}$ are query variables that can be instantiated in the query. In the
library from Figure~\ref{fig:elal-graph} we would find the commutativity axiom
library from Figure~\ref{fig:elal-graph} we would find the associativity axiom
\textsf{SemiGrp}/\textsf{assoc}, its directly inherited versions in \textsf{Monoid}, to
\textsf{Ring} and in particular the version
$u$?\textsf{IntArith}?\textsf{c}/\textsf{g}/\textsf{assoc}.
......@@ -40,35 +31,27 @@ This can be used for:
together with the justification $u$?\textsf{IntArith}?\textsf{c}/\textsf{comm} that can
directly be used in a proof.
\end{compactdesc}
The implementation of a web service that conducts such searches is very simple: instead of
harvesting formulae from a formal digital library directly as
in~\cite{IKRU:mizar:11}, we flatten the library first, and then harvest
formulae. Conveniently, {\mmt} flattening gives the included constants and axioms local names
that are syntactically identical to the respective symbol paths in {\mmt} URIs, so that the
generation of {\mmt} URIs for the formula harvests is trivial. Moreover, we can leverage the
\mmt URIs to determine the origin of the induced formulae.
% For building a math literate search application we follow the outline described in section \ref{sec:ind}.
% For building a math literate search application we follow the outline described in Section \ref{sec:ind}.
% Namely, we forst generate the induced theory graph and then, in the
% application, leverage the \mmt URIs to explain the origin the induced formulae.
But first we need to replace the human-oriented search front-end of MWS,
i.e. the input of search queries and the presentation of search results. The {\latin}
atlas is written in an extension of the TWELF encoding~\cite{RS:twelfmod:09} of
LF~\cite{HarperEtAl:affdl93}, so it is natural to use an extension of LF notation with
\paragraph{Induced statements in the {\latin} library}
The {\latin} atlas is written in an extension of the TWELF encoding~\cite{RS:twelfmod:09}
of LF~\cite{HarperEtAl:affdl93}, so it is natural to use an extension of LF notation with
query variables for input. Therefore, we use the {\mmt} notation language and
interpretation service described in \cite{IR:ui:12} to transform LF-style input into
{\mmt} objects and subsequently to MWS queries.
\paragraph{Induced statements in the {\latin} library}
We implemented library flattening as described in section \ref{sec:flat} in {\mmt} and applied it
to the {\latin} library. The flattening (once) of the {\latin} library increases the number of
declarations from 2310 to 58847 (a factor of 25.4) and the total size of the library from
123.9 MB to 1.8 GB (a factor of 14.8). As expected, the multiplication factor depends on
the level of modularity of the library. For instance, the highly modular math sub-library
containing mainly algebraic structures increases from 2.3 MB to 79 MB thus having a
multiplication factor of 34.3, more than double the library average. The size of the MWS
harvests also increases considerably, from 25.2 MB to 539.0 MB.
We implemented library flattening as described in Section \ref{sec:flat} in {\mmt} and
applied it to the {\latin} library. The flattening (once) of the {\latin} library
increases the number of declarations from 2310 to 58847 (a factor of 25.4) and the total
size of the library from 123.9 MB to 1.8 GB (a factor of 14.8). As expected, the
multiplication factor depends on the level of modularity of the library. For instance, the
highly modular math sub-library containing mainly algebraic structures increases from 2.3
MB to 79 MB thus having a multiplication factor of 34.3, more than double the library
average. The size of the MWS harvests also increases considerably, from 25.2 MB to 539.0
MB.
\paragraph{Explaining URIs of induced statements}
The presentation of the {\mmt} URIs requires some work as well: while the {\mmt} system
......@@ -84,15 +67,14 @@ localize the result in the theory \cn{u}?\textsf{IntArith} with the sentence
\underline{\texttt{http://cds.omdoc.org/cds/elal?IntArith}} (\underline{subst},
\underline{justification}).
\end{labeledquote}
Here the underlined fragments carries hyperlinks, the second pointing to the
justification:
Here the underlined fragments carry hyperlinks, the second pointing to the justification:
\begin{labeledquote}\sf\label{lq:view}
\underline{\textsf{IntArith}} is a \underline{\textsf{CGroup}} if we interpret $\circ$
as + and $G$ as $\mathbb{Z}$.
\end{labeledquote}
which can be directly inferred from the information associated to the morphism $\mathsf{c}$ in the
{\mmt} URI. Then we skip over $\mathsf{g}$, since its assignment is trivial and generate the
sentence.
which can be directly inferred from the information associated to the morphism
$\mathsf{c}$ in the {\mmt} URI. Then we skip over $\mathsf{g}$, since its assignment is
trivial and generate the sentence.
\begin{labeledquote}\sf\label{lq:inclusions}
\underline{\textsf{CGroup}}s are \underline{\textsf{SemiGrp}}s \underline{by
construction}
......@@ -103,10 +85,14 @@ and finally we ground the explanation by the sentence
x,y,z : G . (x\circ y)\circ z=x\circ (y\circ z)$}
\end{labeledquote}
The sentences (\ref{lq:theory}) to (\ref{lq:ground}) can be generated from templates,
since the {\mmt} system gives access to the necessary information: source and target theory
as well as the assignment $\psi'$ for (\ref{lq:view}), the fact that the path from
\textsf{SemiGrp} to \textsf{CGroup} only consists of inclusion that triggers the template
for (\ref{lq:inclusions}) and the original formulation of the axiom $\mathsf{assoc}$.
since the {\mmt} system gives access to the necessary information: source and target
theory as well as the assignment $\psi'$ for (\ref{lq:view}), the fact that the path from
\textsf{SemiGrp} to \textsf{CGroup}\footnote{In fact these theory identifiers are not
adequate for explanations. We conjecture that verbalization of the primary symbol of the
respective theory would be the right choice here -- see~\cite{Kohlhase:dmesmgm14} for
these concepts -- but leave studying this to future work.} only consists of inclusion
that triggers the template for (\ref{lq:inclusions}) and the original formulation of the
axiom $\mathsf{assoc}$.
\begin{figure}
\begin{center}
......@@ -115,11 +101,11 @@ for (\ref{lq:inclusions}) and the original formulation of the axiom $\mathsf{ass
\caption{The {\flatsearch} Web Interface for {\latin}}\label{fig:flatsearch}
\end{figure}
The resulting search interface is shown in Figure \ref{fig:flatsearch} and is available at \cite{flatsearch-demo}.
Note that we make use of another peculiarity of the {\mmt} system in this explanation: all
constants in the theory graph carry notation declarations~\cite{KMR:NoLMD08}, which can be
used to generate human-readable presentations of arbitrary formal objects in the
graph.
The resulting search interface is shown in Figure \ref{fig:flatsearch} and is available at
\cite{flatsearch-demo:on}. Note that we make use of another peculiarity of the {\mmt} system
in this explanation: all constants in the theory graph carry notation
declarations~\cite{KMR:NoLMD08}, which can be used to generate human-readable
presentations of arbitrary formal objects in the graph.
%%% Local Variables:
%%% mode: LaTeX
......@@ -127,6 +113,7 @@ graph.
%%% End:
% LocalWords: miancu mws ProKoh mwsofse compactdesc forall qvar qvar qvar qvar newpart
% LocalWords: qvar elal-graph textsf SemiGrp textsf assoc textsf IntArith comm CGroup
% LocalWords: qvar elal-graph textsf SemiGrp textsf assoc textsf IntArith comm CGroup cn
% LocalWords: mapsto mmt affdl93 ednote labeledquote lq mathbb texttt subst mwssofse12
% LocalWords: circ mathsf includegraphics textwidth flatsearch
% LocalWords: circ mathsf includegraphics textwidth flatsearch CodHorKoh Monoid
% LocalWords: verbalization dmesmgm14
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment