org/farm-refs.bib

   1 @inproceedings{corneli2005scholia,
   2 title={A Scholia-based Document Model for Commons-based Peer Production},
   3 author={J. Corneli and A. Krowne},
   4 booktitle={Free Culture and the Digital Library Symposium Proceedings},
   5 address={Atlanta, Georgia},
   6 editor={M. Halbert},
   7 publisher={MetaScholar Initiative at Emory University},
   8 pages={240--253},
   9 year={2005},
  10 url={http://metameso.org/~joe/docs/sbdm.html},
  11 keywords = {scholia, commons-based peer production}
  12 }
  13
  14 @inproceedings{budzynska2014model,
  15   author    = {Katarzyna Budzynska and
  16                Mathilde Janier and
  17                Chris Reed and
  18                Patrick Saint{-}Dizier and
  19                Manfred Stede and
  20                Olena Yaskorska},
  21   title     = {A Model for Processing Illocutionary Structures and Argumentation in Debates},
  22   booktitle = {Proceedings of the Ninth International Conference on Language Resources
  23                and Evaluation (LREC-2014), Reykjavik, Iceland, May 26-31, 2014},
  24   pages     = {917--924},
  25   year      = {2014},
  26   url       = {http://www.lrec-conf.org/proceedings/lrec2014/summaries/77.html},
  27   timestamp = {Fri, 26 Sep 2014 08:11:49 +0200},
  28   biburl    = {http://dblp.uni-trier.de/rec/bib/conf/lrec/BudzynskaJRSSy14},
  29   bibsource = {dblp computer science bibliography, http://dblp.org},
  30   keywords = {inference anchoring theory, IAT}
  31 }
  32
  33 @article{benkler2002coase,
  34   title={Coase's {Penguin}, or, {Linux} and {``}{The} {Nature} of the {Firm}{''}},
  35   author={Benkler, Yochai},
  36   journal={Yale Law Journal},
  37   pages={369--446},
  38   year={2002},
  39   publisher={JSTOR},
  40   keywords = {commons-based peer production}
  41 }
  42
  43
  44 @article{krowne2003building,
  45   title={Building a digital library the commons-based peer production way},
  46   author={Krowne, Aaron},
  47   journal={D-Lib magazine},
  48   volume={9},
  49   number={10},
  50   year={2003},
  51   keywords = {commons-based peer production, digital libraries}
  52 }
  53
  54 @book{nelson1981literary,
  55         author = {Nelson, T.H.},
  56         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},
  57         publisher = {Sausalito, California: Mindful Press},
  58         year = {1981},
  59         keywords = {hypertext, knowledge}
  60 }
  61
  62 @INPROCEEDINGS{pease:05,
  63  AUTHOR   ={Pease, A., Colton, S., Smaill, A., and Lee, J.},
  64  YEAR     ={2005},
  65  TITLE    ={Modelling Lakatos's philosophy of mathematics},
  66  BOOKTITLE={Computing, philosophy and cognition: Proceedings of the European Computing and Philosophy Conference (ECAP 2004)},
  67  PAGES = {57-85},
  68  EDITOR   ={Magnani, L. and Dossena, R.},
  69  PUBLISHER={College Publications},
  70  ADDRESS  ={},
  71  }
  72
  73 @article{pease2017lakatos,
  74 author = {Alison Pease and John Lawrence and Katarzyna Budzynska and Joseph Corneli and Chris Reed},
  75 title = {Lakatos-style Collaborative Mathematics through Dialectical, Structured and Abstract Argumentation},
  76 journal = {Artificial Intelligence},
  77 volume = {246},
  78 pages = {181--219},
  79 year = {2017},
  80 month={May},
  81 addendum = {{\textbf{CORE: A*}}},
  82 keywords = {argumentation, mathematics}
  83 }
  84
  85 @inproceedings{kaliszyk2014developing,
  86   title={Developing corpus-based translation methods between informal and formal mathematics},
  87   author={Kaliszyk, Cezary and Urban, Josef and Vysko{\v{c}}il, Ji{\v{r}}{\'\i} and Geuvers, Herman},
  88   booktitle={International Conference on Intelligent Computer Mathematics},
  89   pages={435--439},
  90   year={2014},
  91   organization={Springer},
  92   url={http://cl-informatik.uibk.ac.at/cek/docs/14/ckjujvhg-cicm14-poster.pdf},
  93   keywords = {corpus-based translation}
  94 }
  95
  96 @misc{kaliszyk2014developing-misc,
  97   title={Developing corpus-based translation methods between informal and formal mathematics [{P}oster of \cite{kaliszyk2014developing}]},
  98   author={Kaliszyk, Cezary and Urban, Josef and Vysko{\v{c}}il, Ji{\v{r}}{\'\i} and Geuvers, Herman},
  99   url={http://cl-informatik.uibk.ac.at/cek/docs/14/ckjujvhg-cicm14-poster.pdf},
 100   note={\url{http://cl-informatik.uibk.ac.at/cek/docs/14/ckjujvhg-cicm14-poster.pdf}},
 101   keywords = {corpus statistics}
 102 }
 103
 104 @inproceedings{sowa2003analogical,
 105   title={Analogical reasoning},
 106   author={Sowa, John F and Majumdar, Arun K},
 107   editor={A. Aldo and W. Lex and B. Ganter},
 108   booktitle={Conceptual Structures for Knowledge Creation and Communication: 11th International Conference on Conceptual Structures, ICCS 2003, Dresden, Germany, July 21-25, 2003, Proceedings},
 109   pages={16--36},
 110   series={LNAI},
 111   number={2746},
 112   year={2003},
 113   organization={Springer},
 114   keywords = {analogical reasoning}
 115 }
 116
 117 @incollection{sowa2008conceptual,
 118   title={Conceptual Graphs},
 119   author={Sowa, John F},
 120   booktitle={Handbook of Knowledge Representation},
 121   editor={van Harmelen, F. and  Lifschitz, V. and Porter, B.},
 122   publisher={Elsevier},
 123   year={2008},
 124   pages={213--237},
 125   chapter={5},
 126   keywords = {conceptual graphs}}
 127
 128 @article{lytinen1992conceptual,
 129   title={Conceptual dependency and its descendants},
 130   author={Lytinen, Steven L},
 131   journal={Computers \& Mathematics with Applications},
 132   volume={23},
 133   number={2-5},
 134   pages={51--73},
 135   year={1992},
 136   publisher={Elsevier},
 137   keywords = {conceptual dependency}
 138 }
 139
 140 @article{schank1972conceptual,
 141   title={Conceptual dependency: A theory of natural language understanding},
 142   author={Schank, Roger C},
 143   journal={Cognitive psychology},
 144   volume={3},
 145   number={4},
 146   pages={552--631},
 147   year={1972},
 148   publisher={Academic Press},
 149   keywords = {conceptual dependency, natural language}
 150 }
 151
 152 @phdthesis{leon2011computational,
 153   title={A computational model for automated extraction of structural schemas from simple narrative plots},
 154   author={Le{\'o}n Aznar, Carlos},
 155   year={2011},
 156   school={Universidad Complutense de Madrid, Servicio de Publicaciones},
 157   keywords={stories}
 158 }
 159
 160 @book{barr1981handbook,
 161   title={The handbook of artificial intelligence},
 162   author={Barr, Avron and Feigenbaum, Edward A},
 163   volume={1},
 164   year={1981},
 165   publisher={Butterworth-Heinemann},
 166   url={https://archive.org/details/handbookofartific01barr},
 167   keywords={handbook}
 168 }
 169
 170 @inproceedings{corneli2017towards,
 171 title={Towards mathematical {AI} via a model of the content and process of mathematical question and answer dialogues},
 172 author={Joseph Corneli and Ursula Martin and Dave Murray-Rust and Alison Pease},
 173 booktitle={Intelligent Computer Mathematics 10th International Conference, CICM 2017, Edinburgh, UK, 2017, Proceedings},
 174 editor={Herman Geuvers and Matthew England and Osman Hasan and Florian Rabe and Olaf Teschke},
 175 year={2017},
 176 url={http://metameso.org/~joe/papers/corneli2017towards.pdf},
 177 keywords={IATC}}
 178
 179 @inproceedings{martin2017bootstrapping,
 180 title={Bootstrapping the next generation of mathematical social machines},
 181 author={Ursula Martin and Alison Pease and Joseph Corneli},
 182 booktitle={Off the Beaten Track workshop at POPL, UPMC Paris, January 21, 2017},
 183 editor={Kuper, Lindsey and Atkey, Bob},
 184 year={2017},
 185 organization={\textbf{ACM}},
 186 url={http://popl17.sigplan.org/event/obt-2017-talk-5},
 187 keywords={IATC, social machines}}
 188
 189 @article{lamport1995write,
 190   title={How to write a proof},
 191   author={Lamport, Leslie},
 192   journal={The {A}merican {M}athematical {M}onthly},
 193   volume={102},
 194   number={7},
 195   pages={600--608},
 196   year={1995},
 197   publisher={JSTOR}
 198 }
 199
 200 @article{lamport2012write21st,
 201   title={How to write a 21st century proof},
 202   author={Lamport, Leslie},
 203   journal={Journal of fixed point theory and applications},
 204   volume={11},
 205   number={1},
 206   pages={43--63},
 207   year={2012},
 208   publisher={Springer}
 209 }
 210
 211 @book{lakatos1976proofs,
 212   title={Proofs and {Refutations}: {The} {Logic} of {Mathematical} {Discovery}},
 213   author={Lakatos, Imre},
 214   year={1976},
 215   publisher={Cambridge University Press}
 216 }
 217
 218 @article {Bundy20130194,
 219   author = {Bundy, Alan},
 220   title = {The interaction of representation and reasoning},
 221   volume = {469},
 222   number = {2157},
 223   year = {2013},
 224   doi = {10.1098/rspa.2013.0194},
 225   publisher = {The Royal Society},
 226   abstract = {Automated reasoning is an enabling technology for many applications of informatics. These applications include verifying that a computer program meets its specification; enabling a robot to form a plan to achieve a task and answering questions by combining information from diverse sources, e.g. on the Internet, etc. How is automated reasoning possible? Firstly, knowledge of a domain must be stored in a computer, usually in the form of logical formulae. This knowledge might, for instance, have been entered manually, retrieved from the Internet or perceived in the environment via sensors, such as cameras. Secondly, rules of inference are applied to old knowledge to derive new knowledge. Automated reasoning techniques have been adapted from logic, a branch of mathematics that was originally designed to formalize the reasoning of humans, especially mathematicians. My special interest is in the way that representation and reasoning interact. Successful reasoning is dependent on appropriate representation of both knowledge and successful methods of reasoning. Failures of reasoning can suggest changes of representation. This process of representational change can also be automated. We will illustrate the automation of representational change by drawing on recent work in my research group.},
 227   issn = {1364-5021},
 228   URL = {http://rspa.royalsocietypublishing.org/content/469/2157/20130194},
 229   eprint = {http://rspa.royalsocietypublishing.org/content/469/2157/20130194.full.pdf},
 230   journal = {Proceedings of the Royal Society of London A: Mathematical, Physical and Engineering Sciences}
 231 }
 232
 233 @inproceedings{sussman2005programming,
 234   title={Why programming is a good medium for expressing poorly understood and sloppily formulated ideas},
 235   author={Sussman, Gerald Jay},
 236   booktitle={{OOPSLA} '05: {C}ompanion to the 20th annual {ACM} {SIGPLAN} conference on {O}bject-oriented programming, systems, languages, and applications},
 237   pages={6--6},
 238   year={2005},
 239   organization={ACM}
 240 }
 241
 242 @article{mccarthy2008well,
 243   title={The well-designed child},
 244   author={McCarthy, John},
 245   journal={Artificial Intelligence},
 246   volume={172},
 247   number={18},
 248   pages={2003--2014},
 249   year={2008},
 250   publisher={Elsevier}
 251 }
 252
 253 @inproceedings{sussman2011programming,
 254   title={We {Really} {Don't} {Know} {How} {To} {Compute!}},
 255   author={Sussman, Gerald Jay},
 256   booktitle={Strange Loop},
 257   year={2011},
 258   url={https://www.infoq.com/presentations/We-Really-Dont-Know-How-To-Compute},
 259   abstract={Though we have been building and programming computing machines for about 60 years and have learned a great deal about composition and abstraction, we have just begun to scratch the surface. A mammalian neuron takes about ten milliseconds to respond to a stimulus. A driver can respond to a visual stimulus in a few hundred milliseconds, and decide an action, such as making a turn. So the computational depth of this behavior is only a few tens of steps. We don't know how to make such a machine, and we wouldn't know how to program it. The human genome -- the information required to build a human from a single, undifferentiated eukariotic cell -- is about 1GB. The instructions to build a mammal are written in very dense code, and the program is extremely flexible. Only small patches to the human genome are required to build a cow or a dog rather than a human. Bigger patches result in a frog or a snake. We don't have any idea how to make a description of such a complex machine that is both dense and flexible. New design principles and new linguistic support are needed. I will address this issue and show some ideas that can perhaps get us to the next phase of engineering design.},
 260 }
 261
 262 @techreport{gabi-iatc,
 263   title={Extending {Inference} {Anchoring} {Theory} for use with mathematical argumentation},
 264   author={Rino Nesin, Gabriela},
 265   institution={University of Edinburgh},
 266   year={2016}}
 267
 268 @book{mercier2017enigma,
 269   title={The enigma of reason},
 270   author={Mercier, Hugo and Sperber, Dan},
 271   year={2017},
 272   publisher={Harvard University Press}
 273 }
 274
 275 @article{moshman2004inference,
 276   title={From inference to reasoning: {The} construction of rationality},
 277   author={Moshman, David},
 278   journal={Thinking \& Reasoning},
 279   volume={10},
 280   number={2},
 281   pages={221--239},
 282   year={2004},
 283   publisher={Taylor \& Francis}
 284 }
 285
 286 @inproceedings{gabriel2000mob,
 287   title={Mob software: {The} erotic life of code},
 288   author={Gabriel, Richard P and Goldman, Ron},
 289   booktitle={Proc. {A}{C}{M} {C}onf. {O}bject-{O}riented {P}rogramming, {S}ystems, {L}anguages, and {A}pplications},
 290   year={2000}
 291 }
 292
 293 @article{lamport1994temporal,
 294   title={The temporal logic of actions},
 295   author={Lamport, Leslie},
 296   journal={ACM Transactions on Programming Languages and Systems (TOPLAS)},
 297   volume={16},
 298   number={3},
 299   pages={872--923},
 300   year={1994},
 301   publisher={ACM}
 302 }
 303
 304 @article{lamport1999specifying,
 305   title={Specifying {Concurrent} {Systems} with {TLA}{$^{+}$}},
 306   author={Lamport, Leslie},
 307   journal={NATO Science Series, III: Computer and Systems Sciences},
 308   volume={173},
 309   pages={183--247},
 310   year={1999},
 311   publisher={IOS Press},
 312   number={173},
 313   series={Calculational System Design},
 314   place={Amsterdam}
 315 }
 316
 317 @article{lamport2014tla2,
 318   title={{TLA}$^{+2}$: {A} {Preliminary} {Guide}},
 319   author={Lamport, Leslie},
 320   url={http://lamport.azurewebsites.net/tla/tla2-guide.pdf},
 321   year={2014},
 322 }
 323
 324 @article{alexander1964city,
 325   title={A city is not a tree},
 326   author={Alexander, Christopher},
 327   journal={Architectural Forum},
 328   volume={122},
 329   number={1},
 330   year={1965},
 331   month={April},
 332   pages={58--62},
 333 }
 334
 335 @book{alexander2012battle,
 336   title={The battle for the life and beauty of the earth: a struggle between two world-systems},
 337   author={Alexander, Christopher and Neis, Hans Joachim and Alexander, Maggie Moore},
 338   year={2012},
 339   publisher={Oxford University Press}
 340 }
 341
 342 @inproceedings{gucklesberger2017addressing,
 343 author={Christian Guckelsberger and Christoph Salge and Simon Colton},
 344 title={{Addressing} the {``}{Why?}{''} in {Computational} {Creativity}: {A} {Non-Anthropocentric}, {Minimal} {Model} of {Intentional} {Creative} {Agency}},
 345 editor={Goel, Ashok and Jordanous, Anna and Pease, Alison and Jacob, Mikhail and Guzdial, Matthew},
 346 booktitle={Proceedings of the Eighth International Conference on Computational Creativity, ICCC 2017},
 347 year={2017},
 348 url={http://computationalcreativity.net/iccc2017/ICCC_17_accepted_submissions/ICCC-17_paper_37.pdf}
 349 }
 350
 351 @inproceedings{veale2017dejavu,
 352 author={Tony Veale},
 353 title={D{\'e}j{\`a} {Vu} {All} {Over} {Again}: {On} the {Creative} {Value} of {Familiar} {Elements} in the {Telling} of {Original} {Tales}},
 354 editor={Goel, Ashok and Jordanous, Anna and Pease, Alison and Jacob, Mikhail and Guzdial, Matthew},
 355 booktitle={Proceedings of the Eighth International Conference on Computational Creativity, ICCC 2017},
 356 year={2017},
 357 url={http://computationalcreativity.net/iccc2017/ICCC_17_accepted_submissions/ICCC-17_paper_11.pdf}
 358 }
 359
 360 @inproceedings{martin1999computers,
 361   title={Computers, reasoning and mathematical practice},
 362   author={Martin, U.},
 363   booktitle={{Computational} {Logic}: {Proceedings} of the {NATO} {Advanced} {Study} {Institute} on {Computational} {Logic}},
 364   pages={301--346},
 365   editor={Ulrich Berger and Helmut Schwichtenberg},
 366   year={1999},
 367   organization={Springer},
 368   note={Held in Marktoberdorf, Germany, July 29 – August 10, 1997.}
 369 }
 370
 371 @book{hilbert1992natur,
 372   title={Natur und mathematisches Erkennen: Vorlesungen, gehalten 1919-1920 in G{\"o}ttingen},
 373   author={Hilbert, David},
 374   year={[1919] 1992},
 375   publisher={Birkh{\"a}user}
 376 }
 377
 378 @article{corry1997origins,
 379   title={The origins of eternal truth in modern mathematics: {Hilbert} to {Bourbaki} and beyond},
 380   author={Corry, Leo},
 381   journal={Science in Context},
 382   volume={10},
 383   number={02},
 384   pages={253--296},
 385   year={1997},
 386   publisher={Cambridge Univ Press}
 387 }
 388
 389 @misc(gowers-massively,
 390     author={Gowers, Timothy},
 391     title={Is massively collaborative mathematics possible?},
 392     howpublished={\url{http://gowers.wordpress.com/is-massively-collaborative-mathematics-possible/}},
 393     note = {Accessed: 2017-05-30}
 394 )
 395
 396
 397
 398 @Article{Ganesalingam2016,
 399 author="Ganesalingam, M.
 400 and Gowers, W. T.",
 401 title="A Fully Automatic Theorem Prover with Human-Style Output",
 402 journal="Journal of Automated Reasoning",
 403 year="2016",
 404 pages="1--39",
 405 abstract="This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians.",
 406 issn="1573-0670",
 407 doi="10.1007/s10817-016-9377-1",
 408 url="http://dx.doi.org/10.1007/s10817-016-9377-1"
 409 }
 410
 411 @article{gowers2009massively,
 412   title={Massively collaborative mathematics},
 413   author={Gowers, W.T. and Nielsen, M.},
 414   journal={Nature},
 415   volume={461},
 416   number={7266},
 417   pages={879--881},
 418   year={2009},
 419   publisher={Nature Publishing Group}
 420 }
 421
 422 @misc{gowers-talk,
 423  author={Gowers, W.T. and Ganesalingam, M.},
 424  title={Modelling the mathematical discovery process},
 425  note={Maxwell Institute Lecture, Fri, November 2, 4pm -- 5pm, James Clerk Maxwell Building, University of Edinburgh},
 426  year={2012},
 427 }
 428
 429 @techreport{schank-and-birnbaum,
 430   title={Memory, meaning, and syntax},
 431   author={Schank, R. and Birnbaum, L},
 432   institution={Department of Computer Science, Yale University},
 433   number={189},
 434   year={1980}}
 435
 436 @article{ehrig1992introduction,
 437   title={Introduction to graph grammars with applications to semantic networks},
 438   author={Ehrig, Hartmut and Habel, Annegret and Kreowski, Hans-J{\"o}rg},
 439   journal={Computers \& Mathematics with Applications},
 440   volume={23},
 441   number={6-9},
 442   pages={557--572},
 443   year={1992},
 444   publisher={Elsevier}
 445 }
 446
 447 @mastersthesis{ginev2011structure,
 448   title={The structure of mathematical expressions},
 449   author={Ginev, Deyan},
 450   year={2011},
 451   school={Jacobs University},
 452   address={Bremen, Germany}
 453 }
 454
 455 @article{godel1994qed,
 456   title={The {QED} {Manifesto}},
 457   author={Anonymous},
 458   journal={Lecture Notes in Artificial Intelligence},
 459   volume={814},
 460   pages={238--251},
 461   year={1994}
 462 }
 463
 464 @article{scott1993type,
 465   title={A type-theoretical alternative to {ISWIM}, {CUCH}, {OWHY}},
 466   author={Scott, Dana S},
 467   journal={Theoretical Computer Science},
 468   volume={121},
 469   number={1-2},
 470   pages={411--440},
 471   year={1993},
 472   publisher={Elsevier}
 473 }
 474
 475 @article{tarski1986logical,
 476   title={What are logical notions?},
 477   author={Tarski, Alfred and Corcoran, John},
 478   journal={History and philosophy of logic},
 479   volume={7},
 480   number={2},
 481   pages={143--154},
 482   year={1986},
 483   publisher={Taylor \& Francis}
 484 }
 485
 486 @book{alexander1977pattern,
 487   title={{A} {P}attern {L}anguage: {T}owns, {B}uildings, {C}onstruction},
 488   author={Alexander, Christopher and Ishikawa, Sara and Silverstein, Murray},
 489   year={1977},
 490   series={Center for Environmental Structure Series},
 491   publisher={Oxford University Press},
 492   address={Oxford}
 493 }
 494
 495 @book{alexander1964notes,
 496   title={Notes on the Synthesis of Form},
 497   author={Alexander, Christopher},
 498   volume={5},
 499   year={1964},
 500   publisher={Harvard University Press}
 501 }
 502
 503 @article{halmos1970write,
 504   title={How to write mathematics},
 505   author={Halmos, Paul R},
 506   journal={Enseign. Math},
 507   volume={16},
 508   number={2},
 509   pages={123--152},
 510   year={1970}
 511 }
 512
 513 @article{william1994proof,
 514   title={On proof and progress in mathematics},
 515   author={Thurston, William},
 516   journal={Bull. Amer. Math. Soc.(NS)},
 517   volume={30},
 518   pages={161--177},
 519   year={1994}
 520 }
 521
 522 @article{thurston-math-ed,
 523 title={Mathematical education},
 524 author={Thurston, W.P.},
 525 journal={Notices of the AMS},
 526 volume={37},
 527 number={7},
 528 year={1990},
 529 pages={844--850}
 530 }
 531
 532 @article{simon1958heuristic,
 533   title={Heuristic problem solving: The next advance in operations research},
 534   author={Simon, Herbert A and Newell, Allen},
 535   journal={Operations research},
 536   volume={6},
 537   number={1},
 538   pages={1--10},
 539   year={1958},
 540   publisher={INFORMS}
 541 }
 542
 543
 544 @article{sloman2008well,
 545   title={The well-designed young mathematician},
 546   author={Sloman, Aaron},
 547   journal={Artificial Intelligence},
 548   volume={172},
 549   number={18},
 550   pages={2015--2034},
 551   year={2008},
 552   publisher={Elsevier}
 553 }
 554
 555
 556 @article{wiedijk2007qed,
 557   title={The {QED} manifesto revisited},
 558   author={Wiedijk, Freek},
 559   journal={Studies in Logic, Grammar and Rhetoric},
 560   volume={10},
 561   number={23},
 562   pages={121--133},
 563   year={2007}
 564 }
 565
 566 @article{harrison2016preface,
 567   title={Preface: Twenty Years of the {QED} Manifesto},
 568   author={Harrison, John and Urban, Josef and Wiedijk, Freek},
 569   journal={Journal of Formalized Reasoning},
 570   volume={9},
 571   number={1},
 572   pages={1--2},
 573   year={2016}
 574 }
 575
 576 @book{peirce-diagrammatic,
 577   title={The New Elements of Mathematics},
 578   author={Peirce, Charles S.},
 579   volume={4},
 580   publisher={Mouton},
 581   place={The Hague, Netherlands},
 582   year={1976}}
 583
 584 @article{DBLP:journals/corr/KaliszykCS17,
 585   author    = {Cezary Kaliszyk and
 586                Fran{\c{c}}ois Chollet and
 587                Christian Szegedy},
 588   title     = {HolStep: {A} Machine Learning Dataset for Higher-order Logic Theorem
 589                Proving},
 590   journal   = {CoRR},
 591   volume    = {abs/1703.00426},
 592   year      = {2017},
 593   url       = {http://arxiv.org/abs/1703.00426},
 594   timestamp = {Mon, 03 Apr 2017 12:41:34 +0200},
 595   biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/KaliszykCS17},
 596   bibsource = {dblp computer science bibliography, http://dblp.org}
 597 }
 598
 599
 600 @article{DBLP:journals/corr/LoosISK17,
 601   author    = {Sarah M. Loos and
 602                Geoffrey Irving and
 603                Christian Szegedy and
 604                Cezary Kaliszyk},
 605   title     = {Deep Network Guided Proof Search},
 606   journal   = {CoRR},
 607   volume    = {abs/1701.06972},
 608   year      = {2017},
 609   url       = {http://arxiv.org/abs/1701.06972},
 610   timestamp = {Wed, 01 Feb 2017 17:47:56 +0100},
 611   biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/LoosISK17},
 612   bibsource = {dblp computer science bibliography, http://dblp.org}
 613 }
 614
 615
 616 @book{ganesalingam2013language,
 617   title={The {Language} of {Mathematics}, {A} {Linguistic} and {Philosophical} {Investigation}},
 618   author={Ganesalingam, Mohan},
 619   series={LNCS},
 620   volume={7805},
 621   year={2013},
 622   publisher={Springer Verlag}
 623 }
 624
 625 @inproceedings{cramer2011parsing,
 626   title={Parsing and disambiguation of symbolic mathematics in the Naproche system},
 627   author={Cramer, Marcos and Koepke, Peter and Schr{\"o}der, Bernhard},
 628   booktitle={International Conference on Intelligent Computer Mathematics},
 629   pages={180--195},
 630   year={2011},
 631   organization={Springer}
 632 }
 633
 634 @inproceedings{cramer2010presupposition,
 635   title={Presupposition Projection and Accommodation in Mathematical Texts.},
 636   author={Cramer, Marcos and K{\"u}hlwein, Daniel and Schr{\"o}der, Bernhard},
 637   booktitle={KONVENS},
 638   pages={29--36},
 639   year={2010}
 640 }
 641
 642 @incollection{gowers2000two,
 643   title={The two cultures of mathematics},
 644   author={Gowers, William Timothy},
 645   booktitle={Mathematics: Frontiers and Perspectives},
 646   editor={V. Arnold and others},
 647   pages={65--78},
 648   year={2000},
 649   publisher={American Mathematics Society}
 650 }
 651
 652
 653 @book{gabriel1996patterns,
 654   title={Patterns of software},
 655   author={Gabriel, Richard P},
 656   year={1996},
 657   publisher={Oxford University Press},
 658   place={New York}
 659 }
 660
 661 @phdthesis{grimm2013implementation,
 662   title={Implementation of bourbaki's elements of mathematics in coq: part one, theory of sets},
 663   author={Grimm, Jos{\'e}},
 664   year={2013},
 665   journal={research report RR-6999, INRIA. 2013, pp.205},
 666   school={INRIA}
 667 }
 668
 669 @article{grimm2009implementation,
 670   title={Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers},
 671   author={Grimm, Jos{\'e}},
 672   journal={Research Report RR-7150, INRIA},
 673   year={2009}
 674 }
 675
 676 @phdthesis{grimm2015implementation,
 677   title={Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers},
 678   author={Grimm, Jos{\'e}},
 679   year={2015},
 680   school={Inria Sophia Antipolis; INRIA}
 681 }
 682
 683
 684 @article{mccarthy1960recursive,
 685   title={Recursive functions of symbolic expressions and their computation by machine, {Part} {I}},
 686   author={McCarthy, John},
 687   journal={Communications of the ACM},
 688   volume={3},
 689   number={4},
 690   pages={184--195},
 691   year={1960},
 692   publisher={ACM}
 693 }