@@ -8,7 +8,7 @@ First, each paper starts with establishing a common ground on which the results
\item Firstly, concepts from the literature are used to conveniently build up the local definitions. From the theory graphs perspective
this functions as a (possibly partial) import.
\item Secondly, properties of locally introduced concepts are \emph{adopted} from the literature. Mathematically, this is justified by
and (implicit or explicit) equivalence \ednote{``equivalence'' is too strong here} between the local definition and that used by the referenced theorem.
and (implicit or explicit) subsumption between the local definition and that used by the referenced theorem.
From the theory graph perspective this function as a theory morphism that induces the properties locally due to its truth-preserving semantics.
\end{itemize}
Therefore, a paper corresponds, not to a single theory, but to a theory pattern that leads to a theory of the main contxribution of the paper.
...
...
@@ -391,130 +391,7 @@ given in the literature (which we represent as a realm).
\end{figure}
\begin{oldpart}{from bluenote}
We will progress by going through the examples from the introduction. \ednote{MK@MK: say
something about what digital libraries should look like: a theory for every variant
highly modularized, narratively enhanced overview for salient theories that are often
used, see Carette/Farmer high-level theories, \cite{CarFarKoh:tr13}}
\begin{example}[A Course grounded in a Formal Library]\label{sec:course}
Take for instance a course which introduces (naive) set theory informally, but grounds
itself in a formal, modular definition. Then we have the situation in
Figure~\ref{fig:slides-library}. On the right hand side, we have a careful introduction in
the form of a modular theory graph starting at a theory \cn{ZFset} that introduces
membership relation and the axioms of existence, extensionality, and separation and
defines the set constructor $\{\cdot |\cdot\}$ from these axioms. On the left we have a
theory \cn{SET} that ``adopts'' the symbols $\in$ and $\{\cdot |\cdot\}$ via a partial
inclusion $\cn{a_1}$ from \cn{ZFset} to \cn{SET} but ``defines'' them by alluding the
intuitions of the students. Note that a partial inclusion always gives rise to a view in
the opposite direction, here the view \cn{v_1} from \cn{SET} to \cn{set}. Note that we
cannot discharge the proof obligations in \cn{v_1}, since the definition of the set
constructor $\{\cdot |\cdot\}$ is opaque -- i.e. given as natural language, which is not
subject to formal methods; see~\cite{Kohlhase:fsgo13} for a discussion. We should think
of \cn{v_1} as a ``definitional view'' that gives meaning to the opaque parts in \cn{SET}:
the proof obgligations have to be met in order for the diagram to commute (which is an
invariant we want to maintain).
We call this situation where the symbols of a theory are imported via a partial inclusion
and their meaning is specified via a view that is a partial inverse an \textbf{adoption}
and the morphism pair an \textbf{adoption} morphism.
\begin{figure}[ht]\centering
\begin{tikzpicture}[yscale=1.7]
\node at (1,2.6) {\large Library};
\node at (-4.5,2.6) {\large Course};
\node[thy] (zfset) at (1,-.2) {\mthy{ZFset}{$\in$, \cn{Ex}, \cn{Ext}, \cn{Sep}; $\{\cdot |\cdot\}$}};
\node[thy] (zfunion) at (-.2,1) {\mthy{ZFunion}{\cn{Un}, $\cup$}};
\node[thy] (zfpow) at (2.2,1) {\mthy{ZFpow}{\cn{Pow}, $\mathcal{P}$}};
\node at (1.1,1) {\ldots};
\node[thy] (zfop) at (1,2) {ZFops};
\draw[include] (zfset) -- (zfunion);
\draw[include] (zfset) -- (zfpow);
\draw[include] (zfunion) -- (zfop);
\draw[include] (zfpow) -- (zfop);
\node[thy] (set) at (-4.5,-.2) {\mthy{SET}{$\in$, $\{\cdot |\cdot\}$}};
\node[thy] (sop) at (-4.5,2) {\mthy{SETOPS}{$\cup$,\ldots,$\mathcal{P}$}};
