From 3ba73456aec1a17d00f431da57a99c603798baa8 Mon Sep 17 00:00:00 2001 From: Joe Corneli Date: Sat, 27 May 2017 21:56:15 +0100 Subject: [PATCH] add revised outline --- org/farm-2017.org | 144 ++++++++++++++++++++++++++++++++---------- org/farm-refs.bib | 183 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 293 insertions(+), 34 deletions(-) create mode 100644 org/farm-refs.bib diff --git a/org/farm-2017.org b/org/farm-2017.org index f2e3f7a..6a622ab 100644 --- a/org/farm-2017.org +++ b/org/farm-2017.org @@ -1,6 +1,25 @@ -* OUTLINE - -#+BEGIN_COMMENT +#+TITLE: Functional models of mathematical reasoning +#+AUTHOR: Joe Corneli, Raymond Puzio +#+EMAIL: contact@planetmath.org +#+DATE: May 27, 2017 for Thursday 1 June, 2017 deadline +#+DESCRIPTION: Outline and draft of 12 page paper on math text analysis for FARM workshop at ICFP 2017 +#+KEYWORDS: arxana, hypertext, inference anchoring theory +#+LANGUAGE: en +#+OPTIONS: H:3 num:nil 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: +#+BIBLIOGRAPHY: farm-refs plain +#+LATEX_HEADER: \usepackage[backend=bibtex,sorting=none]{biblatex} +#+LATEX_HEADER: \addbibresource{farm-refs} +#+STARTUP: showeverything + + +#+BEGIN_QUOTE Functional Programming has emerged as a mainstream software development paradigm, and its artistic and creative use is booming. A growing number of software toolkits, frameworks and environments for @@ -20,56 +39,113 @@ purely functional (“mostly functional” is fine), and may be manifested as a domain specific language or tool. Moreover, submissions focusing on questions or issues about the use of functional programming are within the scope. -#+END_COMMENT +#+END_QUOTE + +* 0 Introduction + +** 0.1 CONTEXT OF APPLICATION +- modelling mathematical dialogues, people don't just write their things in metamath +- people may make different expository choices +- mathematical text contains argumentation an narrative in addition to logic and calculations ([[1.2][1.2]]) +** 0.2 FORCES +- push to make everything formal (QED, Tarski, LCF) [[1.1][1.1]] +- push to make everything understandable (Alexander) +** 0.3 PROBLEM +- each different user will have a different "way in", depending on their background knowledge ([[3.2][3.2]]) +- how to get behind the scenes to see why? +- how to tailor a given formal content to a given reader? +** 0.4 SOLUTION (STRATEGY) +- focus on expressivity +- focus on representing process +- formalization and efficiency are important, but will be left for later. +** 0.5 RATIONALE +- objective: understand mathematics as people do it (literary criticism, rhetoric, argumentation) +- objective: learn from these methods to build new mathematical texts +- build on intuitive diagrams +- build on the idea of parsing natural language (complementary to Mohan's work) +** 0.6 RESOLUTION of FORCES +- outcome: sharing diagrams with people who can use them +- potential: draw new diagrams +- philosophical: bridging 'two cultures' (proof checkers and artists/designers/hackers) + +* 1 THEORETICAL FOUNDATIONS Informal mathematical language is more general, and the reasoning involved may be abductive, inductive, or heuristic. :RAY: + +Even though a mathematical result and its proof involve strict logic, +the process of formulating, motivating proving and explaining go +beyond strict formality. (Pierce, Lautman) + +** <<1.1>> 1.1 Examples of actual texts (different registers) + +*** TODO Pull up examples from real texts. + +- E.g. Artin's Galois theory book +- E.g. Gowers's "Eventually this is something a computer can solve" + +** <<1.2>> 1.2 A formal language doesn't do anything with this ("Proofs and Prologues") + +- (Conclusion from inductive reasoning in 1.1.) + +* 2 LANGUAGE DESIGN The presentation here will describe a strategy we have been developing for representing mathematical dialogues and other informal texts. :JOE: + +Since we cannot simply build on formal theorem proving, we need to +look further afield for prior work on which to build. (Bundy: choosing +representation strategy that fits can make the problem easier to +solve; Corneli: here we are looking for representations *of* +reasoning, so this gives us a heuristic to guide our search.) + +** <<2.1>> 2.1 Gabi's work on IATC +** <<2.2>> 2.2 Lytinen CD -** 1 THEORETICAL FOUNDATIONS Informal mathematical language is more general, and the reasoning involved may be abductive, inductive, or heuristic. +* 3 IMPLEMENTATION ISSUES (REQUIREMENTS) :JOE: -*** 1.1 -*** 2.2 +We've already seen an *abstract* model of social creativity in +Lakatos, but when we try to zoom in and look at concrete details, we +see further challenges. We know that a 'city is not a tree', let's +generalise and assert that a proof dialogue is not a tree. This gives +us a guiding principle. -** 2 LANGUAGE DESIGN The presentation here will describe a strategy we have been developing for representing mathematical dialogues and other informal texts. +** <<3.1>> 3.1 Let's look at one of our illustrations: it's a graph, no it's a hypergraph! -*** 2.1 -*** 2.2 +** <<3.2>> 3.2 Reason as a social thing (Minsky, Sperber & Mercier, Gowers 'quantum of progress' from Polymath) -** 3 IMPLEMENTATION ISSUES A publication appearing in "Artificial Intelligence" this month describes the high-level features of informal mathematics, and helped inspire this project. +** <<3.3>> 3.3 Lakatos stuff: How is this different from what we're doing? -*** 3.1 -*** 3.2 +* 4 APPLICATIONS Our latest efforts produce more detailed models of mathematical arguments. :JOE: +We need to model what's there and how it evolves, noting that evolution is heuristic -** 4 APPLICATIONS Our latest efforts produce more detailed models mathematical arguments. +** <<4.1>> 4.1 Kinematics (IATC+CD) +** <<4.2>> 4.2 Dynamics (Lytinen's stuff with goals and scripts) -*** 4.1 -*** 4.2 +* 5 MECHANICAL ENGINEERING DESIGNS A graphical formalism and a corresponding prototype implementation will be described. :RAY: -** 5 A graphical formalism and a corresponding prototype implementation will be described. +** <<5.1>> 5.1 Import and improve technical stuff on Arxana (cf. Nemas doc) +** <<5.2>> 5.2 Example -*** 5.1 -*** 5.2 +* 6 RELATED WORK (GAMES, POETRY): parallels between dialogues and discursive Q&A, traditional proofs. :JOE: -** 6 Applications include modelling collaborative proof dialogues and discursive Q&A, as well as more traditional proofs. +How does this look in a broader context? -*** 6.1 -*** 6.2 +** <<6.1>> 6.1 prior art: board games, story stuff; table that compares between. +** <<6.2>> 6.2 Alexander: "a city is not a tree"; compare Lamport -** 7 In our planned next steps we plan to bring in explicit type-theoretic representations of mathematical objects within a service-oriented architecture./ +----- -*** 7.1 -*** 7.2 +* 7 PART TWO In our planned next steps we plan to bring in explicit type-theoretic representations of mathematical objects within a service-oriented architecture. :onhold: -** 8 mob programming +** <<7.1>> 7.1 There is a degree of formality in the specifications, but also informality in the heuristics. -*** 8.1 -*** 8.2 +* 8 MOB PROGRAMMING :onhold: -** 9 music from corneli, pease, stefanou survey ("Chapter 6") +** <<8.1>> +** <<8.2>> -*** 9.1 -*** 9.2 +* 9 RELATED WORK music from corneli, pease, stefanou survey ("Chapter 6"); NNexus project; Socratic :onhold: -** 10 prior art: board games, story stuff +** <<9.1>> +** <<9.2>> -*** 10.1 -*** 10.2 +* 10 CONCLUSION :onhold: +** <<10.1>> +** <<10.2>> diff --git a/org/farm-refs.bib b/org/farm-refs.bib new file mode 100644 index 0000000..078963f --- /dev/null +++ b/org/farm-refs.bib @@ -0,0 +1,183 @@ +@inproceedings{corneli2005scholia, +title={A Scholia-based Document Model for Commons-based Peer Production}, +author={J. Corneli and A. Krowne}, +booktitle={Free Culture and the Digital Library Symposium Proceedings}, +address={Atlanta, Georgia}, +editor={M. Halbert}, +publisher={MetaScholar Initiative at Emory University}, +pages={240--253}, +year={2005}, +url={http://metameso.org/~joe/docs/sbdm.html}, +keywords = {scholia, commons-based peer production} +} + +@inproceedings{budzynska2014model, + author = {Katarzyna Budzynska and + Mathilde Janier and + Chris Reed and + Patrick Saint{-}Dizier and + Manfred Stede and + Olena Yaskorska}, + title = {A Model for Processing Illocutionary Structures and Argumentation in Debates}, + booktitle = {Proceedings of the Ninth International Conference on Language Resources + and Evaluation (LREC-2014), Reykjavik, Iceland, May 26-31, 2014.}, + pages = {917--924}, + year = {2014}, + url = {http://www.lrec-conf.org/proceedings/lrec2014/summaries/77.html}, + timestamp = {Fri, 26 Sep 2014 08:11:49 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/lrec/BudzynskaJRSSy14}, + bibsource = {dblp computer science bibliography, http://dblp.org}, + keywords = {inference anchoring theory, IAT} +} + +@misc{corneli2017qand, +title={Towards mathematical {AI} via a model of the content and process of mathematical dialogues}, +author={Joseph Corneli and Ursula Martin and Dave Murray-Rust and Alison Pease}, +howpublished={Submitted to: \emph{Conferences on Intelligent Computer Mathematics 2017}}, + keywords = {knowledge representation and reasoning, IATC} +} + +@article{benkler2002coase, + title={Coase's {Penguin}, or, {Linux} and {``}{The} {Nature} of the {Firm}{''}}, + author={Benkler, Yochai}, + journal={Yale Law Journal}, + pages={369--446}, + year={2002}, + publisher={JSTOR}, + keywords = {commons-based peer production} +} + + +@article{krowne2003building, + title={Building a digital library the commons-based peer production way}, + author={Krowne, Aaron}, + journal={D-Lib magazine}, + volume={9}, + number={10}, + year={2003}, + keywords = {commons-based peer production, digital libraries} +} + +@book{nelson1981literary, + author = {Nelson, T.H.}, + title = {{L}iterary {M}achines: {T}he report on, and of, {P}roject {X}anadu concerning word processing, electronic publishing, hypertext, thinkertoys, tomorrow's intellectual revolution, and certain other topics including knowledge, education and freedom}, + publisher = {Sausalito, California: Mindful Press}, + year = {1981}, + keywords = {hypertext, knowledge} +} + +@article{pease2017lakatos, +author = {Alison Pease and John Lawrence and Katarzyna Budzynska and Joseph Corneli and Chris Reed}, +title = {Lakatos-style Collaborative Mathematics through Dialectical, Structured and Abstract Argumentation}, +journal = {Artificial Intelligence}, +volume = {246}, +pages = {181--219}, +year = {2017}, +month={May}, +addendum = {{\textbf{CORE: A*}}}, +keywords = {argumentation, mathematics} +} + +@inproceedings{kaliszyk2014developing, + title={Developing corpus-based translation methods between informal and formal mathematics}, + author={Kaliszyk, Cezary and Urban, Josef and Vysko{\v{c}}il, Ji{\v{r}}{\'\i} and Geuvers, Herman}, + booktitle={International Conference on Intelligent Computer Mathematics}, + pages={435--439}, + year={2014}, + organization={Springer}, + url={http://cl-informatik.uibk.ac.at/cek/docs/14/ckjujvhg-cicm14-poster.pdf}, + keywords = {corpus-based translation} +} + +@misc{kaliszyk2014developing-misc, + title={Developing corpus-based translation methods between informal and formal mathematics [{P}oster of \cite{kaliszyk2014developing}]}, + author={Kaliszyk, Cezary and Urban, Josef and Vysko{\v{c}}il, Ji{\v{r}}{\'\i} and Geuvers, Herman}, + url={http://cl-informatik.uibk.ac.at/cek/docs/14/ckjujvhg-cicm14-poster.pdf}, + note={\url{http://cl-informatik.uibk.ac.at/cek/docs/14/ckjujvhg-cicm14-poster.pdf}}, + keywords = {corpus statistics} +} + +@inproceedings{sowa2003analogical, + title={Analogical reasoning}, + author={Sowa, John F and Majumdar, Arun K}, + editor={A. Aldo and W. Lex and B. Ganter}, + booktitle={Conceptual Structures for Knowledge Creation and Communication: 11th International Conference on Conceptual Structures, ICCS 2003, Dresden, Germany, July 21-25, 2003, Proceedings}, + pages={16--36}, + series={LNAI}, + number={2746}, + year={2003}, + organization={Springer}, + keywords = {analogical reasoning} +} + +@incollection{sowa2008conceptual, + title={Conceptual Graphs}, + author={Sowa, John F}, + booktitle={Handbook of Knowledge Representation}, + editor={van Harmelen, F. and Lifschitz, V. and Porter, B.}, + publisher={Elsevier}, + year={2008}, + pages={213--237}, + chapter={5}, + keywords = {conceptual graphs}} + +@article{lytinen1992conceptual, + title={Conceptual dependency and its descendants}, + author={Lytinen, Steven L}, + journal={Computers \& Mathematics with Applications}, + volume={23}, + number={2-5}, + pages={51--73}, + year={1992}, + publisher={Elsevier}, + keywords = {conceptual dependency} +} + +@article{schank1972conceptual, + title={Conceptual dependency: A theory of natural language understanding}, + author={Schank, Roger C}, + journal={Cognitive psychology}, + volume={3}, + number={4}, + pages={552--631}, + year={1972}, + publisher={Academic Press}, + keywords = {conceptual dependency, natural language} +} + +@phdthesis{leon2011computational, + title={A computational model for automated extraction of structural schemas from simple narrative plots}, + author={Le{\'o}n Aznar, Carlos}, + year={2011}, + school={Universidad Complutense de Madrid, Servicio de Publicaciones}, + keywords={stories} +} + +@book{barr1981handbook, + title={The handbook of artificial intelligence}, + author={Barr, Avron and Feigenbaum, Edward A}, + volume={1}, + year={1981}, + publisher={Butterworth-Heinemann}, + url={https://archive.org/details/handbookofartific01barr}, + keywords={handbook} +} + +@inproceedings{corneli2017towards, +title={Towards mathematical {AI} via a model of the content and process of mathematical question and answer dialogues}, +author={Joseph Corneli and Ursula Martin and Dave Murray-Rust and Alison Pease}, +booktitle={Intelligent Computer Mathematics 10th International Conference, CICM 2017, Edinburgh, UK, 2017, Proceedings}, +editor={Herman Geuvers and Matthew England and Osman Hasan and Florian Rabe and Olaf Teschke}, +year={2017}, +url={http://metameso.org/~joe/papers/corneli2017towards.pdf}, +keywords={IATC}} + +@inproceedings{martin2017bootstrapping, +title={Bootstrapping the next generation of mathematical social machines}, +author={Ursula Martin and Alison Pease and Joseph Corneli}, +booktitle={Off the Beaten Track workshop at POPL, UPMC Paris, January 21, 2017}, +editor={Kuper, Lindsey and Atkey, Bob}, +year={2017}, +organization={\textbf{ACM}}, +url={http://popl17.sigplan.org/event/obt-2017-talk-5}, +keywords={IATC, social machines}} \ No newline at end of file -- 2.11.4.GIT