2 #+AUTHOR: Joe Corneli, Raymond Puzio
3 #+EMAIL: contact@planetmath.org
4 #+DATE: April 15, 2017 for Friday, 26 May, 2017 deadline
5 #+DESCRIPTION: Organizer for presentation on arxana and math text analysis at Oxford.
6 #+KEYWORDS: arxana, hypertext, inference anchoring
8 #+OPTIONS: H:3 num:t toc:t \n:nil @:t ::t |:t ^:nil -:t f:t *:t <:t
9 #+OPTIONS: TeX:t LaTeX:nil skip:nil d:nil todo:t pri:nil tags:not-in-toc
10 #+INFOJS_OPT: view:nil toc:nil ltoc:t mouse:underline buttons:0 path:http://orgmode.org/org-info.js
11 #+EXPORT_SELECT_TAGS: export
12 #+EXPORT_EXCLUDE_TAGS: noexport
15 #+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://metameso.org/~joe/solarized-css/build/solarized-light.css" />
16 #+BIBLIOGRAPHY: arxana-redux-refs plain
17 #+LATEX_HEADER: \usepackage[backend=bibtex,sorting=none]{biblatex}
18 #+LATEX_HEADER: \addbibresource{arxana-redux-refs}
19 #+STARTUP: showeverything
21 * Overview (Introduction)
23 For the Scheme 2017 workshop at the International Conference on
24 Functional Programming to take place at Oxford this Autumn, we will be
25 making a presentation on Arxana and math texts.
27 We plan to get some version of /Arxana/ working, then use it to mark
28 up some mathematical text along the lines of /IAT/ and then come up
29 with a demo which shows what such a /scholiumific representation/ is
32 ** Glossary of keywords
34 - IAT :: Inference Anchoring Theory was devised by Budzynska et
35 al \cite{budzynska2014model} to model the logical structure
36 of dialogical arguments. This has since been adapted to
37 model mathematical arguments \cite{corneli2017qand}. The
38 primary features of this adaptation are: (1) to introduce
39 more explicit relationships between pieces of mathematical
40 content; and (2) to advance a range of ``predicates'' that
41 relate mathematical propositions. These predicates
42 describe inferential structure, judgements of validity or
43 usefulness, and reasoning tactics.
44 - scholium :: A scholium is a word for a marginal annotation or
45 scholarly, explanatory, remark. Corneli and Krowne proposed
46 a "scholia-based document model" \cite{corneli2005scholia}
47 for "commons-based peer production," that is, the kind of
48 collaborative online knowledge-building that happens on
49 sites like Wikipedia or in online forums
50 \cite{benkler2002coase}, or in other digital libraries
51 broadly construed \cite{krowne2003building}. The proposal
52 is that online text resources grow ``by attaching.'' One
53 familiar class of examples is provided by revision control
54 systems, e.g., Git, which builds a network history of
55 changes to documents in a directed acyclic graph (DAG).
56 - Arxana :: Arxana is the name given to a series of prototype
57 implementations of the scholium-based document model with
58 an Emacs front-end. Arxana is inspired in part by Ted
59 Nelson's Xanadu™ project, which was the first effort to
60 work with ``hypertext'' per se
61 \cite{nelson1981literary}. We have been specifically
62 interested in applications within mathematics, which has
63 given Arxana a unique flavour. In particular, we propose
64 to use a scholium model to model the logic of proofs, not
65 just to represent mathematical texts for reading.
66 - CD :: Conceptual Dependence theory is a system for representing
67 knowledge about actions. The basis of this theory is a set of
68 /primitives/ which describe basic types of actions such as
69 "PTRANS — transfer of location" or "MBUILD — construction of a
70 thought or new information". Each primitive comes with a set
71 of /slots/ which accept objects of certain types. By filling
72 in the slots of a primitive, one obtains the most basic form
73 of a /conceptual dependency graph/. By combining such basic
74 graphs, one can build up more complicated CD graphs which
75 describe actions in greater detail.
77 ** Statement of the research problem
79 The kinds of structures that are described by ``IAT+Content''
80 are still more or less graphs. However, to work with
81 mathematics we need to be able to talk about /hypergraphs/. For
82 example, if we say ``In September 1993, an error was found in
83 Wiles's proposed proof of Fermat's Last Theorem'' we would like
84 to point to the entire proposed proof as an object. Similarly,
85 we would like to be able to draw a connection between this 1993
86 proposal with the corrected version published in 1995.
88 As we will see (*I should think! -JC*), even a proof itself is
89 more conveniently represented by hypergraph structures. In
90 particular, some of the ``predicates'' are really generative
91 functions. Indeed, some of them are ``heuristics'' which take
94 Another feature of our representation is that hypergraphs can be
95 placed inside nodes and links of other hypergraphs. This allows
96 one to organize ther representation by levels of generality. For
97 instance, at the highest level, there might be the structure of
98 statements and proofs of theorems. At thje next level, there
99 would be the individual propositions and the argument structure.
100 At the lowest level, there would be the grammatical structure of
101 the propositions. Having a way of ``coarse-graining'' the
102 representation is important in order to have it be managable and
103 allow users to zoom in and out of the map to find the appropriate
104 level of detail. This is related to Fare's categorical theory
105 of levels of a computer system [add citation].
107 One effect of this is that the markup we are devising is
108 ``progressive'' in the sense that we can describe heuristics with
109 nodes without fully formalising them. A corresponding user feature is
110 to be able to fold things at many levels. This is important because
111 the diagrams get quite large.
113 *** Proofs and prologues
115 In several of our examples, such as the Gowers problem and Artin's
116 book, on sees a structure in which a proof or calculation is preceded
117 by a kind of prologue in which the author describes motivation and
118 strategy. Unlike the proof proper which consists of mathematical
119 statements and deductions, the language here is more general and
120 the reasoning may be abductive, inductive, or heuristic.
122 We would like to have a representation for these sorts of prologues
123 and indicate how they connect with the proof which they introduce
124 as well as the rest of the text. A challenge here is that the
125 texts in question can allude and refer to all sorts of referents
126 including themselves at a high level of abstraction and require
127 a certain amount of common sense to be understood.
129 Since the issues that arise here are similar to those which arise in
130 undestanding and representing natural language stories, we should be
131 able to adapt techniques such as conceptual dependency relation or
132 goals and themes to a mathematical context.
134 *** Registers of mathematical discourse
136 The natural language which occurs in mathematical texts comes in
137 several different types. Since these types differ in ways such as
138 vocabulary, type of reasoning, subject matter, and degree of
139 literality, it simplifies the study of the subject to distinguish
140 these types and examine them individually.
142 One type of mathematical language is what we may call the /formal
143 register/. This is the type of language which is used to state
144 mathematical propositions. For example, "Every natural number can be
145 expressed as the sum of four squares." or "In every triangle, the sum
146 of the angles equals two right angles." In this register, vocabulary
147 is interpreted in a certain technical fashion and the reasoning is
148 purely deductive. Semantically, such statements are assumed to be
149 equivalent to symbolic expressions in formal logic (in whatever formal
150 system one is working). For the examples, the following would be
153 &(\forall n \in \mathbb{N}) (\exists a, b, c, d \in \mathbb{N})
154 n = a^2 + b^2 + c^2 + d^2 \\
155 &(\forall \Delta abc \in \mathrm{trinagle})
156 \angle abc + \angle bca + \angle cab = 2 * \perp
158 Indeed, in mathematical writing, such statements in natural language
159 and their formal equivalents both appear and may even be combined
160 within a single sentence, such as "Whenever $(x, y)$ lies inside the
161 region, we have $x^2 + y^4 < 12$.".
163 This register of discourse has been studied by de Bruijn, Ranta, GG
164 and others and there exist parsers which can translate between natural
165 language and formal expressions. While there is much work to be done,
166 at least some basic principles are understood and have been
167 illustrated with example programs so, for the purpose of this project,
168 we shall take this subject as given and allow ourselves to introduce
169 formal restatements of propositions without worrying about how the
170 translation might be accomplished.
172 Another type of mathematical language is what we will call the
173 /expository register/. This is the sublanguage which is used to
174 express how and why one is interested in a particular formal statement
175 and describe mathematical reasoning. Examples of such language
178 + It is easy to see that our theory is complete if we assume the
179 descending chain condition.
181 + A more elegant way of proving theorem 5 is by induction on the
182 degree; however, we chose to present the current proof because it
183 makes it clear that the result depends upon the factorizibility
186 + Is it possible to prove that any point and any line will do?
188 + Can we do this for $x+yx+y$? For $e$? Rationals with small denominator?
190 The expository register has several salient features:
192 The things which it discusses are mathematical objects and
193 mathematical propositions (as opposed, say, to physical objects or
194 psychological states). It is used to convey narratives of how one or
195 more actors navigate their way through mathematical hyperreality.
197 It is metamathematical, discussing not only with statements but also
198 inference and proofs. For instance, in the first example "it is
199 easy" says something about the proof of a statement. Likewise, it
200 discusses types of proofs and proof strategies.
202 Whereas the formal register only has deductive reasoning of the
203 strictest sort, in the expository register we also have inductive and
204 abductive reasoning as well as reasoning by analogy, heuristics, and
205 looser forms of approximate and plausible reasoning. Concomittantly,
206 the truth judgements made go beyond the truth values of formal logic
207 to vaguer assertions such as "this proof is elegant" or "this
208 statement sounds likely to be false". This is closer to what one has
209 in non-mathetical discourse. These sorts of assertions influence the
210 choice of actions and strategies.
214 In order to build a theory of the expository register, we will draw
215 upon several well-studied topics in AI which deal with situations
216 that have common features, namely the block world, board games, and
219 | | Block World | Board Games | Story Comprehension | Mathematical Texts |
220 |---+-------------+-------------+---------------------+--------------------|
223 ** Suitability of venue
225 As we will also see, it is not just incidental that our work is
226 implemented in LISP. Actually, the kind of hypergraph programs
227 we use are a ``natural'' extension of the basic LISP data model.
229 Emacs (and Org mode) are suitable for interacting with other
230 programming languages and long-running processes, e.g., MAXIMA.
232 *** What is on offer in this approach
234 One thing we have here is links that contain code.
236 Another thing hypergraphs give us is links to links - of course
237 we can also think about higher-dimensional versions of the same,
242 Here we'll describe the structures coming from several different
243 places, e.g., Gabi, Lakatos, etc.
245 ** Content (=structure=) :GRAY:
246 *** object $O$ is =used_in= proposition $P$
247 **** Example: ``The Caley graph of group \(G\)'' has sub-object $G$
248 *** proposition $Q$ is a =sub-proposition= of proposition $P$
249 **** Example: ``$P$ is difficult to prove'' has sub-proposition $P$
250 *** proposition $R$ is a =reformed= version of proposition $P$
251 **** Example: ``Every $x$ is a \(P\)'' might be reformed to ``Some $x$ is a \(P\)''
252 *** property $p$ is as the =extensional_set= of all objects with property $p$
253 **** Example: the set $\mathcal{P}$ of primes is the extension of the predicate $\mathit{prime}$.
254 *** $O$ =instantiates= some class $C$
255 **** Comment: This is not quite syntactic sugar for =has_property=!
256 If we have a class of items $C$ we want to be able say that $x$ is a
257 member of $C$. In principle, we could write $x$ =has_property= $C$.
258 But I think there are cases where we would want to
259 distinguish between, e.g.,
260 $2$ =has_property= prime, and $prime(2)$ =instantiates=
261 $prime(x)$. This =instantiates= operation is a natural extension of
262 backquote; so e.g., we could write the true statement
263 $prime(4)$ =instantiates= $prime(x)$, even though $prime(4)$ is false.
264 **** Comment: Perhaps we need a further distinction between objects and 'schemas'
265 So we might write =has_property(member_of(x,primes))= to talk about
266 class membership. Presumably (except in Russell paradox situations)
267 this is the same as =has_property(x,prime)=, or whatever.
268 *** $s$ =expands= $y$
269 **** Comment: This is something that a computer algebra system like MAXIMA could confirm
271 **** Comment: This is something that a computer algebra system like MAXIMA could confirm
272 *** $s$ =contains as summand= $t$
273 **** Comment: This is more specific than the =used in= relation
274 This relation is interesting, for example, in the case of sums like
275 $s+t$ where $t$ is, or might be, ``small''. Note that there
276 would be similar ways to talk about any algebraic or
277 syntactic relation (e.g., multiplicand or integrand or whatever).
278 In my opinion this is better than having one general-purpose 'structural'
279 relation that loses the distinction between all of these. However,
280 generalising in this way does open a can of worms for addressing.
281 I.e. do we need XPATH or something like that for indexing into
282 something deeply nested?
283 *** $M$ =generalises= $m$
284 **** Comment: Here, content relationships between methods.
285 Does this work? Instead of talking about content relationships 'at
286 the content level' we are now interested in assertions like
287 "binomial theorem" =generalises= "eliminate cross terms",
288 where both of the quoted concepts are heuristics, not 'predicates'
289 *** Proposition vs Object vs Binder vs Inference rule?
290 Note that there are different kinds of `content'. If for example I
291 say `\(0<a<b<1 \Rightarrow a^N < b^N\)', then this is more than just a
292 proposition, but something that can be used as a ``binder''; i.e., if
293 I fill in specific values of $a$ and $b$ (and, optionally, $N$) I know
294 the property holds for them. At the same time, this sort of "binder"
295 is presumably also a *theorem* that has been proved. This is,
296 additionally, similar to an *inference rule* since it allows us to move
297 from one statement to another, schematically (see discussion above
298 about "instantiates"). Anyway, this isn't yet about another kind of
299 structural relation, but it does suggest that we should be a bit
300 careful about how we think about content.
301 ** inferential structure (=rel=) :PINK:
304 *** =conjunction= (s,t)
305 *** =has_property= (o,p)
306 **** Comment: It seems useful in some case to be able to say that a 'method' or heuristic has a property
307 E.g. =has_property(strategyx, HAL)=
308 **** Comment: has_property should probably 'emit' the property as a side-effect
309 This way we can more easily see which is the object and which is the property.
310 It seems that thing that has a property may also be a 'proposition',
311 or, at least, a bit of 'object code' (like: "compute XYZ").
312 Furthermore, at least in this case, the 'property' might be a heuristic
313 or method (like "we actually know how to compute this").
314 *** =instance_of= (o,m)
315 *** =independent_of= (o,d)
316 *** =case_split= (s, {si}.i)
318 ** reasoning tactics; ``meta''/guiding (=meta=) :BLUE:
321 **** Note: use method $m$ to prove $s$
322 **** Comment: perhaps this should be =strategy= (m [, s ]) so that s is optional
323 This is because, just for graphical simplicity, we might assume that
324 the statement that we want to prove is known in advance (e.g., it is
325 the statement of the problem).
327 This is the style at the beginning of gowers-example.pdf
328 **** Comment: how to show that a suggestion 'has been implemented'?
329 We might need some other form of 'certificate' for that.
330 E.g., it would say =implements(BLOB OF CODE,strategyx)=.
331 *** =auxiliary= (s,a)
333 **** Comment: analogies between statements are different from auxiliaries to prove
334 Introducing some set of 'analogies' in a way sets us up for
335 'inductive' reasoning across a class of examples. What do they all
336 have in common? Which one is the most suitable? Etc.
337 ** heuristics and value judgements (=value=) :GREEN:
343 **** Comment: It seems that we will have several layers of 'guidance'
344 Many of them will be neither value judgements nor metamathematical tags
345 like =strategy=, =goal=, or =auxiliary=. Rather, the heuristics may be
346 used at an even higher level to produce or to implement these. So,
347 for example, the heuristic might be what a =strategy= concretely
348 suggests. It's also true that a given =auxiliary= might need a
349 heuristic "header", that explains /why/ this auxiliary problem has
350 been suggested. Similar to a =strategy= the heuristic might look
351 for something that 'satisfies' or 'implements' the heuristics.
352 In some cases we've looked at, this 'satisficing' object will appear
353 directly as the argument of the heuristic, hence =heuristic(x)=.
354 For example: =specialise(THE PROBLEM, (sqrt(2)+sqrt(3))^2)=.
355 Incidentally, this particular example is only meaningful in connection
356 with *another* heuristic that has told us how to *generalise* the
357 problem, i.e., that has turned a static expression into something
358 with a variable in it.
359 ** Performatives (=perf=) :YELLOW:
360 *** =Agree= (s [, a ])
361 **** Note: optional argument $a$ is a justification for $s$
362 *** =Assert= (s [, a ])
363 **** Note: optional argument $a$ is support for $s$
364 **** Comment: It seems like we might want to be able to assert a 'graph structure'
365 Here is an example from early in gowers-example.pdf
367 Assert(exists(strategy(PROBLEM, strategyx))
368 AND has_property(strategyx,HAL))
370 *** =Challenge= (s [, c ])
371 **** Note: $c$ is a counter-argument or counter-example to $s$
373 **** Note: object with name $o$ satisfies property $p$
375 **** Note: takes a =value= argument
377 *** =QueryE= ({pi(X)}.i)
378 **** Note: Asks for the class of objects for which all of the properties pi hold
379 *** =Retract= (s [, a ])
380 **** Note: can only be made by someone who asserted $s$; $a$ is an optional reason
382 **** Note: Takes a =meta= argument
384 * Extensions to the core
388 By itself, IAT is useful for describing *what* takes place in a
389 mathematical discourse, but not so useful for figuring out *why*
390 and *how*. To adress these issues, we will augment it with the
391 framework of /conceptual dependency theory/ (CD), which has been used
392 for such purposes in the context of machine understanding of stories.
394 The main ingredient of CD is a set of primitives which describe
395 types of actions. Ususally, these consist of various physical and
396 mental operations but, for the purpose at hand, we will take them to
397 be the performatives of IAT.
399 We will have two classes of objects: the participants in the dialogue
400 and mathematical propositions.
402 *** TODO We should figure out what the inferences between basic assertions (I/R, I/E, etc.) would look like here.
406 In order to figure out why and how actions take place, CD theory
407 introduces procedural knowledge in the form of scripts, MOPs, TOPs,
408 goals, and plans. For our purposes, goals and plans will be used.
410 This relates to the meta items of the spec. Maybe we should expand
411 the goal item using some sort of ontology like that of Schank and
422 This file is in versioned storage in the "mob" branch of our arxana
423 repo; instructions to access are here:
424 http://repo.or.cz/w/arxana.git/blob_plain/d187e244a8eb7d2208f1fe98db1ef895c6cd4a36:/README.mob
426 A working copy of this repository is checked out at
427 =/home/shared-folder/arxana-redux/arxana/= on the Linode.
429 And a "scratch" copy of the file has been copied to:
430 =/home/shared-folder/arxana-redux/arxana-redux.org=
432 This can be edited in live sessions using =togetherly.el=.
436 *** Corpus/Examples: Hand-drawn diagrams in IAT+C
438 /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./
440 - Minipolymath, treated by Gabi in the Transactions on Social Computing paper, pdf available from https://www.overleaf.com/read/jyhzpqsythzq
441 - Our randomly selected MathOverflow discussion (from Q&A article)
442 - Gowers 2012 trick problem, http://metameso.org/ar/gowers-example.pdf
443 - Also there's Schuam's Abstract Algebra exercise 337, a diagram is shown on arxana.net.
444 - Redone using IATC: http://metameso.org/ar/schuams-example.pdf
445 - An example from the Ganesalingam and Gowers paper: http://metameso.org/ar/robotone-example.pdf
446 - Galois theory. Emil Artin's book.
448 - possibly an example from metamath or coq or whatever to show that we can model that stuff as discourse...
453 **** Items we've worked on before
455 Over the years as we've worked on Arxana, we have generated all sorts
456 of files. Here are descriptions and locations of some of them which
457 are relevant to the current project.
459 Many of these are stored in =/home/shared-folder/public_html/=, and
460 accessible on the web at [[http://metameso.org/ar/]].
464 - "nemas" document: http://metameso.org/ar/metamathematics.pdf
465 - Joe's thesis Appendix B: http://metameso.org/ar/thesis-appendix-b.pdf
466 - Metamathematics preprint: http://metameso.org/ar/mathematical-semantics.pdf
467 - hcode function spec: http://metameso.org/ar/hcode.pdf
468 - Lakatos game spec: http://metameso.org/ar/lakatos-flowchart.pdf
472 - [[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.
473 - [[http://metameso.org/cgi-bin/current.pl/Two_years_later][Two years later]] collects many of the mathematical themes in
475 - [[http://metameso.org/cgi-bin/current.pl/samples_of_formal_mathematical_writing][samples of formal mathematical writing]] is a small collection
476 of statements in mathematical language (leaving out ``the part
477 in between dollar signs'')
481 - [[http://arxana.net][arxana.net]] has links to source code from various prototypes
482 - It also has a small gallery of hand-drawn diagrams
484 **** And other things elsewhere:
486 - Handbook of artificial intelligence by Feigenbaum (Sam and Pam)
487 - 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]])
488 - Could we reuse this stuff for the "narrative"
489 - How do we know how to read the text and transform it into IATC?
490 - An example is Gowers's "total stuckness": how do we turn that into code?
491 - Conceptual dependency representation - from "Deep Blue" website ([[https://deepblue.lib.umich.edu/bitstream/handle/2027.42/30278/0000679.pdf?sequence=1][link]]).
492 - AI textbook in wiki.
494 *** TODO Initial non-working pseudocode prototype
496 Here it makes sense to at least try and transcribe the main examples
497 in some "pseudocode", inspired by IATC and hcode, which we can then
498 refine into a working version later.
500 Several examples have been transcribed:
502 - http://metameso.org/ar/mpm3.html
503 - http://metameso.org/ar/gowers2012.html
504 - http://metameso.org/ar/robotone-opensets.html
506 However, as per the headline, these don't currently *do* anything.
508 *** TODO Basic working version
510 *** TODO Can the system come up with answers to new, basic, questions?
512 - Inspired by Nuamah et al's geography examples
513 - Simple comparisons, like, how does this concept relate to that concept? We informally talk about this as ``analogy'' between concepts. But...
515 *** TODO Foldable views (like in Org mode) so that people can browse proofs
517 - This may come after the May submission
518 - Folding and unfolding the definitions of terms in something like an APM context is relevant example. Just `unpacking' terms.
522 ** In a mathematics context
524 - ``Lakatos-style Collaborative Mathematics through Dialectical,
525 Structured and Abstract Argumentation'' shows how it is possible to
526 ``formalize'' the informal logic proposed by Lakatos
527 \cite{pease2017lakatos}.
528 - [[http://www.emis.de/monographs/Trzeciak/biglist.html][Mathematical English Usage - a Dictionary]] (Jerzy Trzeciak)
529 - [[https://case.edu/artsci/math/wells/pub/html/abouthbk.html][The Handbook of Mathematical Discourse]] (Charles Wells)
530 - [[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)
532 ** Does what we're doing relate in any way to other formal proof checkers?
534 - 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.
536 - 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})
538 - There's also a generative program by Ganesalingam and Gowers thath meshes natural language and formal mathematical reasoning.
540 - 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 formally verified.
544 /We're probably better off pruning these out of the final paper, but some topics of interest can be noted here./
546 - One interesting project within the DAG paradigm is the
547 [[https://github.com/ipfs/ipfs/blob/master/papers/ipfs-cap2pfs/ipfs-p2p-file-system.pdf][InterPlanetary File System]] (IPFS).
551 - I think it is probably not realistic to get the clojure.spec
552 type-based work running *in addition* to the scholium-based
553 stuff, but the topics seem related. In particular, the
554 objects that we would describe using clojure.spec are somehow
555 the "C" in IAT+C. So, we could have a think about how
556 structural relationships between objects and propositions (per
557 Gabi's description of IAT+C) might relate to the clojure.spec
558 stuff. I think would be appropriate to have a few pages of
559 ``future work'' describing these issues.
561 * References :noexport:
563 # bibliography items are rendered
564 # with the following command
571 Tasks, timeline, and other things we don't need to include in the
576 Note: this could be more nicely organized using the org agenda.
579 *** Science March on Saturday
581 *** Met: Tuesday 25th April
582 *** DONE Joe get this document under version control
584 *** Meet Monday 1 May (note: this is a Bank Holiday in the UK)
586 *** Meet Saturday May 13
588 *** *outline* of talk May 16th
590 *** *Present* 23/24th May at [[http://dream.inf.ed.ac.uk/events/ciao-2017/][CIAO 2017]]. :TALK:
591 *** *Submit* 26th May :DEADLINE:
595 *** DONE Figure out what to do and record it in this document. :meta:
596 *** DONE Set up collaborative editing for files.
597 *** WONTFIX Some way to share images (e.g. whiteboard in BBB or screenshare or...)
598 *** DONE Debug Togetherly
599 *** DONE make =visible-mode= on by default in this buffer
602 The following is for controlling Togetherly and Org mode. This might
603 not be necessary if line 454 of togetherly.el is commented
604 out/changed. Also, it isn't actually evaluated. How to fix?
607 #+BEGIN_SRC emacs-lisp
608 (defun execute-startup-block ()