simplify iatc slides

[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 paper deadline
#+DESCRIPTION: Organizer for presentation on arxana and math text analysis at Oxford.
#+KEYWORDS: arxana, hypertext, inference anchoring
#+LANGUAGE: en
#+OPTIONS: H:4 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 and FARM 2017 workshops at the International Conference
on Functional Programming (/ICFP/) to take place at Oxford this
September, are making presentations about /Arxana/ and math texts.  We
plan to follow this up with submissions to relevant international
conferences next year, like /IJCAI/ or the main conference track at
ICFP.

For the demo at FARM, we want to have Arxana working, then use it to
mark up a mathematical text using /IATC/ + /CD/.  We hope to have a
demo ready that shows what this sort of /scholiumific representation/
is good for.

Together with our colleagues in Ursula Martin's fellowship
project on "The Social Machine of Mathematics" we have written
a 12 page paper for the FARM workshop that describes
these ideas in more detail.  It can be found here:
http://metameso.org/ar/farm-2017.pdf

Further information on the project and ongoing development, including
agenda items relevant to future papers, can be found below.

** Previous presentations

*** CIAO talk
This talk outlined the project and some related ideas, and described some of
the big picture in which this work fits; an outline of the
slides is here: [[file:~/arxana/org/ciao-talk.org][ciao-talk.org]]
*** Emacs NYC July 10th
This presentation walked through the concepts of Arxana
and showed code embedded in networks; abstract at
http://metameso.org/ar/
*** Big Proof talk same week
Some of Joe's biography and reasons for working on this project,
followed by the Q&A example presented at CICM and the Gowers 2012
example as in our FARM paper. Slides here:
http://metameso.org/~joe/docs/ini-big-proof.pdf

** 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.[fn:1] In 2017, we submitted a lightning talk for
          the [[http://www.schemeworkshop.org/][Scheme and Functional Programming]] workshop, and a full
          paper for the [[http://functional-art.org/2017/cfp.html][Functional Art, Music, Modelling and Design]]
          (FARM) workshop.

- IJCAI :: the *International Joint Conference on Artificial
           Intelligence* is one of the top international yearly
           conferences in AI.  The deadline for paper submissions is
           usually in January or February, and the conference is
           usually in July or August.  In [[http://www.chessprogress.com/IJCAI-2018/][IJCAI 2018]] will be held in
           Stockholm.

- 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.

- IATC :: 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; the adapted version is called
          *Inference Anchoring Theory + Content*
          \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).

- 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.

[fn:1] Previous publications in the ICFP conference series touch on things like this:
 /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/
 (... the foregoing list being 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).

* Outline of our ICFP workshop submissions

Our draft notes have been moved to a separate org mode file, see [[file:~/arxana/org/icfp-workshops.org::*Plan%20of%20our%20ICFP%20workshop%20contributions][Plan
of our ICFP workshop contributions]].

** FARM

The outline of sections in our final FARM submission is as follows:

- Introduction 
- Background
 - Framing the Current Effort
- Survey of Related Work 
 - Models of Mathematical Reasoning
  - Inference Anchoring Theory + Content
  - Conceptual Dependence
  - Structured Proofs
  - Lakatos Games
 - The Search for the 'Quantum of Progress'
- Example: A Diagrammatic Model of Mathematical Reasoning via IATC 
- Towards Functional Models of Mathematical Reasoning
 - Kinematics (IATC+CD)
 - Dynamics
- Our Prototype, /Arxana/
 - System Overview
 - Application to Mathematical Reasoning 
- Conclusions and Future Work
- Partial Specification of IATC 

** Scheme

For the Scheme workshop we only submitted an abstract, which is on
http://metameso.org/ar/

* Guide to files in our git repository <<short-docs>>

The items currently receiving the most attention are: [[arxana-redux]], [[arxana-merge]], and [[honey-spec]].

** org
*** arxana-redux.org <<arxana-redux>>
*This file -- a guide to our work in progress.*
*** honey-spec.org <<honey-spec>>
Gives a specification for the backend. Status: consensus draft, needs to be applied to code
in [[arxana-merge]].
*** robotone-opensets.org
Walk through a simple proof ROBOTONE proof from \cite{Ganesalingam2016} and mark it up in IATC.
*** mpm.org
Walk through parts of a MiniPolymath proof and mark it up in IATC.
*** scheme-2017.org
Our submitted abstract for Scheme 2017 lightning talk.
*** gowers2012.org
Walk through a simple proof from Gowers and mark it up in IATC.
*** ciao-talk.org
Slides on "Reasoning about mathematics with graphical programs" presented Tuesday 23 May, 2017 at "CIAO 25 AB 70" in Edinburgh.
*** farm-2017.org
Preliminary outline of our FARM 2017 submission.

** latex
*** arxana-reboot.tex <<arxana2010>>
This is the 2010-era version of Arxana.  Unlike its predecessor [[arxana2005]], this uses Common Lisp and
MySQL for storage, so the setup process is more complicated.  In principle some other external datastore could be used, i.e., a [[https://en.wikipedia.org/wiki/Graph_database][graph database]] like [[https://en.wikipedia.org/wiki/Neo4j][Neo4j]] or a hypergraph database like [[http://hypergraphdb.org/][HypergraphDB]] or [[https://github.com/opencog/atomspace][AtomSpace]],
the latter being especially quite close to what we're working on, since they make use of "Atoms" which are similar to our "nemas", and since they have Scheme bindings for their database operations.

*** arxana-merge.tex <<arxana-merge>>
This is the 2017 rewrite of Arxana.  It is derived from [[arxana2010]] and
[[honey]] -- specifically, honey provides a backend entirely inside Emacs,
so we can dispense with complicated connections to external programs.
Some additional features from [[arxana2005]] still need to be merged in.

*** honey-demo.tex
Exposition of the "Higher Order NEsted Yarnknotter" (HONEY) system.  Some of this text went into our paper for FARM 2017.
*** sbdm4cbpp.tex <<arxana2005>>
This is the 2005-era version of Arxana.  It runs entirely in Emacs, using a hash table for storage.
A version of the software was demoed in Atlanta at the Free Culture and the Digital Library Symposium, in connection with
\cite{corneli2005scholia}.  It was largely replaced by [[arxana2010]], though this version still has some features that the
later version lacked.
*** sch-prog.png
A figure to illustrate code embedded inside of networks; used in an early draft of the FARM paper.

** elisp
*** binom-demo.el
*** bootstart.el
*** clyde.el
*** honey.el <<honey>>
All of the code for low-layer HONEY functionality.
*** prelim.el
*** sch-prog-demo.el
*** sch-prog.el
*** simple-ui.el
*** search-expanded.el
This contains meso-layer search functionality built on top of HONEY.
*** tarot.el
Used for building arxana.net.  Could be expanded to produce adaptive text (e.g., narrative tarot readings); see \cite{veale2017dejavu} for an illustration of how.

** elsewhere

*** In our web directory

Many of these have been copied to =/home/shared-folder/public_html/=,
and accessible on the web via [[http://metameso.org/ar/]].

- "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

*** On the old AsteroidMeta 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'')

* Other relevant background

This file includes some references in BibTeX.  Some annotations on
specific items are here:

- *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.

* Infrastructure

The current 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 floobits.

*Note* Due to buggy behavior of togetherly, we've since decided to
switch to Floobits for live editing sessions, via:

=M-x floobits-join-workspace RET https://floobits.com/holtzermann17/arxana RET=

* Extensions to the core of IATC

** 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.

** 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
** Progress on preparing the work for public consumption

*** DONE Corpus/Examples: Hand-drawn diagrams in IATC

/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...
- ...

*** DONE Initial non-working "paper prototype" for FARM example(s)

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.


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

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

In our FARM paper we have analysed some of the Gowers paper in more
depth.

*** DONE Complete a short summary documentation

- The section [[short-docs]] here describes the files in our repository. (This needs to be maintained.)
- [[file:~/arxana/latex/honey-spec.org][honey-spec.org]] gives a specification for the backend. (This is nearly accurate but some revisions need to be carried out.)

*** DONE connect frontend for interaction and backend for storage
We have shown how this works with backend storage in-memory in Emacs,
noting that (/in principle/) storage could be in a database or something
else.  This flexibility is ensured by the clear separation of concerns
between different layers of the system.


** Future work
*** Immediate upcoming: Before September 3-9 ICFP conference, focusing on our demo
**** TODO Clean up namespaces of functions                      :maintenance:
E.g. write =honey:add-nema= instead of =add-nema=.
**** TODO find the generic interface layer and put it in its own file :maintenance:
Sketched in honey-spec.org, but let's make sure it's consistent.
**** TODO Assemble/disassemble a buffer from/to distributed storage :demoscheme:

While not needed for our FARM demo, this could be useful for the
Scheme demo because it makes a relatively convincing case.  And
furthermore this would be good as user facility and for us as we
continue working on the project.

- E.g., related work of arxana-merge merge automatically.

**** TODO Write a basic IATCD evaluator to load Listing 1 stuff        :demofarm:

/What is a better name for IATCD?/ ;-)

This is just at the level of moving data around - specifically turning
s-expressions into triples.

**** TODO Use scholium-based programs to run Listing 2                 :demofarm:

This is a minimal *working* implementation of what we talk about in the paper.

**** TODO How do inferential connections work (I/R, I/E, etc.)? :demofarm:

E.g. fig. 7 of Lytinen.

This is just for exposition, when talking about prior art it would be nice to know how they did it.

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

*** Next steps: Paper for IJCAI 2018
**** TODO IJCAI 2018: Write up applications to mathematics            :platform:
Possibly for IJCAI/ECAI.
Papers due *January 2018*? http://www.chessprogress.com/IJCAI-2018/calls/
To take place *July 13-19, 2018*
**** Demo the system walking through the steps of a proof like GCP or MPM.
**** Demo with APM prelim problems
This might be a "future work" section for this paper.
**** Demo with APM-Xi content
Show interface with types.
- E.g. APM-Xi style formulations of category theory definitons could be salient to work with.

*** Next steps: Paper for ICFP 2018
**** TODO ICFP 2018: Logic programming like Reasoned Schemer but for hypergraphs :platform:
Possibly submit to [[http://conf.researchr.org/home/icfp-2018][ICFP]]. Papers due *Fri 16 Mar 2018*.
Event to take place in St. Louis, Missouri, United States, to take place *late September*.
**** Fuzzy search to retrieve loose matches and analogies
**** Write a simple user language and an interface that generates triplets/quintuplets
**** 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...

**** 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.
- Note that there is some relevant prior work in the "Wikum" paper of Amy Zhang et al

*** Other next steps: from the Future Work section of our FARM paper

This could potentially be used as the basis of an ERC fellowship
proposal.  The "2018" version of the call was released August 3 2017,
and is due October 17 2017.  Presumably the "2019" version of the call
will be run on a similar timeline.  A long PDF describing the current
call is here: [[http://ec.europa.eu/research/participants/data/ref/h2020/other/guides_for_applicants/h2020-guide18-erc-stg-cog_en.pdf][h2020-guide18-erc-stg-cog_en.pdf]].

**** Formal proof
***** Demo the system walking through the steps of a proof like GCP or MPM.
If we keep at it, might have this ready by January, in time for an
IJCAI paper.
***** Refine both representations and reasoning aspects.
***** Integrate external computer algebra / proof checking systems.
**** Embodiment and cognitive science
***** Build on CD theory to reason about embodied intuitions in geometric problems, integrate with Lakoff and Núñez's conceptual metaphors \cite{kaliszyk2014developing-misc}.
**** Linguistics and NLP
***** Integrate parsers to generate IATC+CD automatically.
***** Use these models to seed statistical machine learning, e.g., expanding on the work of Kaliszyk et al who ascertained the frequency of various schematic usages like ``let \(X\) be a \(Y\)'' in a specific corpus of proofs.
**** Machine learning
***** Integrate with knowledge bases of mathematical terms and frequency data (as above).
***** Model Stack Exchange dialogues, in parallel with the work done  on Reddit discussions \cite{zhang2017characterizing}.
***** Build a system with multiple agents that ``converse with each other to sharpen their wits'' \cite{heretical-theory}.

* 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 

* 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