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

Merge branch 'master' of gl.kwarc.info:immt/papers

parents 463d306e 24eb1609
No related branches found
No related tags found
No related merge requests found
Intuitively, the knowledge space of a mathematical library is formed of all the statements
that can be proved in it so it is not possible to (easily) mechanically generate the
entire knowledge space. However, in the context of theory graphs a substantial amount of
interesting knowledge can be generated by leveraging relations between theories (such as
imports or theory morphisms). Specifically, in \mmt we define \emph{induced} statements
in a theory graph as statements that are valid without being explicitly represented. We
look at two examples of induced statements.
\begin{definition}
Given a theory graph $G$ \emph{flattening} is theory graph operation $\flat$ that takes
a theory graph $G$ and returns a theory graph $\overline{G}$. An application for $\flat$
is one that uses $\overline{G}$ as a knowledge base instead of $G$.
\end{definition}
A key aspect of \mmt is that it's URI language is expressive enough such that we can
produce URI for the induced statements that are not only unique but also explicitly
explain the existence of the induced statement so that we can relate to the original
theory graph. That allows applications to tie the induced theory graph to the original one
and, for instance, produce explanations of how each induced statement is produced.
\begin{itemize}
\item accessing induced statements
\end{itemize}
......@@ -114,6 +114,7 @@ the graph. This problem can be solved by technology: incremental, in-place flatt
the {\mmt} front-end. At the same time, it becomes more and more difficult to avoid
duplication and maintain a maximally shared structure, for this we need a search system
that takes induced statements (these are the ones we want to share) into account.
\end{oldpart}
%%% Local Variables:
%%% mode: latex
......
Intuitively, the knowledge space of a mathematical library is formed of all the statements
that can be proved in it so it is not possible to (easily) mechanically generate the
entire knowledge space. However, in the context of theory graphs a substantial amount of
interesting knowledge can be generated by leveraging relations between theories (such as
imports or theory morphisms). Specifically, in \mmt we define \emph{induced} statements
in a theory graph as statements that are valid without being explicitly represented. We
look at two examples of induced statements.
\begin{definition}
Given a theory graph $G$ \emph{flattening} is theory graph operation $\flat$ that takes
a theory graph $G$ and returns a theory graph $\overline{G}$. An application for $\flat$
is one that uses $\overline{G}$ as a knowledge base instead of $G$.
\end{definition}
A key aspect of \mmt is that it's URI language is expressive enough such that we can
produce URI for the induced statements that are not only unique but also explicitly
explain the existence of the induced statement so that we can relate to the original
theory graph. That allows applications to tie the induced theory graph to the original one
and, for instance, produce explanations of how each induced statement is produced.
\subsection{Flattening Theory Graphs}\ednote{MK: I think that this should become a section
of its own}
To better understand the situation in modular libraries, consider the theory graph in
Figure~\ref{fig:elal-graph}. The right side of the graph introduces the elementary
algebraic hierarchy building up algebraic structures step by step up to rings; the left
......
No preview for this file type
......@@ -75,13 +75,16 @@
\section{Preliminaries}\label{sec:prel}
\input{prel}
\section{Induced Statements in Theory Graphs}\label{sec:libraries}
\section{Induced Statements in Theory Graphs}\label{sec:ind}
\input{induced}
\section{Flattening Theory Graphs}\label{sec:flat}
\input{libs}
\section{Inducing Realm Faces/Flattening Realms}
\section{Inducing Realm Faces/Flattening Realms}\label{sec:realms}
\input{realms}
\section{Accessing Induced Statements}\label{sec:searching}
\section{Searching the knowledge space of the LATIN library}\label{sec:searching}
\input{search}
\section{Conclusion and Future Work}\label{sec:concl}
......
......@@ -139,14 +139,14 @@ primitive symbols and all their properties as axioms.
$e_{\mathit{ax}_1}, e_{\mathit{ax}_2}, /_{ax_1}, /_{ax_2}$
\end{tabular}};
\node[thy] (slash1) at (-3,4) {\begin{tabular}{l}
\node[thy] (slash1) at (-3,2.7) {\begin{tabular}{l}
\textsf{$\cn{slash}_\circ$}\\\hline
$/ : G \arr G $ \\
$\;\;= \lambda a,b . a \circ inv(b)$ \\ \hline
\end{tabular}};
\node[thy] (circ2) at (3,4) {\begin{tabular}{l}
\node[thy] (circ2) at (3,2.7) {\begin{tabular}{l}
\textsf{$\cn{circ}_/$}\\\hline
$\circ : G \arr G \arr G $ \\
$\;\;= \lambda a,b . a / (e / b)$ \\
......@@ -155,13 +155,13 @@ primitive symbols and all their properties as axioms.
\end{tabular}};
%%%% inv
\node[thy] (thy1) at (-3,7) {\begin{tabular}{l}
\node[thy] (thy1) at (-3,5) {\begin{tabular}{l}
\textsf{$\cn{inv\_thm}_\circ$}\\\hline
$inv\_thm_\circ:\; \vdash inv(e) \doteq e $ \\
$\;\;= trans \; e_{right} \; inv_{ax} $ \\ \hline
\end{tabular}};
\node[thy] (thy2) at (3,7) {\begin{tabular}{l}
\node[thy] (thy2) at (3,5) {\begin{tabular}{l}
\textsf{$\cn{inv\_thm}_/$}\\\hline
$inv\_thm_/:\; \vdash inv(e) \doteq e $ \\
$\;\;= e_{ax_2} e $ \\ \hline
......@@ -169,7 +169,7 @@ primitive symbols and all their properties as axioms.
%%%%
\node[thy,dotted] (face) at (0,10) {\begin{tabular}{l}
\node[thy,dotted] (face) at (0,8) {\begin{tabular}{l}
\textsf{$\cn{group}$}\\\hline
$G : \mathit{type}$ \\
$\circ : G \arr G \arr G $ \\
......@@ -310,6 +310,51 @@ the theorem.
\ednote{MK: find a good example for an alignment, say where this idea is from.}
\paragraph{Opening A pillar}
\begin{figure}[ht]\centering
\begin{tikzpicture}
\node[thy] (group1) at (-1.5,0) {\textsf{$\mathsf{group}_\circ$}};
\node[thy] (group2) at (1.5,0) {\textsf{$\cn{group}_/$}};
\node[thy] (slash1) at (-1.5,1) {\textsf{$\cn{slash}_\circ$}};
\node[thy] (circ2) at (1.5,1) {\textsf{$\cn{circ}_/$}};
%%%% inv
\node[thy] (thy1) at (-1.5,2) {\textsf{$\cn{inv\_thm}_\circ$}};
\node[thy] (thy2) at (1.5,2) {\textsf{$\cn{inv\_thm}_/$}};
%%%%
\node[thy] (p1) at (-2.5,4) {\textsf{\cn{group/p}}};
\node[thy] (p2) at (2.5,4) {\textsf{\cn{group/q}}};
%%%%
\node[thy,dotted] (face) at (0,3) {\textsf{$\cn{group}$}};
\draw[conservative] (group1) to (slash1);
\draw[conservative] (group2) to (circ2);
\draw[conservative] (slash1) to (thy1);
\draw[conservative] (circ2) to (thy2);
\draw[view] (group1) to node[near end, above] {$v_1$} (circ2);
\draw[view] (group2) to node[near end, above] {$v_2$} (slash1);
\draw[view, dotted] (face) to node[above] {$i_1$} (thy1);
\draw[view, dotted] (face) to node[above] {$i_2$} (thy2);
%%%
\draw[view, dotted] (face) to node[above] {$f_1$} (p1);
\draw[view, dotted] (face) to node[above] {$f_2$} (p2);
\draw[view, dotted] (thy1) to node[right] {$p_1$} (p1);
\draw[view, dotted] (thy2) to node[left] {$p_2$} (p2);
\end{tikzpicture}
\caption{A Realm of Groups}\label{fig:realm-gr}
\end{figure}
\paragraph{Accessing induced statements}
$F/s$ means there is an unique theory in a pillar of $F$ that contains symbol $s$.
$F/p/s$ means there is a pillar $p$ for realm $F$ that contains symbol $s$.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment