save progress

[arxana.git] / org / farm-talk.org

#+TITLE:     \large{Modelling the Way Mathematics Is Actually Done}
#+AUTHOR:    Joseph Corneli, Ursula Martin, Dave Murray-Rust,\newline Alison Pease, Raymond Puzio, Gabriela Rino Nesin
#+EMAIL:     contact@planetmath.org
#+DATE:      9 September, 2017
#+DESCRIPTION: Organizer for presentation on arxana and math text analysis at Oxford.
#+KEYWORDS: arxana, hypertext, inference anchoring
#+LANGUAGE: en
#+OPTIONS: H:1 num:t toc:nil \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
#+LATEX_CLASS: beamer
#+LATEX_CLASS_OPTIONS: [presentation,serif]
#+LATEX_HEADER: \usepackage{beamerhacks}
#+LINK_UP:
#+LINK_HOME:
#+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://metameso.org/~joe/solarized-css/build/solarized-light.css" />
#+STARTUP: showeverything

# convert example-graph.png -fuzz 1% -fill 'rgb(255,255,230)' -opaque white fond-graph.png

* "From cons cells to triples, from trees to hypergraphs"

/cons cell/ =(a . b)=, =car=, =cdr= \SoThat /nema/ =(a c b)=, =src=, =txt=, and =snk=.\newline
A repository of nemas is a /plexus/.  =(0 a 0)= is used to represent =a=.

/Mom resents the fact that John disapproves of Jane and Jim's
marriage./

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 8cm
    [[file:./fond-mom.png]]

\textbf{History}: *Arxana*: "A Scholia-based Document Model for Commons-based Peer Production", 2005;  various backends since then. *Inference Anchoring Theory + Content*, 2016-2017

* The problem:
 - Whereas formal mathematical theories are well studied, computers cannot yet adequately represent and reason about mathematical dialogues and other informal texts.
- Machine learning is likely to be useful for building mathematical AI.
- But for that we need representations of mathematics in which meaningful patterns can be found.
* Background
\textbf{Formal register}:
\begin{eqnarray*}
&& \hspace{-1cm}\text{\emph{``Every integer equals the sum of four squares.''}}\\
&\equiv& (\forall n \in \mathbb{N}) (\exists m_1,m_2,m_3,m_4 \in \mathbb{N}) \, n = \sum_{i=1}^{4} m_i^2
\end{eqnarray*}
- Nothing essential is lost in translating between the verbal and symbolic statements ("no reference is made ... to meaning").
- /Trees/ provide the look and feel of the formal register.

\textbf{Expository register}:
\begin{quote}
"Next, we will prove the four-square theorem using an algebraic identity similar to the one we just used to prove the two squares theorem."
\end{quote}
* Framing the Current Effort

The blocks world, board games, and story comprehension require increasingly sophisticated patterns of \emph{inference}, \emph{thinking}, and \emph{reasoning}.

\medskip

\begingroup\scriptsize
\begin{myenv}[1\textwidth]{3em}
\begin{tabular}{llll}
\emph{Level} & \textbf{Blocks World} & \textbf{Board Games} & \textbf{Story Comprehension}\\
\hline
elements & blocks on a table & game pieces on board & episodes from everyday life\\
inference & follow instructions & rules \& strategy & analogy\\
thinking & consistency & prediction of winning & costs and benefits\\
reasoning & (trivial) & multiple strategies & ethical dilemmas\\
\end{tabular}
\end{myenv}
\endgroup

\hspace{2.78in} \textcolor{brightpink}{$\uparrow$}

Understood as a computational challenge, mainstream mathematics lies
somewhere in between board games and story comprehension.

* Survey of Related Work

\textbf{Annotative programming}: \emph{Flare}, \emph{ZigZag}, \emph{AtomSpace}

\bigskip

\textbf{Models of Mathematical Reasoning}:

# http://www.fileformat.info/info/unicode/font/dejavu_sans_oblique/blockview.htm?block=emoticons
1. Inference Anchoring Theory + Content \deja{☺}
1. Conceptual Dependence \deja{☺}
1. Structured Proofs \deja{😐}
1. Lakatos Games \deja{😼}

* Inference Anchoring Theory + Content

This is what we use to model *what* people say when they talk about
mathematics.

\vspace{-.5cm}

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 11cm
    [[file:./fond-analogies.png]]

* Inference Anchoring Theory + Content (ctd.)

