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

fixing errors

parent 5143b8f5
No related branches found
No related tags found
No related merge requests found
......@@ -119,10 +119,10 @@ position. The case for (\ref{ex:fitif}) is similar.
<m:csymbol cd="set">setst</m:csymbol>
<m:csymbol cd="nats">naturalnumbers</m:csymbol>
</m:apply>
<m:bvar><m:mi>x</m:mi></m:bvar>
<m:bvar><m:ci>x</m:ci></m:bvar>
<m:apply>
<m:mo>is prime</m:mo>
<m:mi>x</m:mi>
<m:symbol>is prime</m:csymbol>
<m:ci>x</m:ci>
</m:apply>
</m:bind>
\end{lstlisting}
......@@ -256,12 +256,12 @@ see~\cite{SS:ProcTextMatrices05} for some extreme examples of elision in matrixe
Declarations get phrase-level markup in \omdoc via a dedicated role system, which allows
to designate a phrase (verbal or formula) as a declaration (via
\lstinline|o:role="declaration"|\footnote{Note that XHTML and \mathml (and most other XML
vocabularies) allow foreign-namespace attributes and ignore them.}). %|
Additional attributes \lstinline|o:decname|, \lstinline|o:type|,
\lstinline|o:restriction|, \lstinline|o:quant|, \lstinline|o:force|, \lstinline|o:deps|,
and \lstinline|o:scope| can be used to point to the respective functional parts of the
declaration. Consider for instance the declaration \nlex{$\delta\in\mathbb{R}^+$} from
(\ref{ex:nlbinder}). This would be marked up via the declaration attributes as shown in
vocabularies) allow foreign-namespace attributes and ignore them.}). Additional
attributes \lstinline|o:decname|, \lstinline|o:type|, \lstinline|o:restriction|,
\lstinline|o:quant|, \lstinline|o:force|, \lstinline|o:deps|, and \lstinline|o:scope| can
be used to point to the respective functional parts of the declaration. Consider for
instance the declaration \nlex{$\delta\in\mathbb{R}^+$} from (\ref{ex:nlbinder}). This
would be marked up via the declaration attributes as shown in
Listing~\ref{lst:nlbinder}. Here we have an existential declaration for the identifier
$\delta$\footnote{The force determined by the context of \nlex{$\delta\in\mathbb{R}^+$} in
(\ref{ex:nlbinder}), but it should be considered a trait of the
......@@ -297,7 +297,9 @@ we use a list of references in \lstinline|decname| to point to the two identifie
<m:apply>
<m:csymbol name="arith">abs</m:csymbol>
<m:apply>
<m:csymbol name="arith">minus</m:csymbol><m:ci id="x">x</m:ci><m:ci id="y">y</m:ci>
<m:csymbol name="arith">minus</m:csymbol>
<m:ci id="x">x</m:ci>
<m:ci id="y">y</m:ci>
</m:apply>
</m:apply>
<m:ci>$\delta$</m:ci>
......@@ -319,7 +321,7 @@ uses a highly aggregated form.
<m:apply>
<m:csymbol cd="numbers-orders">greater</m:csymbol>
<m:ci id="n">n</m:ci>
<m:mn>10</m:mn>
<m:cn>10</m:cn>
</m:apply>
<h:span> is prime</h:span>
</h:span>
......@@ -373,18 +375,17 @@ As the concept of tree depth is global, we reserve the system identifier
choice does not influence the verbalization or notation of the symbol.} using the \omdoc
\lstinline|m:symbol| element.
\omdoc notation definitions (the \lstinline|o:notation| element) are a
device for presenting content formulae. They consist of pairs of formula schemata, one in
content \mathml -- the \defemph{prototype} -- used to match a content \mathml expression,
and render it as the presentation \mathml expression in the
\defemph{rendering}\footnote{We can also use them the other way around for
notation-definition driven parsing, matching presentation \mathml formulae view the
\lstinline|o:rendering| element and constructing content \mathml formulae
via the \lstinline|o:prototype| element.}; the instances of any
\lstinline|o:expr| elements are rendered recursively. Note that the
matching-based setup allows to distinguish `applied' occurrences for functional objects;
see~\cite{KMR:NoLMD08} for details. In our example the notation definition in lines 2 to 7
of Listing~\ref{lst:treedepth} introduces the formula notation for tree depth.
\omdoc notation definitions (the \lstinline|o:notation| element) are a device for
presenting content formulae. They consist of pairs of formula schemata, one in content
{\mathml} -- the \defemph{prototype} -- used to match a content \mathml expression, and
render it as the presentation \mathml expression in the \defemph{rendering}\footnote{We
can also use them the other way around for notation-definition driven parsing, matching
presentation \mathml formulae view the \lstinline|o:rendering| element and constructing
content \mathml formulae via the \lstinline|o:prototype| element.}; the instances of any
\lstinline|o:expr| elements are rendered recursively. Note that the matching-based setup
allows to distinguish `applied' occurrences for functional objects; see~\cite{KMR:NoLMD08}
for details. In our example the notation definition in lines 2 to 7 of
Listing~\ref{lst:treedepth} introduces the formula notation for tree depth.
The verbalization for the symbol \lstinline|tdepth| is marked up with the \lstinline|o:term|
element: The first occurrence of the relational noun \nlex{depth} is marked as a
......@@ -455,16 +456,16 @@ two content \mathml expressions that formalize it.
\end{figure}
On the right side of Figure~\ref{fig:definition} we see the dual situation, where a formal
definition via a \lstinline|o:constant| element is annotated by two
narrative (definition) texts \tmeta{text1} and \tmeta{text2}. In this way we can start
with a narrative statement and formalize it in place by annotating it with ``content
\omdoc'' or start with formal content (e.g. from a theorem prover) and annotate it with
generated ``presentation \omdoc'' for human consumption. As in Section~\ref{sec:mixing} we
can freely interleave formal and informal parts, and as in Section~\ref{sec:intro:object}
we can use parallel markup to represent ambiguity. Note that we do not need an \omdocv2
analogue to the generic \lstinline|semantics| element in MathML, since the
statement-level elements in \omdoc and \mmt already have the grouping capabilities needed
to form a single root as required by XML.
definition via a \lstinline|o:constant| element is annotated by two narrative (definition)
texts \tmeta{text1} and \tmeta{text2}. In this way we can start with a narrative statement
and formalize it in place by annotating it with ``content \omdoc'' or start with formal
content (e.g. from a theorem prover) and annotate it with generated ``presentation
\omdoc'' for human consumption. As in Section~\ref{sec:mixing} we can freely interleave
formal and informal parts, and as in Section~\ref{sec:intro:object} we can use parallel
markup to represent ambiguity. Note that we do not need an \omdocv2 analogue to the
generic \lstinline|semantics| element in MathML, since the statement-level elements in
\omdoc and \mmt already have the grouping capabilities needed to form a single root as
required by XML.
\subsubsection{Inline Statements}\label{sec:inline-statements}
......@@ -592,47 +593,57 @@ the relevant logic or logical framework. In order to more precisely express the
between logical framework and logic or logic and theory, \omdoc provides the \cn{meta}
relation as a distinguished kind of import.
\begin{wrapfigure}r{4.7cm}\vspace*{-1em}\centering
\begin{tikzpicture}[yscale=.9]
\begin{wrapfigure}r{5.5cm}\vspace*{-1em}\centering
\begin{tikzpicture}[yscale=.7]
\node[thy] (FOL) at (-1,1.5) {\cn{FOL}};
\node[thy] (SFOL) at (1,1.5) {\cn{SFOL}};
\node[thy] (LF) at (0,3) {\cn{LF}};
\node[thy] (Mon) at (0,0) {\cn{CGroup}};
\node[thy] (Rg) at (-2,0) {\cn{Ring}};
\node[thy] (Cg) at (0,0) {\cn{CGroup}};
\node[thy] (Rg) at (2,0) {\cn{Ring}};
\node[thy] (Mon) at (-1.8,0) {\cn{Monoid}};
\draw[include] (Mon) -- node[above] {\cn{add}} (Rg);
\draw[struct] (Cg) -- node[above] {\footnotesize\cn{add}} (Rg);
\draw[struct] (Mon) to[out=-15,in=195] node[below] {\footnotesize\cn{mul}} (Rg);
\draw[include] (Mon) -- (Cg);
\draw[meta] (LF) -- (FOL);
\draw[meta] (LF) -- (SFOL);
\draw[meta] (FOL) -- (Cg);
\draw[meta] (SFOL) -- (Rg);
\draw[meta] (FOL) -- (Mon);
\draw[meta] (FOL) -- (Rg);
\draw[view] (FOL) -- node[above] {\cn{m}} (SFOL);
%%legend
\node (IF) at (-2.9,1.8) {};
\node (IT) at (-1.7,1.8) {};
\node (MF) at (-2.9,2.4) {};
\node (MT) at (-1.7,2.4) {};
\node (IF) at (-2.9,.6) {};
\node (IT) at (-1.7,.6) {};
\node (SF) at (-2.9,1.4) {};
\node (ST) at (-1.7,1.4) {};
\node (MF) at (-2.9,2.2) {};
\node (MT) at (-1.7,2.2) {};
\node (VF) at (-2.9,3.0) {};
\node (VT) at (-1.7,3.0) {};
\draw[include] (IF) -- node[above] {\footnotesize \emph{import}} (IT);
\draw[meta] (MF) -- node[above] {\footnotesize \emph{meta}} (MT);
\draw[view] (VF) -- node[above] {\footnotesize \emph{view}} (VT);
\draw[struct] (SF) -- node[above] {\footnotesize \emph{structure}} (ST);
\end{tikzpicture}
\caption{Pluralism in OMDoc}\label{fig:ex-log-pl}
\end{tikzpicture}\vspace*{-1em}
\caption{Pluralism in OMDoc}\label{fig:ex-log-pl}\vspace*{-.5em}
\end{wrapfigure}
Using views, translations at the logical or logical-framework level, induce translation at the lower levels allowing one to relate different logical
languages and make use of that by, e.g. automatically translating documents from one logic to another.
Using views, translations at the logical or logical-framework level, induce translation at
the lower levels allowing one to relate different logical languages and make use of that
by, e.g. automatically translating documents from one logic to another.
Figure~\ref{fig:ex-log-pl} (extending the example in Figure~\ref{fig:ex-thy-graph}) shows
an instance of logical pluralism in \omdoc/\mmt where the logical framework \cn{LF} and
the logics \cn{FOL} (First-Order Logic) and \cn{SFOL} (Sorted First-Order Logic) are
declared as theories. Then, \cn{Ring} and \cn{Monoid} build on \cn{FOL} and the relation
between \cn{FOL} and \cn{SFOL} is formalized as a view, inducing a translation of
\cn{Ring} and \cn{Monoid} into \cn{SFOL}.
declared as theories. Then, \cn{Monoid} and \cn{Cgroup} build on \cn{FOL}, while \cn{Ring}
-- for the sake of argument -- has \cn{SFOL} as a meta-theory. The relation between
\cn{FOL} and \cn{SFOL} is formalized as a view, inducing a translation of \cn{Ring} and
\cn{Monoid} into \cn{SFOL}, which gives meaning to the two structures \cn{add} and
\cn{mul} that make up most of the content of \cn{Ring}.
\subsubsection{Understanding Framing}\label{sec:framing}
......@@ -666,18 +677,19 @@ primary goal of the \omdoc format from the start, here we are only applying it t
\end{tikzpicture}\vspace*{-.5em}
\caption{Framing Spaces}\label{fig:fram}\vspace*{-.5em}
\end{wrapfigure}
Consider for instance the situation in example (\ref{ex:fram2}), where we have the absolute
value $|\cdot|$ on $\mathbb{R}$, which, together with the fact that $\mathbb{R}$ forms a
one-dimensional vector space over the field of real numbers (witnessed by view
Consider for instance the situation in example (\ref{ex:fram2}), where we have the
absolute value $|\cdot|$ on $\mathbb{R}$, which, together with the fact that $\mathbb{R}$
forms a one-dimensional vector space over the field of real numbers (witnessed by view
$\mathsf{v_1}$), makes \textsf{NReal1} into a normed vector space (see view
$\mathsf{v_2}$). Furthermore, we have a view $\mathsf{v_4}$ from the theory \textsf{TopSp}
of topological spaces to the theory \textsf{MetSp} of metric spaces: the topology
$\mathcal{O}$ over a set $S$ can be defined as the collection of unions of open balls
$\mathsf{ball}(s,r)$ with $s\in S$ and $r\in\mathbb{R}$, where $\mathsf{ball}(s,r):=\{t\in
S|d(s,t)<r\}$. Finally there is a view $\mathsf{v_3}$ from \textsf{MetSp} to the theory
\textsf{NVS} of normed vector spaces: we can define a distance function $d$ by
$d(x,y):=\|x-y\|$. In this situation, flattening supplies the concepts of \nlex{ball} and
\nlex{open} to \textsf{NVS}, accounting for the bridging references in (\ref{ex:fram2}).
$\mathsf{ball}(s,r)$ with $s\in S$ and $r\in\mathbb{R}$, where
$\mathsf{ball}(s,r):=\{t\in S|d(s,t)<r\}$. Finally there is a view $\mathsf{v_3}$ from
\textsf{MetSp} to the theory \textsf{NVS} of normed vector spaces: we can define a
distance function $d$ by $d(x,y):=\|x-y\|$. In this situation, flattening supplies the
concepts of \nlex{ball} and \nlex{open} to \textsf{NVS}, accounting for the bridging
references in (\ref{ex:fram2}).
For (\ref{ex:fram1}) we need to explain the application of the adjective \nlex{discrete}
to the complex noun \nlex{normed vector space}. Recall that a metric space is called
......
No preview for this file type
......@@ -109,7 +109,7 @@
\section{Phenomena of Mathematical Vernacular} \label{sec:pheno}
\input{phenomena}
\section{Requirements for a target language for semantics construction analysis} \label{sec:req}
\section{Requirements for a Target Language for Semantics Construction Analysis} \label{sec:req}
\input{requirements}
% \section{Active Documents}\label{sec:activdocs}
% \input{activdocs}
......
......@@ -58,7 +58,7 @@ The Naproche project~\cite{CramerFKKSV09} starts from the common mathematical la
(\scorezero{\phenref{flexiform}}) and a proof checking software to formally check texts
written in this language. Therefore, the Naproche CNL focuses on proofs to permit adequate
proof checking by the Naproche system and doesn't necessarily aim to cover all phenomena
from section~\ref{sec:pheno}. Still, it is interesting to evaluate it with respect to
from Section~\ref{sec:pheno}. Still, it is interesting to evaluate it with respect to
these requirements.
At the phrase level, the Naproche CNL includes a language for formulae which can be
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment