spacing

[arxana.git] / org / arxana-redux.org

#+TITLE:     Arxana Redux
#+AUTHOR:    Joe Corneli, Raymond Puzio
#+EMAIL:     contact@planetmath.org
#+DATE:      April 15, 2017 for Friday, 26 May, 2017 deadline
#+DESCRIPTION: Organizer for presentation on arxana and math text analysis at Oxford.
#+KEYWORDS: arxana, hypertext, inference anchoring
#+LANGUAGE: en
#+OPTIONS: H:3 num:t toc:t \n:nil @:t ::t |:t ^:nil -:t f:t *:t <:t
#+OPTIONS: TeX:t LaTeX:nil skip:nil d:nil todo:t pri:nil tags:not-in-toc
#+INFOJS_OPT: view:nil toc:nil ltoc:t mouse:underline buttons:0 path:http://orgmode.org/org-info.js
#+EXPORT_SELECT_TAGS: export
#+EXPORT_EXCLUDE_TAGS: noexport
#+LINK_UP:
#+LINK_HOME:
#+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://metameso.org/~joe/solarized-css/build/solarized-light.css" />
#+BIBLIOGRAPHY: arxana-redux-refs plain
#+LATEX_HEADER: \usepackage[backend=bibtex,sorting=none]{biblatex}
#+LATEX_HEADER: \addbibresource{arxana-redux-refs}
#+STARTUP: showeverything

* Overview (Introduction)

For the Scheme 2017 workshop at the International Conference on
Functional Programming (/ICFP/) to take place at Oxford this Autumn,
we will be making a presentation on Arxana and math texts.
We plan to get some version of /Arxana/ working, then use it to mark
up some mathematical text along the lines of /IAT/ and then come up
with a demo which shows what such a /scholiumific representation/ is
good for.  We will draw on /CD/ theory to move /IAT/ style
representations into a computable form.

** Glossary of keywords