\textbf{Performatives}

\begingroup\scriptsize
\begin{tabular}{p{.3\columnwidth}@{\hspace{-.25ex}}p{.7\columnwidth}}
\texttt{Assert} (\emph{s} [, \emph{a} ]) & Assert belief that statement \emph{s} is true, optionally because of \emph{a}.\\
\texttt{Agree} (\emph{s} [, \emph{a} ]) & Agree with a previous statement \emph{s}, optionally because of \emph{a}.\\
\texttt{Challenge} (\emph{s} [, \emph{a} ]) & Assert belief that statement \emph{s} is false, optionally because of \emph{a}.\\
\texttt{Retract} (\emph{s} [, \emph{a} ]) & Retract a previous statement \emph{s}, optionally because of \emph{a}.\\
\texttt{Define} (\emph{o}, \emph{p}) & Define object \emph{o} via property \emph{p}.\\
\texttt{Suggest} (\emph{s}) & Suggest a strategy \emph{s}.\\
\texttt{Judge} (\emph{s}) & Apply a heuristic value judgement \emph{s} to some statement.\\
\texttt{Query} (\emph{s}) & Ask for the truth value of statement \emph{s}.\\
\texttt{QueryE} (\{$p_i$($X$)\} . \emph{i}) & Ask for the class of objects \emph{X} for which all of the properties $p_i$ hold.
\end{tabular}
\endgroup

* Inference Anchoring Theory + Content (ctd.)

\textbf{Inferential Structure}

\begingroup\scriptsize
\begin{tabular}{p{.3\columnwidth}@{\hspace{-.25ex}}p{.7\columnwidth}}
% Gabi's notes used ``stronger'' but ``implies'' is more intuitive
\texttt{implies} (\emph{s}, \emph{t}) & Statement \emph{s} implies statement \emph{t}.\\
\texttt{not} (\emph{s}) & Negation of \emph{s}.\\
\texttt{conjunction} (\emph{s}, \emph{t}, \ldots) & Conjunction of statements \emph{s}, \emph{t}, \ldots \\
\texttt{has\_property} (\emph{o}, \emph{p}) & Object \emph{o} has property \emph{p}.\\
\texttt{instance\_of} (\emph{o}, \emph{m}) & Object \emph{o} is an instance of the broader class \emph{m}.\\
\texttt{indep\_of} (\emph{o}, \emph{d}) & Object \emph{o} does not depend on the choice of object \emph{d}.\\
\texttt{case\_split} (\emph{s}, \{$s_i$\} . \emph{i}) & Statement \emph{s} is equivalent to the conjunction of the $s_i$'s.\\
\texttt{wlog} (\emph{s}, \emph{t}) & Statement \emph{t} is equivalent to statement \emph{s} but easier to prove.\\
\end{tabular}
\endgroup

\textbf{Reasoning tactics}

\begingroup\scriptsize
\begin{tabular}{p{.3\columnwidth}@{\hspace{-.25ex}}p{.7\columnwidth}}
\texttt{goal} (\emph{s}) & Used with \texttt{Suggest} to guide other agents to work on \emph{s}.\\
\texttt{strategy} (\emph{m}, \emph{s}) & Method \emph{m} may be used to prove \emph{s}.\\
\texttt{auxiliary} (\emph{s}, \emph{a}) & Statement \emph{s} requires an auxiliary lemma \emph{a}.\\
\texttt{analogy} (\emph{s}, \emph{t}) & Statement \emph{s} and statement \emph{t} should be seen as analogous in some way.\\
\texttt{implements} (\emph{s}, \emph{m}) & Statement \emph{s} implements the method \emph{m} from a previousl suggested strategy.\\
\texttt{generalises} (\emph{m}, \emph{n}) & Method \emph{m} generalises method \emph{n}.  \\
\end{tabular}
\endgroup

* Inference Anchoring Theory + Content (ctd.)

\textbf{Heuristics and Value Judgements}

\begingroup\scriptsize
\begin{tabular}{p{.3\columnwidth}@{\hspace{-.25ex}}p{.7\columnwidth}}
\texttt{easy} (\emph{s} [, \emph{t}]) & Statement \emph{s} is easy to prove; opt., easier than statement \emph{t}.\\
\texttt{plausible} (\emph{s}) & Statement \emph{s} is plausible.\\
\texttt{beautiful} (\emph{s}) & Statement \emph{s} is beautiful (or mathematically elegant).\\
\texttt{useful} (\emph{s}) & Statement \emph{s} can be used in an eventual proof.\\
\texttt{heuristic} (\emph{x}) & Statement \emph{x} describes an heuristic (with less rigour than a strategy).\\
\end{tabular}
\endgroup

\textbf{Content-Focused Structural Relations}

\begingroup\scriptsize
\begin{tabular}{p{.3\columnwidth}@{\hspace{-.25ex}}p{.7\columnwidth}}
\texttt{used\_in} (\emph{o}, \emph{s}) & Object \emph{o} is used in statement \emph{s}.\\
\texttt{sub\_prop} (\emph{s}, \emph{t}) & Statement \emph{s} contains proposition \emph{t}.\\
\texttt{reform} (\emph{s}, \emph{t}) & Statement \emph{s} can be reformed into statement \emph{t}.\\
\texttt{extensional\_set} (\emph{p}) & The set of objects with property \emph{p}.\\
\texttt{instantiates} (\emph{s}, \emph{t}) & Statement \emph{s} schematically instantiates statement \emph{t}. \\
\texttt{expands} (\emph{x}, \emph{y}) & Expression \emph{x} expands to expression \emph{y}.\\
\texttt{sums} (\emph{x}, \emph{y}) & Expression \emph{x} sums to expression \emph{y}. \\
\texttt{cont\_summand} (\emph{x}, \emph{y}) & Expression \emph{x} contains \emph{y} as a summand. \\
\end{tabular}
\endgroup

* Conceptual Dependence

CD was used by Schank, Lytinen, and others to represent knowledge
about actions, and to \emph{reason about stories}.

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 11cm
    [[file:./fond-cd-example.png]]

Something like CD should be capable of reasoning about *why* people
say what they do when they talk about mathematics.

* Structured Proofs

This is a semi-formal style of writing down proofs that is not
all that well suited to describing \emph{informal} reasoning.

\vspace{-.5cm}

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 11cm
    [[file:./fond-structured.png]]

...

* Lakatos Games

This is a \emph{formalised} description of informal reasoning, with a
constrained structure.  It's plausible, but not sufficient.

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 8cm
    [[file:./fond-lg.png]]

* The Search for the `Quantum of Progress'

Ganesalingam and Gowers's ROBOTONE:

\begin{quote}
can ... be regarded as repeatedly applying a single tactic, which is itself constructed by
taking a list of subsidiary tactics and applying the first
that can be applied.\footnote{M. Ganesalingam and W. T. Gowers. A Fully Automatic Theorem Prover with
Human-Style Output. \emph{Journal of Automated Reasoning}, pages 1–39, 2016.}
\end{quote}

*Its answers to the `why question' would not be very interesting.*

Cf. Sussman's HACKER,[fn:: Gerald J. Sussman, A Computational
Model of Skill Acquisition, PhD thesis, MIT, 1973.] which solved
problems in the block world: not in the most efficient way, but in an
interesting way.

* Example: A Diagrammatic Model of Mathematical Reasoning via IATC
* Towards Functional Models of Mathematical Reasoning
* Kinematics (IATC+CD)
* Dynamics
* Our Prototype, \emph{Arxana}
* System Overview
* Application to Mathematical Reasoning
* Future directions for development
* Conclusions and Future Work
* Partial Specification of IATC

* World's first combination of IATC and CD
- what we have now in Listing 2 will probably need to be considerably
  rethought
- Describe what we're trying to do, if you change one subgraph on one
  you get to the other
* Summary
*** \phantom{y}                                               :B_block:BMCOL:
    :PROPERTIES:
    :BEAMER_COL: 0.5
    :BEAMER_ENV: block
    :END:
Column 1
*** \phantom{x}                                               :B_block:BMCOL:
    :PROPERTIES:
    :BEAMER_COL: 0.5
    :BEAMER_ENV: block
    :END:
Column 2
* Future work
* The end
* outtakes                                                         :noexport:
** Other things we've worked on

#+C Local Variables:
#+C org-tree-slide-skip-outline-level: 3
#+C mode-line-format: nil
#+C org-latex-compiler: "xelatex"
#+C eval: (org-display-inline-images t t)
#+C eval: (setq org-tree-slide-header nil)
#+C End:

* Frame with references                                            :noexport:
  :PROPERTIES:
  :BEAMER_OPT: fragile,allowframebreaks,label=
  :END:
  \printbibliography