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, L.},
 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{gucklesberger2016addressing,
 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{martin1999computers,
 352   title={Computers, reasoning and mathematical practice},
 353   author={Martin, U.},
 354   booktitle={{Computational} {Logic}: {Proceedings} of the {NATO} {Advanced} {Study} {Institute} on {Computational} {Logic}},
 355   pages={301--346},
 356   editor={Ulrich Berger and Helmut Schwichtenberg},
 357   year={1999},
 358   organization={Springer},
 359   note={Held in Marktoberdorf, Germany, July 29 – August 10, 1997.}
 360 }
 361
 362 @book{hilbert1992natur,
 363   title={Natur und mathematisches Erkennen: Vorlesungen, gehalten 1919-1920 in G{\"o}ttingen},
 364   author={Hilbert, David},
 365   year={[1919] 1992},
 366   publisher={Birkh{\"a}user}
 367 }
 368
 369 @article{corry1997origins,
 370   title={The origins of eternal truth in modern mathematics: {Hilbert} to {Bourbaki} and beyond},
 371   author={Corry, Leo},
 372   journal={Science in Context},
 373   volume={10},
 374   number={02},
 375   pages={253--296},
 376   year={1997},
 377   publisher={Cambridge Univ Press}
 378 }
 379
 380 @misc(gowers-massively,
 381     author={Gowers, Timothy},
 382     title={Is massively collaborative mathematics possible?},
 383     howpublished={\url{http://gowers.wordpress.com/is-massively-collaborative-mathematics-possible/}},
 384     note = {Accessed: 2017-05-30}
 385 )
 386
 387
 388 @Article{Ganesalingam2016,
 389 author="Ganesalingam, M.
 390 and Gowers, W. T.",
 391 title="A Fully Automatic Theorem Prover with Human-Style Output",
 392 journal="Journal of Automated Reasoning",
 393 year="2016",
 394 pages="1--39",
 395 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.",
 396 issn="1573-0670",
 397 doi="10.1007/s10817-016-9377-1",
 398 url="http://dx.doi.org/10.1007/s10817-016-9377-1"
 399 }
 400
 401 @article{gowers2009massively,
 402   title={Massively collaborative mathematics},
 403   author={Gowers, W.T. and Nielsen, M.},
 404   journal={Nature},
 405   volume={461},
 406   number={7266},
 407   pages={879--881},
 408   year={2009},
 409   publisher={Nature Publishing Group}
 410 }