Discourse-level Parallel Markup and Adopting Meaning in
Flexiformal Theory Graphs

Representation formats based on theory graphs have been very successful
in formalized
mathematics. Theories - sets of symbols and axioms - serve as modules
and theory morphisms
- truth-preserving mappings from the (the language of the) source theory
to the target
theory - formalize inheritance and applicability of theorems. In the MMT
system we have
re-developed the formal part of the OMDoc theory graph into a
foundation-independent
meta-system for formal mathematics and implemented it in the MMT API. 
But full
formalization of mathematical is tedious in the best of situations,
often prohibitively
costly, and forces commitment to irrelevant foundational choices. As it
is also
unnecessary for many applications, we are currently extending the MMT
format to allow
content of flexible formality in an effort to regain the original OMDoc
coverage.

However, in flexiformal representation formats, the basic inventory of
two kinds of theory
morphisms in MMT is insufficient due to the presence of natural language
and presentation
markup in formulae: these are -- in the absence of AI techniques --
opaque to formal
methods. As a consequence, we have to give other means of assigning
meaning to them. In
this paper, we study two interrelated mechanisms for that:

1. extending parallel markup (fine-grained cross-referencing between
presentation and
  content markup originally introduced for formulae in MathML) to the
discourse level and
2. meaning adoption via postulated views.

The first gives meaning to informal statements (definitions, theorems,
proofs) by linking
them with formal counterparts. The second introduces a new kind of
theory morphism that
differs from the two primary MMT ones in its dynamics. Currently MMT has
 
- structures, which contribute to the specification of a target theory
by importing the
  symbols and axioms of the source theory (modulo a mapping).
- views, which establish a meaning-preserving mapping between two
pre-existing theories by
  satisfying proof obligations (proving the translated axioms of the
source) in the target
  theory. Semantically they show that the target is a specialization or
implementation of
  the source.

For meaning adoption we have a situation that is somewhere inbetween.
For instance, we
have the situation of a recap in the introduction of a paper. This
briefly introduces the
concepts and properties necessary to make the paper self-contained
without giving a full
development. Instead their meaning is established by adopting the
referenced development
-- which we assume to be in the form of a theory (graph) for this
discussion. The reader
can remember or accept the content of the recap or read up on the
referenced source. In a
theory graph-based setting we want to understand the relation between a
recap and its
source as a constitutive relation; we call it an adoption. An adoption
behaves dynamically
like a structure in that it adds to the specification of its target --
like a structure it
does not have/need proof obligations, but logically like a view from the
target to the
source, in that it makes the recap a specialization of the full development.

In the paper we will look at additional situations where adoption
happens and work out the
details of postulated views and the influence on property and symbol
inheritance.