- ICFP :: the International Conference on Functional Programming is an
 annual academic conference in the field of computer science
 sponsored by the ACM SIGPLAN, the Association for Computing
 Machinery's Special Interest Group on programming languages.
 Previous publications in the conference series touch on
 things like /A functional programmer's guide to homotopy type theory/,
 /Program synthesis: opportunities for the next decade/,
 /Lem: reusable engineering of real-world semantics/ [Lem stands for "[[http://www.cl.cam.ac.uk/~pes20/lem/][Lightweight executable mathematics]]"],
 /Functional programming with structured graphs/,
 /Painless programming combining reduction and search: design principles for embedding decision procedures in high-level languages/,
 /Using camlp4 for presenting dynamic mathematics on the web: DynaMoW, an OCaml language extension for the run-time generation of mathematical contents and their presentation on the web/,
 /TeachScheme!: a checkpoint/,
 /A functional I/O system or, fun for freshman kids/ and
 /Commutative monads, diagrams and knots/
 (i.e., a selection of papers from the proceedings over
 the last 10 years that mention "mathematics" or
 something similar; hopefully at least a few of them
 are relevant).  We plan to submit to the
 [[http://www.schemeworkshop.org/][Scheme and Functional Programming]] workshop,
 though perhaps we might also want to have a look
 at the [[http://functional-art.org/2017/cfp.html][Functional Art, Music, Modelling and Design]]
 workshop in case it proves to be a better fit.

- IAT :: Inference Anchoring Theory was devised by Budzynska et
     al \cite{budzynska2014model} to model the logical structure
     of dialogical arguments.  This has since been adapted to
     model mathematical arguments \cite{corneli2017qand}.  The
     primary features of this adaptation are: (1) to introduce
     more explicit relationships between pieces of mathematical
     content; and (2) to advance a range of ``predicates'' that
     relate mathematical propositions.  These predicates
     describe inferential structure, judgements of validity or
     usefulness, and reasoning tactics.

- scholium :: A scholium is a word for a marginal annotation or
     scholarly, explanatory, remark. Corneli and Krowne proposed
     a "scholia-based document model" \cite{corneli2005scholia}
     for "commons-based peer production," that is, the kind of
     collaborative online knowledge-building that happens on
     sites like Wikipedia or in online forums
     \cite{benkler2002coase}, or in other digital libraries
     broadly construed \cite{krowne2003building}.  The proposal
     is that online text resources grow ``by attaching.''  One
     familiar class of examples is provided by revision control
     systems, e.g., Git, which builds a network history of
     changes to documents in a directed acyclic graph (DAG).

- Arxana :: Arxana is the name given to a series of prototype
     implementations of the scholium-based document model with
     an Emacs front-end.  Arxana is inspired in part by Ted
     Nelson's Xanadu™ project, which was the first effort to
     work with ``hypertext'' per se
     \cite{nelson1981literary}. We have been specifically
     interested in applications within mathematics, which has
     given Arxana a unique flavour.  In particular, we propose
     to use a scholium model to model the logic of proofs, not
     just to represent mathematical texts for reading.

- CD :: Conceptual Dependence was introduced as a tool for
     understanding natural language \cite{schank1972conceptual}. It
     is also used to represent knowledge about actions
     \cite{lytinen1992conceptual,sowa2008conceptual}.  The basis of
     the theory is a set of /primitives/ which describe basic types
     of actions such as "PTRANS — transfer of location" or "MBUILD
     — construction of a thought or new information". Each
     primitive comes with a set of /slots/ which accept objects of
     certain types. By filling in the slots of a primitive, one
     obtains the most elementary form of a /conceptual dependency
     graph/. By combining such basic graphs, one can build up more
     complicated CD graphs which describe actions in greater
     detail.

** Plan of the work

- Unlike a classical proof which consists of mathematical statements
  and deductions, informal mathematical language is more general, and
  the reasoning involved may be abductive, inductive, or heuristic.

- The presentation here will describe a strategy we have been
  developing for representing mathematical dialogues and other
  informal texts.

- A publication appearing in "Artificial Intelligence" this month
  describes the high-level features of informal mathematics, and
  helped inspire this project.

- Our latest efforts produce more detailed models mathematical
  arguments.

- A graphical formalism and a corresponding prototype implementation
  will be described.

- Applications include modelling collaborative proof dialogues and
  discursive Q&A, as well as more traditional proofs.

- In our planned next steps we plan to bring in explicit
  type-theoretic representations of mathematical objects within a
  service-oriented architecture.

** Statement of the research problem

The kinds of structures that are described by ``IAT+Content''
are still more or less graphs.  However, to work with
mathematics we need to be able to talk about /hypergraphs/.  For
example, if we say ``In September 1993, an error was found in
Wiles's proposed proof of Fermat's Last Theorem'' we would like
to point to the entire proposed proof as an object.  Similarly,
we would like to be able to draw a connection between this 1993
proposal with the corrected version published in 1995.

As we will see (*I should think! -JC*), even a proof itself is
more conveniently represented by hypergraph structures.  In
particular, some of the ``predicates'' are really generative
functions.  Indeed, some of them are ``heuristics'' which take
some work to specify.

Another feature of our representation is that hypergraphs can be
placed inside nodes and links of other hypergraphs.  This allows
one to organize ther representation by levels of generality.  For
instance, at the highest level, there might be the structure of
statements and proofs of theorems.  At thje next level, there
would be the individual propositions and the argument structure.
At the lowest level, there would be the grammatical structure of
the propositions.  Having a way of ``coarse-graining'' the
representation is important in order to have it be managable and
allow users to zoom in and out of the map to find the appropriate
level of detail.   This is related to Fare's categorical theory
of levels of a computer system [add citation].

One effect of this is that the markup we are devising is
``progressive'' in the sense that we can describe heuristics with
nodes without fully formalising them.  A corresponding user feature is
to be able to fold things at many levels.  This is important because
the diagrams get quite large.

*** Proofs and prologues

In several of our examples, such as the Gowers problem and Artin's
book, on sees a structure in which a proof or calculation is preceded
by a kind of prologue in which the author describes motivation and
strategy.  Unlike the proof proper which consists of mathematical
statements and deductions, the language here is more general and
the reasoning may be abductive, inductive, or heuristic.

We would like to have a representation for these sorts of prologues
and indicate how they connect with the proof which they introduce
as well as the rest of the text.  A challenge here is that the
texts in question can allude and refer to all sorts of referents
including themselves at a high level of abstraction and require
a certain amount of common sense to be understood.

Since the issues that arise here are similar to those which arise in
undestanding and representing natural language stories, we should be
able to adapt techniques such as conceptual dependency relation or
goals and themes to a mathematical context.

*** Registers of mathematical discourse

The natural language which occurs in mathematical texts comes in
several different types.  Since these types differ in their
vocabulary, manner of reasoning, subject matter, and degree of
literality, it simplifies the study of the subject to distinguish
these types and examine them individually.

**** The formal register
One type of mathematical language is what we may call the
/formal register/.  This is the type of language which is used to state
mathematical propositions.  For example, "Every natural number can be
expressed as the sum of four squares." or "In every triangle, the sum
of the angles equals two right angles."  In this register, vocabulary
is interpreted in a certain technical fashion and the reasoning is
purely deductive.  Semantically, such statements are assumed to be
equivalent to symbolic expressions in formal logic (in whatever formal
system one is working).  For the examples, the following would be
formal equivalents:
\begin{align*}
  &(\forall n \in \mathbb{N}) (\exists a, b, c, d \in \mathbb{N})
     n = a^2 + b^2 + c^2 + d^2 \\
  &(\forall \Delta abc \in \mathrm{triangle})
     \angle abc + \angle bca + \angle cab = 2 * \perp
\end{align*}
Indeed, in mathematical writing, such statements in natural language
and their formal equivalents both appear and may even be combined
within a single sentence, such as "Whenever $(x, y)$ lies inside the
region, we have $x^2 + y^4 < 12$."

This register of discourse has been studied by de Bruijn, Ranta, Mohan
and others and there exist parsers which can translate between natural
language and formal expressions.  Once we have formal representations,
we can reason about them using tools from Frege and others.

While there is much work to be done towards developing a formal linguistic
theory of mathematics, at least some basic principles are understood and have
been illustrated with example programs so, for the purpose of this project,
we shall take this subject as given and allow ourselves to introduce
formal restatements of propositions without worrying about how the
translation might be accomplished.

**** The expository register
Another type of mathematical language is what we will call the
/expository register/.  This is the sublanguage which is used to
express how and why one is interested in a particular formal statement
and describe mathematical reasoning.  Examples of such language
include:

+ It is easy to see that our theory is complete if we assume the
  descending chain condition.

+ A more elegant way of proving theorem 5 is by induction on the
  degree; however, we chose to present the current proof because it
  makes it clear that the result depends upon the factorizibility
  condition.

+ Is it possible to prove that any point and any line will do?

+ Can we do this for $x+yx+y$? For $e$? Rationals with small denominator?

The expository register has several salient features which work together:

# Expanded a bit more in http://metameso.org/cgi-bin/current.pl/Two_years_later
# terms - put examples

- Mathematical content (Universe of discourse) :: The main focus of this type of discusses are mathematical objects and mathematical propositions (which may exist in analogy with physical objects or psychological states).  These are used to convey *narratives* of how one or more actors navigate their way through mathematical hyperreality.  Formal mathematics models the objects in this universe of discourse and their relationships, but the discourse itself is not necessarily formal.

- Metamathematical reasoning :: It is metamathematical, discussing not only with objects and propositions, but also inference and proofs.  For instance, in the first example *"It is easy to see that our theory is complete if we assume the
  descending chain condition"* says something about the proof of a statement.  Likewise, it indicates types of proofs and proof strategies.  It is however,
not a purely formal statement.  It relies on the next feature:

- Heuristic value judgements :: Whereas the formal register only has deductive reasoning of the strictest sort, in the expository register we also have *inductive* and *abductive* reasoning as well as reasoning by analogy, heuristics, and looser forms of approximate and plausible reasoning.  Concomittantly, the truth judgements made go beyond the truth values of formal logic to vaguer assertions such as "this proof is elegant" or "this statement sounds likely to be false".  This is closer to what one has in non-mathetical discourse.  These sorts of assertions influence the choice of actions and strategies.

*** Related fields

In order to build a computational theory of the expository register,
we will draw upon several well-studied topics in AI which deal with
situations that have common features, namely the block world, board
games, and story comprehension.

| /Level/               | *Block World*     | *Board Games*         | *Story Comprehension* |
|-----------------------+-------------------+-----------------------+-----------------------|
| universe of discourse | blocks on a table | game pieces on board  | everyday life         |
| reasoning             | instructions      | rules & strategy      | analogy               |
| value                 | consistency?      | prediction of winning | costs and benefits    |
| role of disagreement  | none              | multiple strategies   | ethical dilemmas      |

In a mathematical setting, thespects are modelled in "IATC" or
"Inference Anchoring Theory + Content" \cite{martin2017bootstrapping,corneli2017towards}.

In a Lakatos setting disagreement is the primary engine that drives discovery.

** Suitability of venue

As we will also see, it is not just incidental that our work is
implemented in LISP.  Actually, the kind of hypergraph programs
we use are a ``natural'' extension of the basic LISP data model.

Emacs (and Org mode) are suitable for interacting with other
programming languages and long-running processes, e.g., MAXIMA.
(Also see preiterature on heuristics in LISP from Lenat.)

*** What is on offer in this approach

Kinematics vs dynamics.

Purely formal logic written as graph subsitution - example.

One thing we have here is links that contain code.

Another thing hypergraphs give us is links to links - of course
we can also think about higher-dimensional versions of the same,
but links to link.

* The core language

Here we'll describe the structures coming from several different
places, e.g., Gabi, Lakatos, etc.

** Content (=structure=)                                               :GRAY:
*** object $O$ is =used_in= proposition $P$
**** Example: ``The Caley graph of group \(G\)'' has sub-object $G$
*** proposition $Q$ is a =sub-proposition= of proposition $P$
**** Example: ``$P$ is difficult to prove'' has sub-proposition $P$
*** proposition $R$ is a =reformed= version of proposition $P$
**** Example: ``Every $x$ is a \(P\)'' might be reformed to ``Some $x$ is a \(P\)''
*** property $p$ is as the =extensional_set= of all objects with property $p$
**** Example: the set $\mathcal{P}$ of primes is the extension of the predicate $\mathit{prime}$.
*** $O$ =instantiates= some class $C$
**** Comment: This is not quite syntactic sugar for =has_property=!
If we have a class of items $C$ we want to be able say that $x$ is a
member of $C$.  In principle, we could write $x$ =has_property= $C$.
But I think there are cases where we would want to
distinguish between, e.g.,
$2$ =has_property= prime, and $prime(2)$ =instantiates=
$prime(x)$.  This =instantiates= operation is a natural extension of
backquote; so e.g., we could write the true statement
$prime(4)$ =instantiates= $prime(x)$, even though $prime(4)$ is false.
**** Comment: Perhaps we need a further distinction between objects and 'schemas'
So we might write =has_property(member_of(x,primes))= to talk about
class membership.  Presumably (except in Russell paradox situations)
this is the same as =has_property(x,prime)=, or whatever.
*** $s$ =expands= $y$
**** Comment: This is something that a computer algebra system like MAXIMA could confirm
*** $s$ =sums= $y$
**** Comment: This is something that a computer algebra system like MAXIMA could confirm
*** $s$ =contains as summand= $t$
**** Comment: This is more specific than the =used in= relation
This relation is interesting, for example, in the case of sums like
$s+t$ where $t$ is, or might be, ``small''.  Note that there
would be similar ways to talk about any algebraic or
syntactic relation (e.g., multiplicand or integrand or whatever).
In my opinion this is better than having one general-purpose 'structural'
relation that loses the distinction between all of these.  However,
generalising in this way does open a can of worms for addressing.
I.e. do we need XPATH or something like that for indexing into
something deeply nested?
*** $M$ =generalises= $m$
**** Comment: Here, content relationships between methods.
Does this work?  Instead of talking about content relationships 'at
the content level' we are now interested in assertions like
"binomial theorem" =generalises= "eliminate cross terms",
where both of the quoted concepts are heuristics, not 'predicates'
*** Proposition vs Object vs Binder vs Inference rule?
Note that there are different kinds of `content'.  If for example I
say `\(0<a<b<1 \Rightarrow a^N < b^N\)', then this is more than just a
proposition, but something that can be used as a ``binder''; i.e., if
I fill in specific values of $a$ and $b$ (and, optionally, $N$) I know
the property holds for them.  At the same time, this sort of "binder"
is presumably also a *theorem* that has been proved.  This is,
additionally, similar to an *inference rule* since it allows us to move
from one statement to another, schematically (see discussion above
about "instantiates").  Anyway, this isn't yet about another kind of
structural relation, but it does suggest that we should be a bit
careful about how we think about content.
** inferential structure (=rel=)                                       :PINK:
*** =stronger= (s,t)
*** =not= (s)
*** =conjunction= (s,t)
*** =has_property= (o,p)
**** Comment: It seems useful in some case to be able to say that a 'method' or heuristic has a property
E.g. =has_property(strategyx, HAL)=
**** Comment: has_property should probably 'emit' the property as a side-effect
This way we can more easily see which is the object and which is the property.
It seems that thing that has a property may also be a 'proposition',
or, at least, a bit of 'object code' (like: "compute XYZ").
Furthermore, at least in this case, the 'property' might be a heuristic
or method (like "we actually know how to compute this").
*** =instance_of= (o,m)
*** =independent_of= (o,d)
*** =case_split= (s, {si}.i)
*** =wlog= (s,t)
** reasoning tactics; ``meta''/guiding (=meta=)                        :BLUE:
*** =goal= (s)
*** =strategy= (s,m)
**** Note: use method $m$ to prove $s$
**** Comment: perhaps this should be =strategy= (m [, s ]) so that s is optional
This is because, just for graphical simplicity, we might assume that
the statement that we want to prove is known in advance (e.g., it is
the statement of the problem).

This is the style at the beginning of gowers-example.pdf
**** Comment: how to show that a suggestion 'has been implemented'?
We might need some other form of 'certificate' for that.
E.g., it would say =implements(BLOB OF CODE,strategyx)=.
*** =auxiliary= (s,a)
*** =analogy= (s,t)
**** Comment: analogies between statements are different from auxiliaries to prove
Introducing some set of 'analogies' in a way sets us up for
'inductive' reasoning across a class of examples.  What do they all
have in common?  Which one is the most suitable?  Etc.
** heuristics and value judgements (=value=)                          :GREEN:
*** =easy= (s,t)
*** =plausible= (s)
*** =beautiful= (s)
*** =useful= (s)
*** =heuristic= (x)
**** Comment: It seems that we will have several layers of 'guidance'
Many of them will be neither value judgements nor metamathematical tags
like =strategy=, =goal=, or =auxiliary=.  Rather, the heuristics may be
used at an even higher level to produce or to implement these.  So,
for example, the heuristic might be what a =strategy= concretely
suggests.  It's also true that a given =auxiliary= might need a
heuristic "header", that explains /why/ this auxiliary problem has
been suggested.  Similar to a =strategy= the heuristic might look
for something that 'satisfies' or 'implements' the heuristics.
In some cases we've looked at, this 'satisficing' object will appear
directly as the argument of the heuristic, hence =heuristic(x)=.
For example: =specialise(THE PROBLEM, (sqrt(2)+sqrt(3))^2)=.
Incidentally, this particular example is only meaningful in connection
with *another* heuristic that has told us how to *generalise* the
problem, i.e., that has turned a static expression into something
with a variable in it.
** Performatives (=perf=)                                            :YELLOW:
*** =Agree= (s [, a ])
**** Note: optional argument $a$ is a justification for $s$
*** =Assert= (s [, a ])
**** Note: optional argument $a$ is support for $s$
**** Comment: It seems like we might want to be able to assert a 'graph structure'
Here is an example from early in gowers-example.pdf
#+BEGIN_SRC c
Assert(exists(strategy(PROBLEM, strategyx))
       AND has_property(strategyx,HAL))
#+END_SRC
*** =Challenge= (s [, c ])
**** Note: $c$ is a counter-argument or counter-example to $s$
*** =Define= (o,p)
**** Note: object with name $o$ satisfies property $p$
*** =Judge= (s)
**** Note: takes a =value= argument
*** =Query= (s)
*** =QueryE= ({pi(X)}.i)
**** Note: Asks for the class of objects  for which all of the properties pi hold
*** =Retract= (s [, a ])
**** Note: can only be made by someone who asserted $s$; $a$ is an optional reason
*** =Suggest= (s)
**** Note: Takes a =meta= argument

* Extensions to the core

** IAT + CD

By itself, IAT is useful for describing *what* takes place in a
mathematical discourse, but not so useful for figuring out *why*
and *how* (viz., kinematics and dynamics).  To address these issues,
we will augment it with the framework of /conceptual dependency theory/ (CD),
which has been used for such purposes in the context of machine understanding of stories
\cite{leon2011computational}.

# also a chapter in the AI Handbook.

The main ingredient of CD is a set of *primitives* which describe
types of actions.  Ususally, these consist of various physical and
mental operations but, for the purpose at hand, we will take them to
be the *performatives* of IAT.

We will have two classes of objects: the participants in the dialogue
and mathematical propositions.  

*** TODO We should figure out what the inferences between basic assertions (I/R, I/E, etc.) would look like here. (e.g. fig. 7 of Lytinen)

- links between basic CD's
 - e.g., joe communicated the IP address to ray, by talking, so that ray could get on the server

** Goals

In order to figure out why and how actions take place, CD theory
introduces procedural knowledge in the form of scripts, MOPs, TOPs,
goals, and plans.  For our purposes, goals and plans will be used.

This relates to the meta items of the spec.  Maybe we should expand
the goal item using some sort of ontology like that of Schank and
Ableson.

** Parsing

A simple example from \cite{lytinen1992conceptual} schematizes the
sentence "John gave Mary a book" as an s-expression.

#+BEGIN_SRC lisp
(atrans actor  (person name john)
        object (phys-obj type book)
        recip  (person name mary))
#+END_SRC

** Possible "warm up" example

"Adjoints exist and are unique." - See Halmos.

#+BEGIN_SRC lisp
(defn adjoint-of-a-bounded-linear-operator-on-a-hilbert-space
  (X Y A Astar)
  (hilbert-space X)
  (hilbert-space Y)
  (bounded-linear-operator A X Y)
  (and (map Astar Y X)
       (forall x :in X :st
               (forall y :in Y :st
                       (eq (inner-product :on Y :of (A x) y)
                           (inner-product :on X :of x (Astar y)))))))

(defproof
  adjoint-of-a-bounded-linear-operator-on-a-hilbert-space:fact:
  adjoints-exist-and-are-unique (A X Y)
  (hilbert-space X)
  (hilbert-space Y)
  (bounded-linear-operator A X Y)
  (bind phi (map phi X Y :takes x
                 :to (inner-product :on Y :of (A x) y)))
  ;; We need to show that phi is linear, but that’s ‘easy’
  (shows (linear phi)
         (linear A)
         (properties-of-inner-product))
  ;; The lemma allows us to spawn a reasonable target
  (obtain v :st
          (unique v :in X :st
                  (forall u :in X :st (eq (varphi u)
                                          (inner-product :in X :of u v))))
          (uniquely-represent-a-linear-functional-by-an-inner-product
           X phi))
  (bind Astar (map Astar Y X :takes w :to v))
  ;; Finally, assert that the Astar so constructed is the adjoint
  (assert (adjoint-of-a-bounded-linear-operator-on-a-hilbert-space X Y
                                                                   A Astar)))
#+END_SRC

* Task tree

** Infrastructure

This file is in versioned storage in the "mob" branch of our arxana
repo; instructions to access are here:
http://repo.or.cz/w/arxana.git/blob_plain/d187e244a8eb7d2208f1fe98db1ef895c6cd4a36:/README.mob

A working copy of this repository is checked out at
=/home/shared-folder/arxana-redux/arxana/= on the Linode.

And a "scratch" copy of the file has been copied to:
=/home/shared-folder/arxana-redux/arxana-redux.org=

This can be edited in live sessions using =togetherly.el=.

** Progress on paper

*** Corpus/Examples: Hand-drawn diagrams in IAT+C

/We are allowed to submit an appendix without a size limit, so if we don't have room for all of the diagrams in the paper, we could put them in the appendix./

- Minipolymath, treated by Gabi in the Transactions on Social Computing paper, pdf available from https://www.overleaf.com/read/jyhzpqsythzq
- Our randomly selected MathOverflow discussion (from Q&A article)
- Gowers 2012 trick problem, http://metameso.org/ar/gowers-example.pdf
- Also there's Schuam's Abstract Algebra exercise 337, a diagram is shown on arxana.net.
 - Redone using IATC: http://metameso.org/ar/schuams-example.pdf
- An example from the Ganesalingam and Gowers paper: http://metameso.org/ar/robotone-example.pdf
- Galois theory. Emil Artin's book.
- Euclid algorithm
- possibly an example from metamath or coq or whatever to show that we can model that stuff as discourse...
- ...

*** Other Background

**** Items we've worked on before

Over the years as we've worked on Arxana, we have generated all sorts
of files.  Here are descriptions and locations of some of them which
are relevant to the current project.

Many of these are stored in =/home/shared-folder/public_html/=, and
accessible on the web at [[http://metameso.org/ar/]].

***** Research notes

- "nemas" document:  http://metameso.org/ar/metamathematics.pdf
- Joe's thesis Appendix B: http://metameso.org/ar/thesis-appendix-b.pdf
- Metamathematics preprint: http://metameso.org/ar/mathematical-semantics.pdf
- hcode function spec: http://metameso.org/ar/hcode.pdf
- Lakatos game spec: http://metameso.org/ar/lakatos-flowchart.pdf

***** Wiki

- [[http://metameso.org/cgi-bin/current.pl?action=browse;oldid=Arxana;id=A_scholium-based_document_model][A scholium-based document model]] is the wiki homepage for Arxana and has several relevant discussions.
- [[http://metameso.org/cgi-bin/current.pl/Two_years_later][Two years later]] collects many of the mathematical themes in
  overview
- [[http://metameso.org/cgi-bin/current.pl/samples_of_formal_mathematical_writing][samples of formal mathematical writing]] is a small collection
  of statements in mathematical language (leaving out ``the part
  in between dollar signs'')

***** Website

- [[http://arxana.net][arxana.net]] has links to source code from various prototypes
 - It also has a small gallery of hand-drawn diagrams

**** And other things elsewhere:

- /Handbook of artificial intelligence/ by Barr and Feigenbaum describes *SAM* and *PAM*, the /Script Applier Mechanism/ and /Plan Applier Mechanism/ by Schank and Abelson et al., on page 306 et seq. \cite{barr1981handbook}
- Winograd, Natural language and stories --- MIT AI Technical Report 235, February 1971 with the title "Procedures as a Representation for Data in a Computer Program for Understanding Natural Language" ([[http://hci.stanford.edu/winograd/shrdlu/AITR-235.pdf][link]])
 - Could we reuse this stuff for the "narrative"
 - How do we know how to read the text and transform it into IATC?
 - An example is Gowers's "total stuckness": how do we turn that into code?
- Conceptual dependency representation - from "Deep Blue" website ([[https://deepblue.lib.umich.edu/bitstream/handle/2027.42/30278/0000679.pdf?sequence=1][link]]).
 - Schank's MARGIE system is described on page 300 /et seq./ of \cite{barr1981handbook}.
- AI textbook in wiki.

*** TODO Initial non-working pseudocode prototype

Here it makes sense to at least try and transcribe the main examples
in some "pseudocode", inspired by IATC and hcode, which we can then
refine into a working version later.

Several examples have been transcribed:

- http://metameso.org/ar/mpm3.html
- http://metameso.org/ar/gowers2012.html
- http://metameso.org/ar/robotone-opensets.html

However, as per the headline, these don't currently *do* anything.

*** TODO Basic working version

*** TODO Can the system come up with answers to new, basic, questions?

- Inspired by Nuamah et al's geography examples
- Simple comparisons, like, how does this concept relate to that concept?  We informally talk about this as ``analogy'' between concepts.  But...

*** TODO Foldable views (like in Org mode) so that people can browse proofs

- This may come after the May submission
- Folding and unfolding the definitions of terms in something like an APM context is relevant example.  Just `unpacking' terms.

* Related work

** In a mathematics context

- ``Lakatos-style Collaborative Mathematics through Dialectical,
  Structured and Abstract Argumentation'' shows how it is possible to
  ``formalize'' the informal logic proposed by Lakatos
  \cite{pease2017lakatos}.
- [[http://www.emis.de/monographs/Trzeciak/biglist.html][Mathematical English Usage - a Dictionary]] (Jerzy Trzeciak)
- [[https://case.edu/artsci/math/wells/pub/html/abouthbk.html][The Handbook of Mathematical Discourse]] (Charles Wells)
- [[http://universaar.uni-saarland.de/monographien/volltexte/2015/111/pdf/wolska_mathematicalProofs_komplett_e.pdf][Students'language in computer-assisted tutoring of mathematical proofs]] (Magdalena A. Wolska)

** Does what we're doing relate in any way to other formal proof checkers?

- Default answer: no, because people have build large repositories of formal math (Mizar, Coq, metamath, etc.).  These other projects don't make a serious effort to deal with mathematical text.  TeX is in one place, and logic is in another place.

 - There's another paper by Josef Urban et al. that is the exception that proves the rule \cite{kaliszyk2014developing} (see also the poster that accompanied this paper \cite{kaliszyk2014developing-misc})

- There's also a generative program by Ganesalingam and Gowers thath meshes natural language and formal mathematical reasoning.

- With these examples in mind, we assert that what we are doing can be combined with proof checkers synergistically.  For instance, one could attach scholia to the statements in an IAT representation which contain formalized representations of the content, and scholia which indicate that certain statements have been