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

tweaks

parent 3c1f7b59
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
adoptions/local.bib
+ 3
− 1
View file @ c2d5310e
......@@ -47,9 +47,11 @@ archivePrefix = "arXiv",
}
%%%% Covers
@MISC{covers-orig,
@online{covers-orig,
author = {Tapani {Hyttinen} and Kaisa {Kangas}},
title = {On model theory of covers of algebraically closed fields},
url = {http://arxiv.org/pdf/1502.01042.pdf},
urldate = {2015-02-16},
year = {2015}
}
......
adoptions/paper.pdf
+ 0
− 0
View file @ c2d5310e
No preview for this file type
adoptions/paper.tex
+ 4
− 1
View file @ c2d5310e
\documentclass{llncs}
\usepackage{url,amstext,amssymb,textcmds}
\usepackage{tikz,standalone}
\usepackage{tikz,standalone,wrapfig}
\usepackage{labeledquote,xspace}
\usetikzlibrary{shapes,arrows}
\usetikzlibrary{mmt}
......@@ -23,6 +23,9 @@
\addbibresource{kwarc.bib}
\usepackage{local}
\tikzstyle{prerealm}=[draw=blue!40,rectangle,rounded corners,inner sep=10pt,inner ysep=20pt]
\tikzstyle{realm}=[prerealm,fill=gray!4]
\tikzstyle{pillar}=[prerealm,fill=gray!10]
%\title{Theory Level Structures in Informal Mathematics}
\title{A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics}
......
adoptions/patterns.tex
+ 56
− 55
View file @ c2d5310e
In this section we look more closely at the examples from section \ref{sec:pheno} and how each can be represented
using theory graphs.
But first, we look at the aspects common to all examples to form an intuition of the theory graphs structures that are needed.
In this section we look more closely at the examples from section \ref{sec:pheno} and how
each can be represented using theory graphs. But first, we look at the aspects common to
all examples to form an intuition of the theory graphs structures that are needed.
The examples in section \ref{sec:pheno} are each slightly different but they have fundamental common aspects.
First, each paper starts with establishing a common ground on which the results of the paper are built. This leverages the literature in two ways.
......@@ -36,13 +36,13 @@ The relation $r$ is between the recap and the cited paper is left unspecified at
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.7) rectangle (5,2.8) {};
\draw[realm] (-1,-1.7) rectangle (5,2.8) {};
%p-paper
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4.2,-0.5) rectangle (-1.8,2.8) {};
\draw[pillar] (-4.2,-0.5) rectangle (-1.8,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[pillar] (-0.5,-1.5) rectangle (1.5,1.8) {};
%p2
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\draw[pillar] (2.5,-1.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,2.6) {$\mathit{Realm}$};
\node (p-name) at (-1.7,2.6) {$\mathit{Paper}$};
......@@ -75,8 +75,8 @@ The relation $r$ is between the recap and the cited paper is left unspecified at
\draw[conservative] (citp) to (top1);
\draw[conservative] (bot2) to (top2);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\end{tikzpicture}
\caption{General Case for Recaps}\label{fig:rec-gen}
\end{figure}
......@@ -103,13 +103,13 @@ It also makes $v$ exist as induced by $v_1$ modulo conservativity.
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.7) rectangle (5,2.8) {};
\draw[realm] (-1,-1.7) rectangle (5,2.8) {};
%p-paper
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4.5,-0.5) rectangle (-1.5,2.8) {};
\draw[pillar] (-4.5,-0.5) rectangle (-1.5,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[pillar] (-0.5,-1.5) rectangle (1.5,1.8) {};
%p2
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\draw[pillar] (2.5,-1.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,2.6) {$\mathit{Realm}$};
\node (p-name) at (-2,2.6) {$\mathit{Paper}$};
......@@ -141,8 +141,8 @@ It also makes $v$ exist as induced by $v_1$ modulo conservativity.
\draw[conservative] (citp) to (top1);
\draw[conservative] (bot2) to (top2);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\end{tikzpicture}
\caption{Publication graph for plain recaps (using Example \ref{ex:covers})}\label{fig:rec-covers}
\end{figure}
......@@ -151,11 +151,11 @@ It also makes $v$ exist as induced by $v_1$ modulo conservativity.
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-3,-3.7) rectangle (5,2.8) {};
\draw[realm] (-3,-3.7) rectangle (5,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-2.5,-3.5) rectangle (1.5,1.8) {};
\draw[pillar] (-2.5,-3.5) rectangle (1.5,1.8) {};
%p2
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-3.5) rectangle (4.5,1.8) {};
\draw[pillar] (2.5,-3.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,2.6) {$\mathit{Realm}$};
\node (p1-name) at (-2,1.6) {$\mathit{Pillar_1}$};
......@@ -189,16 +189,17 @@ It also makes $v$ exist as induced by $v_1$ modulo conservativity.
\draw[conservative] (bot2) to (top2);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\end{tikzpicture}
\caption{Aggregation graph for plain recaps (using Example \ref{ex:covers})}\label{fig:rec-covers}
\end{figure}
\paragraph{Special Case: Equivalence Recap} \label{rc:eq}
Another common situation is that of equivalence recaps where the relation $r$ is an equivalence (isomorphism) between the two theories.
We can represent the relation $r$, in this case, as two views $v_{to}$ and $v_{from}$, one in each direction between the recap and the cited paper that
ensure their isomorphism. Then, the view $v$ is induced by $v_{from} \circ v_1$ modulo conservativity.
\paragraph{Special Case: Equivalence Recap} \label{rc:eq} Another common situation is that
of equivalence recaps where the relation $r$ is an equivalence (isomorphism) between the
two theories. We can represent the relation $r$, in this case, as two views $v_{to}$ and
$v_{from}$, one in each direction between the recap and the cited paper that ensure their
isomorphism. Then, the view $v$ is induced by $v_{from} \circ v_1$ modulo conservativity.
Moreover, the contribution of the paper carries over to the realm via the view $v_{to}$.
This occurs, for instance, in example \ref{ex:mnets} where this intuition is explicitly written down in the paper as ``There are several equivalent ways to
......@@ -215,13 +216,13 @@ A flexiformal system can still reason about the meaning travel induced by a post
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.7) rectangle (5,2.8) {};
\draw[realm] (-1,-1.7) rectangle (5,2.8) {};
%p-paper
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4.5,-0.5) rectangle (-1.5,2.8) {};
\draw[pillar] (-4.5,-0.5) rectangle (-1.5,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[pillar] (-0.5,-1.5) rectangle (1.5,1.8) {};
%p2
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\draw[pillar] (2.5,-1.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,2.6) {$\mathit{Realm}$};
\node (p-name) at (-2,2.6) {$\mathit{Paper}$};
......@@ -246,8 +247,8 @@ A flexiformal system can still reason about the meaning travel induced by a post
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[view,red, bend left = 15] (citp) to node[below] {$\cn{v_{from}}$} (recap);
\draw[view,red, bend left = 15] (recap) to node[below] {$\cn{v_{to}}$} (citp);
\draw[view,red, bend left = 10] (citp) to node[below] {$\cn{v_{from}}$} (recap);
\draw[view,red, bend left = 10] (recap) to node[above] {$\cn{v_{to}}$} (citp);
\draw[conservative] (recap) to (pcont);
......@@ -256,8 +257,8 @@ A flexiformal system can still reason about the meaning travel induced by a post
\draw[conservative] (citp) to (top1);
\draw[conservative] (bot2) to (top2);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\end{tikzpicture}
\caption{Publication graph for equivalence recaps (using Example \ref{ex:mnets})}\label{fig:rec-mnets}
\end{figure}
......@@ -274,13 +275,13 @@ we take into account conservativity to reduce them to the $\bot$ theory.
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4,-1.7) rectangle (5,2.8) {};
\draw[realm] (-4,-1.7) rectangle (5,2.8) {};
%p0
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-3.5,-1.5) rectangle (-1.5,1.8) {};
\draw[pillar] (-3.5,-1.5) rectangle (-1.5,1.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[pillar] (-0.5,-1.5) rectangle (1.5,1.8) {};
%p2
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\draw[pillar] (2.5,-1.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,2.6) {$\mathit{Realm}$};
\node (p3-name) at (-2.8,1.6) {$\mathit{Pillar_{n+1}}$};
......@@ -304,11 +305,11 @@ we take into account conservativity to reduce them to the $\bot$ theory.
\node[thy] (r) at (0.5,2.3) {Realm Face};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[view,red, bend left = 15] (bot1) to node[below] {$\cn{v_{from}}$} (recap);
\draw[view,red, bend left = 15] (recap) to node[below] {$\cn{v_{to}}$} (bot1);
\draw[view,red, bend left = 10] (bot1) to node[below] {$\cn{v_{from}}$} (recap);
\draw[view,red, bend left = 10] (recap) to node[above] {$\cn{v_{to}}$} (bot1);
\draw[conservative] (recap) to (pcont);
......@@ -317,8 +318,8 @@ we take into account conservativity to reduce them to the $\bot$ theory.
\draw[conservative] (citp) to (top1);
\draw[conservative] (bot2) to (top2);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\end{tikzpicture}
\caption{Aggregation graph for equivalence recaps (using Example \ref{ex:mnets})}\label{fig:rec-mnets-aggr}
\end{figure}
......@@ -344,15 +345,15 @@ precisely but there are some interesting things there, we should talk about it}
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.7) rectangle (5,2.8) {};
\draw[realm] (-1,-1.7) rectangle (5,2.8) {};
%p-paper
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-6,-0.5) rectangle (-4,2.8) {};
\draw[pillar] (-6,-0.5) rectangle (-4,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[pillar] (-0.5,-1.5) rectangle (1.5,1.8) {};
%p2
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\draw[pillar] (2.5,-1.5) rectangle (4.5,1.8) {};
%realm2
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-3.5,-1.8) rectangle (-1.5,-.5) {};
\draw[realm] (-3.5,-1.8) rectangle (-1.5,-.5) {};
\node (r-name) at (4.5,2.6) {$\mathit{Realm}$};
......@@ -392,8 +393,8 @@ precisely but there are some interesting things there, we should talk about it}
\draw[conservative] (citp) to (top1);
\draw[conservative] (bot2) to (top2);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\end{tikzpicture}
\caption{Publication graph for specialization recaps (using Example \ref{ex:atm})}\label{fig:rec-atm}
\end{figure}
......@@ -410,13 +411,13 @@ given in the literature (which we represent as a realm).
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.7) rectangle (5,2.8) {};
\draw[realm] (-1,-1.7) rectangle (5,2.8) {};
%p-paper
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4.5,-0.5) rectangle (-1.5,2.8) {};
\draw[pillar] (-4.5,-0.5) rectangle (-1.5,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[pillar] (-0.5,-1.5) rectangle (1.5,1.8) {};
%p2
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\draw[pillar] (2.5,-1.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,2.6) {$\mathit{Realm}$};
\node (p-name) at (-2,2.6) {$\mathit{Paper}$};
......@@ -449,8 +450,8 @@ given in the literature (which we represent as a realm).
\draw[conservative] (citp) to (top1);
\draw[conservative] (bot2) to (top2);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\end{tikzpicture}
\caption{Publication graph for generalization/unspecified recaps (using Example \ref{ex:course})}\label{fig:rec-slides}
\end{figure}
......
adoptions/phenomena.tex
+ 51
− 115
View file @ c2d5310e
......@@ -4,113 +4,53 @@ A common pattern occurs in scientific papers which often have a preliminaries se
recapitulate the central notions and fix notations. In its simplest incarnation this can be seen
as an import. However, in general, it can have a more complex behavior (e.g. see example \ref{ex:atm}).
\begin{example}[http://arxiv.org/pdf/1502.00573.pdf] \label{ex:quant}
\cite{quant-orig} discusses quantifier elimination in $C^*$-algebras and begins by defining the formulas for $C^*$-algebras after the
the introduction.
\begin{labeledquote}\label{def:quant}
\begin{definition}
The \emph{formulas} for $C^*$-algebras are recursively defined as follows.
In each case, $\overline{x}$ denotes a finite tuple of variables (which will later be interpreted as
elements of a $C^*$-algebra).
\begin{itemize}
\item[(1)] If $P(\overline{x})$ is a $*$-polynomial with complex coefficients, then $\|P(\overline{x})\|$ is a formula.
\item[(2)] If $\varphi_1(\overline{x}), . . . , \varphi_n(\overline{x})$ are formulas and $f : \mathbb{R}^n \arr \mathbb{R}$ is continuous, then
$f(\varphi_1(x), . . . , \varphi_n(x))$ is a formula.
\item[(3)] If $\varphi(\overline{x}, y)$ is a formula and $R \in \mathbb{R}^+$
+, then $\mathrm{sup}_{\|y\| \leq R} \varphi(\overline{x}, y)$ and $\mathrm{inf}_{\|y\| \leq R} \varphi(\overline{x}, y)$
are formulas.
\end{itemize}
We think of $\mathrm{sup}_{\|y\| \leq R}$ and $\mathrm{inf}_{\|y\| \leq R}$ as replacements for the first-order quantifiers
$\forall$ and $\exists$, respectively. A formula constructed using only clauses (1) and (2) of the
definition is therefore said to be \emph{quantifier-free}.
\end{definition}
\begin{example}\label{ex:covers}
\cite{covers-orig} discusses covers of the multiplicative group of an algebraically
closed field which are formally defined in the beginning of the paper as follows:
\begin{labeledquote}\sf
\textbf{Definition 1.1} Let $V$ be a vector space over $Q$ and let $F$ be an
algebraically closed field of characteristic $0$. A \emph{cover of the multiplicative
group} of $F$ is a structure represented by an exact sequence
$0 \arr K \arr V \arr F^∗ \arr 1$ , where the map $V \arr F^*$ is a surjective group
homomorphism from $(V, +)$ onto $(F^∗, \cdot)$ with kernel $K$. We will call this map
\emph{exp}.
\end{labeledquote}
The authors refer to \cite{quant-fs14} for a more complete discussion although it uses a slightly different definition. In fact, the
authors explicitly acknowledge that later:
``The definition above is slightly different from the one in \cite{quant-fs14} [...]
Since the two versions are equivalent, we have chosen an approach intended to minimize
the technical complexity of the definitions.''.
\end{example}
\begin{example}{http://arxiv.org/pdf/1502.00978.pdf}\label{ex:calculi}
\cite{calculi-orig} proves some results about undecidable problems for propositional calculi.
In the preliminaries it introduces notations and definitions from scratch:
\begin{labeledquote}
Let us consider the language consisting of an infinite set of propositional variables
$V$ and the signature $\Sigma$, i.e., a finite set of connectives. Letters
$x, y, z, u, p$ , etc., are used to denote propositional variables.
Usually connectives are binary or unary such as $\neg, \vee, \wedge,$ or $\arr$.
\end{labeledquote}
However, it still relies on the literature to fully define the local concepts:
``Propositional formulas or $\Sigma$-formulas are built up from the signature
$\Sigma$ and propositional variables $V$ \emph{in the usual way}. '' [emphasis ours]
When, establishing results, \cite{covers-orig} mentions ``\textsf{Moreover, with an
additional axiom (in $L_{\omega_1\omega}$) stating $K \cong Z$, the class is categorical
in uncountable cardinalities. This was originally proved in \cite{covers-13} but an
error was later found in the proof and corrected in \cite{covers-2}}''.
The paper continues by introducing previous results, by mapping them (implicitly) to the definitions introduced
locally. For instance :
\begin{labeledquote}
\begin{theorem}[Theorem 2.1]
(Linial and Post, 1949). \textbf{Axm}, \textbf{Ext}, and \textbf{Cmpl} are undecidable for $\textbf{Cl}_{\{\neg, \wedge\}}$.
\end{theorem}
\end{labeledquote}
where \textbf{Axm}, \textbf{Axm}, \textbf{Ext}, \textbf{Cmpl} and \textbf{Cl} are all defined locally.
Having established local concepts and their properties (via the literature) the paper continues with its contribution.
However, \cite{covers-orig} uses a generalization of the concept in \cite{covers-13} which
uses the sequence $0 \arr Z \arr C \arr C^* \arr 1$ instead (although later proves some
generalizations). Moreover, \cite{covers-2} also extends the result in \cite{covers-13}
and additionally fixes a hole in the proof mentioned above.
\end{example}
\begin{example}{http://arxiv.org/pdf/1502.01042.pdf}\label{ex:covers}
\cite{covers-orig} discusses covers of the multiplicative group of an algebraically closed field which are formally defined in the beginning
of the paper as follows:
\begin{labeledquote}
\begin{definition}
Let $V$ be a vector space over $Q$ and let $F$ be an algebraically closed field
of characteristic $0$. A \emph{cover of the multiplicative group} of $F$ is a structure represented by
an exact sequence
$0 \arr K \arr V \arr F^∗ \arr 1$ ,
where the map $V \arr F^*$ is a surjective group homomorphism from $(V, +)$ onto
$(F^∗, \cdot)$ with kernel $K$. We will call this map \emph{exp}.
\end{definition}
\begin{example}\label{ex:mnets}
\cite{mnets-orig} studies the properties of multinets. In the preliminaries section they
are introduced with the following definition:
\begin{labeledquote}\sf
\textbf{Definition 2.1} The union of all completely reducible fibers (with a fixed
partition into fibers, also called blocks) of a Ceva pencil of degree $d$ is called a
$(k, d)-\mathit{multinet}$ where $k$ is the number of the blocks. The base $X$ of the
pencil is determined by the multinet structure and called the base of the multinet.
\end{labeledquote}
When, establishing results, \cite{covers-orig} mentions ``Moreover, with an additional axiom (in $L_{\omega_1\omega}$) stating $K \cong Z$, the class is categorical
in uncountable cardinalities. This was originally proved in \cite{covers-13} but an error was later found
in the proof and corrected in \cite{covers-2}''.
However, \cite{covers-orig} uses a generalization of the concept in \cite{covers-13} which uses the sequence
$0 \arr Z \arr C \arr C^* \arr 1$ instead (although later proves some generalizations). Moreover, \cite{covers-2} also
extends the result in \cite{covers-13} and additionally fixes a hole in the proof mentioned above.
\end{example}
\begin{example}{http://arxiv.org/pdf/1502.02059.pdf}\label{ex:mnets}
\cite{mnets-orig} studies the properties of multinets. In the preliminaries section they are introduced with the following
definition:
\begin{labeledquote}
\begin{definition} The union of all completely reducible fibers (with a fixed partition
into fibers, also called blocks) of a Ceva pencil of degree $d$ is called a $(k, d)-\mathit{multinet}$
where $k$ is the number of the blocks. The base $X$ of the pencil is determined by the multinet structure and called the base of the multinet.
\end{definition}
\end{labeledquote}
Later in that section some properties of multinets are introduced with the phrase ``Several important properties of
multinets are listed below which have been collected from \cite{mnets-ref4, mnets-ref10, mnets-ref12}.''
The referenced papers all use slightly different definitions of multinets but they are assumed to be equivalent so that the properties
hold. In fact, in this paper (\cite{mnets-orig}) the assumption is made explicit -- although not proved -- from the start: ``There are several equivalent ways to
define multinets. Here we present them using pencils of plane curves.''
Later in that section some properties of multinets are introduced with the phrase
``\textsf{Several important properties of multinets are listed below which have been
collected from \cite{mnets-ref4, mnets-ref10, mnets-ref12}.}''\ednote{MK: we should
not have the real citations in our paper.} The referenced papers all use slightly
different definitions of multinets but they are assumed to be equivalent so that the
properties hold. In fact, in this paper (\cite{mnets-orig}) the assumption is made
explicit -- although not proved -- from the start: ``\textsf{There are several
equivalent ways to define multinets. Here we present them using pencils of plane
curves.}''
\end{example}
\begin{newpart}{@MI: look closer or try to find an example for this}
\begin{example}{http://arxiv.org/pdf/1502.05657v1.pdf}
\ednote{Possible realm merge}
\end{example}
\end{newpart}
\begin{example}\label{ex:atm}
For instance, \cite{CalStai:natm09} contains the sentence
\begin{labeledquote}\em\label{lq:atm}
\begin{labeledquote}\em\label{lq:atm}\sf
An accelerated Turing machine (sometimes called Zeno machine) is a Turing machine that
takes $2^{-n}$ units of time (say seconds) to perform its $n$\textsuperscript{th} step;
we assume that steps are in some sense identical except for the time taken for their
......@@ -123,7 +63,7 @@ supposedly contains the formal definition, which involves generalizing Turing ma
timed ones, introducing computational time structures, and singling out accelerating ones,
e.g. using (\ref{lq:atm-formal}).
\begin{labeledquote}\label{lq:atm-formal}\em
\begin{labeledquote}\label{lq:atm-formal}\sf
\textbf{Definition 1.3}: An \textbf{accelerated Turing machine} is a \underline{Turing
machine} $M=\langle X,\Gamma,S,s_o,\Box,\delta\rangle$ working with with a
\underline{computational time structure} $T= \tup{\{t_i\}_i,<,+}$ with
......@@ -132,23 +72,17 @@ e.g. using (\ref{lq:atm-formal}).
\end{labeledquote}
\end{example}
\begin{oldpart}{from bluenote, not sure what to do with this -- see ednote}
In \cite{CalStaiKoh:natms12} we are undertaking the experiment to
flexiformalize \cite{CalStai:natm09}, and in
this we have to disambiguate the concept of an accelerated Turing machine.
\ednote{MI@MK: couldn't find the paper referenced, link seems broken, couldn't find repo
on strawberry}
\end{oldpart}
In the examples above the papers local definition of a concept (e.g. of a ``Multinet'' or a ``accelerated Turing machine'' (ATM))
is often slightly different from the one referenced in the literature.
Therefore, treating it as an import is not always adequate as, sometimes, the two concepts have clearly distinguishable semantics.
In the examples above the papers local definition of a concept (e.g. of a ``Multinet'' or
a ``accelerated Turing machine'' (ATM)) is often slightly different from the one
referenced in the literature. Therefore, treating it as an import is not always adequate
as, sometimes, the two concepts have clearly distinguishable semantics.
We have two choices for grounding a concept $c$ that occurs in recap :
\begin{compactenum}
\item either we find the ``real definition'' from the literature and use this as the ``origin'' or
\item we consider the introductory sentence in the recap (e.g. \ref{lq:atm} for ATMs in example \ref{ex:atm})
as a definition and use this as the ``origin''.
\item either we find the ``real definition'' from the literature and use this as the
``origin'' or
\item we consider the introductory sentence in the recap (e.g. \ref{lq:atm} for ATMs in
example \ref{ex:atm}) as a definition and use this as the ``origin''.
\end{compactenum}
Which one is better depends on the situation.
If the notion used in the paper is exactly the same as in the literature, we
......@@ -214,9 +148,11 @@ and enables its declarations to be used in the current development.
\paragraph{Mizar}
In Mizar, formal documents (called \emph{articles}) can be exported as PDF files in a human readable format. The narrative documents
contain a part that verbalizes the imports from the source documents and the notation reservations which can be seen as a ``common ground'' section.
Example \ref{ex:mizar} shows the common ground part for the article on ``Fundamental Group of $n$-sphere for $n \geq 2$'' \cite{topalg_6}.
In Mizar, formal documents (called \emph{articles}) can be exported as PDF files in a
human readable format. The narrative documents contain a part that verbalizes the imports
from the source documents and the notation reservations which can be seen as a ``common
ground'' section. Example \ref{ex:mizar} shows the common ground part for the article on
``Fundamental Group of $n$-sphere for $n \geq 2$'' \cite{topalg_6}.
\begin{example}{http://www.degruyter.com/view/j/forma.2012.20.issue-2/v10037-012-0013-1/v10037-012-0013-1.xml} \label{ex:mizar}
\begin{labeledquote}
......
adoptions/prel.tex
+ 34
− 31
View file @ c2d5310e
......@@ -46,12 +46,12 @@ surprisingly stable.
\ednote{to introduce basic OMDoc notions (docs, theories, declarations, verbalizations, notation definitions, URIs)}
\begin{oldpart}{from bluenote}
A central idea behind the OMDoc/OpenMath data model is that all symbols have a home theory
(the document that introduced the concept; essentially the content dictionary). In the
context of flexiformal\footnote{i.e. formalized to flexible depths; see~\cite{KohKoh:tfndc11} and
~\cite{Kohlhase:tffm13} for a discussion of this notion.} digital libraries, this information design creates a tension
between usability (which demand standardized content dictionaries) and
flexibility/locality.
A central idea behind the OMDoc/OpenMath data model is that all symbols have a home
theory (the document that introduced the concept; essentially the content
dictionary). In the context of flexiformal\footnote{i.e. formalized to flexible depths;
see~\cite{KohKoh:tfndc11} and ~\cite{Kohlhase:tffm13} for a discussion of this
notion.} digital libraries, this information design creates a tension between
usability (which demand standardized content dictionaries) and flexibility/locality.
\ednote{Expand, discuss the alternatives, discuss multiple theories and
realms~\cite{CarFarKoh:tr13}.}
\end{oldpart}
......@@ -75,28 +75,21 @@ and provides practitioners with the useful symbols and theorems via an \emph{int
%
% \end{definition}
Figure \ref{fig:realm} shows a prototypical realm with $F$ as its interface theory (also called a \emph{face}) and $n$ pillars each representing a different (yet equivalent)
development of the concepts in the face. Common examples are the different ways to define natural or real numbers. Each pillar is a conservative development in the sense that all
theories in a pillar are conservative extensions of a bottom theory (denoted with $\bot$). A top theory (denoted with $\top$) aggregates all symbols, axioms and theorems declared
within the pillar.
The view pairs at the bottom establish the equivalence of the pillars and the $n$ views $I_k$ capture the relation of interface-implementation between the face and each pillar.
See \cite{CarFarKoh:rsckmt14} for the complete definition and more examples.
\begin{figure}[ht]\centering
\begin{tikzpicture}
\begin{wrapfigure}r{6.3cm}\vspace*{-2em}
\begin{tikzpicture}[xscale=.7]
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.8) rectangle (8,3.5) {};
\draw[realm] (-1,-1.8) rectangle (8,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[pillar] (-0.5,-1.5) rectangle (1.5,1.8) {};
%p..
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
%pn
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (5.5,-1.5) rectangle (7.5,1.8) {};
\node (r-name) at (7.5,3.3) {$\mathit{Realm}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (3,1.6) {$\mathit{Pillar_{\ldots}}$};
\node (p3-name) at (7.0,1.6) {$\mathit{Pillar_n}$};
\node (r-name) at (7.3,2.6) {$\mathit{Realm}$};
\node (p1-name) at (0.2,1.6) {$\mathit{Pillar_1}$};
% \node (p2-name) at (3,1.6) {$\mathit{Pillar_{\ldots}}$};
\node (p3-name) at (6.8,1.6) {$\mathit{Pillar_n}$};
\node[thy] (top1) at (0.5,1) {$\top_1$};
......@@ -110,7 +103,7 @@ See \cite{CarFarKoh:rsckmt14} for the complete definition and more examples.
\node[thy] (bot3) at (6.5,-1) {$\bot_n$};
\node[thy] (r) at (3.5,3) {$\;\;\;\;\;F\;\;\;\;\;$};
\node[thy] (r) at (3.5,2.3) {$\;\;\;\;\;F\;\;\;\;\;$};
\draw[view] (r) to node[above] {$\cn{I_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{I_{\ldots}}$} (top2);
......@@ -121,14 +114,24 @@ See \cite{CarFarKoh:rsckmt14} for the complete definition and more examples.
\draw[conservative] (bot2) to node[left] {$C_{\ldots}$} (top2);
\draw[conservative] (bot3) to node[left] {$C_n$} (top3);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\draw[view, bend left = 15] (bot2) to (bot3);
\draw[view, bend left = 15] (bot3) to (bot2);
\draw[view, bend left = 10] (bot2) to (bot1);
\draw[view, bend left = 10] (bot1) to (bot2);
\draw[view, bend left = 10] (bot2) to (bot3);
\draw[view, bend left = 10] (bot3) to (bot2);
\end{tikzpicture}
\caption{The architecture of a realm}\label{fig:realm}
\end{figure}
\caption{The architecture of a realm}\label{fig:realm}\vspace*{-1em}
\end{wrapfigure}
Figure \ref{fig:realm} shows a prototypical realm with $F$ as its interface theory (also
called a \emph{face}) and $n$ pillars each representing a different (yet equivalent)
development of the concepts in the face. Common examples are the different ways to define
natural or real numbers. Each pillar is a conservative development in the sense that all
theories in a pillar are conservative extensions of a bottom theory (denoted with
$\bot$). A top theory (denoted with $\top$) aggregates all symbols, axioms and theorems
declared within the pillar. The view pairs at the bottom establish the equivalence of the
pillars and the $n$ views $I_k$ capture the relation of interface-implementation between
the face and each pillar. See \cite{CarFarKoh:rsckmt14} for the complete definition and
more examples.
%%% Local Variables:
%%% mode: latex
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment