Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
P
papers
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
iMMT
papers
Commits
8c8bc209
Commit
8c8bc209
authored
Mar 2, 2015
by
Michael Kohlhase
Browse files
Options
Downloads
Patches
Plain Diff
finished recap
parent
727264ab
No related branches found
No related tags found
No related merge requests found
Changes
3
Show whitespace changes
Inline
Side-by-side
Showing
3 changed files
adoptions/conc.tex
+1
-1
1 addition, 1 deletion
adoptions/conc.tex
adoptions/paper.pdf
+0
-0
0 additions, 0 deletions
adoptions/paper.pdf
adoptions/patterns.tex
+30
-28
30 additions, 28 deletions
adoptions/patterns.tex
with
31 additions
and
29 deletions
adoptions/conc.tex
+
1
−
1
View file @
8c8bc209
...
...
@@ -25,7 +25,7 @@ applicable.
\item
auto-generation of recap material from content commons
\item
need a community process of moving ``original theory'' towards encyclopedias.
\end{todolist}
\ednote
{
multiple recaps
}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "paper"
...
...
This diff is collapsed.
Click to expand it.
adoptions/paper.pdf
+
0
−
0
View file @
8c8bc209
No preview for this file type
This diff is collapsed.
Click to expand it.
adoptions/patterns.tex
+
30
−
28
View file @
8c8bc209
...
...
@@ -120,17 +120,9 @@ In our analysis we restrict ourselves to the case where there is a single recap
simplicity and expositional clarity. The approach can be extended to multiple recaps from
the same realm with minimal effort -- but the diagrams become messy. This already covers
the majority of research papers we have analyzed; they build on an earlier paper and
extend it. All three examples from Section~
\ref
{
sec:cg-preprints
}
fall into this category,
they import the definitions and terminology from a central cited paper, but call on others
from the same realm for results, context, and support.
\begin{oldpart}
{
this cannot be understood here
}
In informal mathematics
$
v
$
is usually not explicitly given, but it may or may not be
justified. In case it is not we call
$
v
$
a
\emph
{
postulated
}
view. The relation
$
r
$
is
between the recap and the cited paper is left unspecified at this point as we
distinguish several cases below.
\end{oldpart}
extend it. Indeed, all three examples from Section~
\ref
{
sec:cg-preprints
}
fall into this
category, they import the definitions and terminology from a central cited paper, but call
on others from the same realm for results, context, and support.
%Mathematical papers re-introduce concepts with the implied assumption of semantic equivalence in the context of the paper.
%I.e. every statement in the paper holds for the original definition too, but not necessarily the converse.
...
...
@@ -312,16 +304,6 @@ written down in the paper as ``\textsf{There are several equivalent ways to defi
sample papers we studied.
% Moreover, examples \ref{ex:quant} and \ref{ex:calculi} also fit in this category.
\begin{oldpart}
{
either put somewhere or delete
}
The implicit or explicit equivalence of the local definitions in the recap theory that
the view
$
v
$
from the face exists and therefore that theorems from the mathematical
field can be used in the paper. In case the equivalence is implicit we speak of a
\emph
{
postulated
}
view, i.e. one where the assigned expressions are (partially)
informal. A flexiformal system can still reason about the meaning travel induced by a
postulated view but cannot look into assigned objects and e.g. proof check them.
\end{oldpart}
\begin{figure}
[ht]
\centering
\begin{tikzpicture}
%realm
...
...
@@ -512,14 +494,18 @@ precisely but there are some interesting things there, we should talk about it}
\caption
{
Publication graph for specialization recaps (using Example
\ref
{
ex:atm
}
)
}
\label
{
fig:rec-atm
}
\end{figure}
\paragraph
{
Postulated Recap/Adoption
}
\label
{
rc:ge
}
Finally, we have the case where
$
s
$
is a plain (partial) include that does not entail conservativity and therefore does not entail
the existence
$
v
$
. In that case we call
$
v
$
a
\emph
{
postulated
}
view and the recap itself an
\emph
{
adoption
}
.
\subsection
{
Postulated Recap/Adoption
}
\label
{
rc:ge
}
This is the case in example
\ref
{
ex:course
}
where the recap theory
\cn
{
SET
}
includes only the symbols
$
\in
$
and
$
\{\cdot
,
\cdot\}
$
from
the formal development
\cn
{
ZFset
}
, but not their axioms. Instead the symbols are ``defined'' by alluding to the literature (common knowledge).
We claim this verbalization effectively postulates the existence of
$
v
$
, by implying that the semantics of the two symbols is compatible with that
given in the literature (which we represent as a realm).
Finally, we have the case where
$
s
$
is a plain (partial) include that does not entail
conservativity and therefore does not entail the existence
$
v
$
. In that case we call
$
v
$
a
\emph
{
postulated
}
view and the recap itself an
\emph
{
adoption
}
.
This is the case in example
\ref
{
ex:course
}
where the recap theory
\cn
{
SET
}
includes only
the symbols
$
\in
$
and
$
\{\cdot
,
\cdot\}
$
from the formal development
\cn
{
ZFset
}
, but not
their axioms. Instead the symbols are ``defined'' by alluding to the literature (common
knowledge). We claim this verbalization effectively postulates the existence of
$
v
$
, by
implying that the semantics of the two symbols is compatible with that given in the
literature (which we represent as a realm).
\begin{figure}
[ht]
\centering
\begin{tikzpicture}
...
...
@@ -570,6 +556,22 @@ given in the literature (which we represent as a realm).
\end{figure}
\begin{oldpart}
{
from the equivalence example
}
The implicit or explicit equivalence of the local definitions in the recap theory that
the view
$
v
$
from the face exists and therefore that theorems from the mathematical
field can be used in the paper. In case the equivalence is implicit we speak of a
\emph
{
postulated
}
view, i.e. one where the assigned expressions are (partially)
informal. A flexiformal system can still reason about the meaning travel induced by a
postulated view but cannot look into assigned objects and e.g. proof check them.
\end{oldpart}
\begin{oldpart}
{
this cannot be understood here
}
In informal mathematics
$
v
$
is usually not explicitly given, but it may or may not be
justified. In case it is not we call
$
v
$
a
\emph
{
postulated
}
view. The relation
$
r
$
is
between the recap and the cited paper is left unspecified at this point as we
distinguish several cases below.
\end{oldpart}
%%% Local Variables:
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment