kwarc.bib

@STRING{premessage = "This is the LaTeX preamble shared by all KWARC *.bib files.  "}



@README{--README--,
  x = { In your publication list, the \selfedit command can be implemented, e.g., as follows:},
  x = { \newcommand{\selfedit}{\footnote{In the review process, submissions from chairs were specially handled by the General Chair.}} },
}

@PREAMBLE{
{\providecommand\seen{seen }
\providecommand\selfedit{}
\providecommand\webpageat{web page at }
\providecommand\homepageat{home page at }
\providecommand\projectpageat{project page at }
\providecommand\systempageat{system home page at }
\providecommand\svnrepoat{Subversion repository at }
\providecommand\January{January}
\providecommand\February{February}
\providecommand\Feb{February}
\providecommand\March{March}
\providecommand\April{April}
\providecommand\May{May}
\providecommand\June{June}
\providecommand\July{July}
\providecommand\August{August}
\providecommand\September{September}   
\providecommand\October{October}
\providecommand\November{November}
\providecommand\December{December}
\providecommand\AUSTRALIA{Australia}   
\providecommand\ROMANIA{Romania}
\providecommand\MEXICO{Mexico}
\providecommand\ITALY{Italy}
\providecommand\USA{USA}
\providecommand\IRELAND{Ireland}
\providecommand\HUNGARY{Hungary}
\providecommand\JAPAN{Japan}
\providecommand\CANADA{Canada}
\providecommand\SPAIN{Spain}
\providecommand\NETHERLANDS{Netherlands}
\providecommand\UK{UK}
\providecommand\SWEDEN{Sweden}
\providecommand\GERMANY{Germany}
\providecommand\openmath{OpenMath}
\providecommand\fc{forthcoming}
\providecommand\PROC{Proceedings}
\providecommand\omdoc{OMDoc}
\providecommand\activemath{ActiveMath} 
\hyphenation{Wiki-Sym}}}


@string{Epmessage = "Read the README please!!!!!!!!!!!!!!"}
@STRING{ai    = "Artificial Intelligence"}
@STRING{mcgh	 = "McGraw-Hill"}
@STRING{jair  = "Journal of Artificial Intelligence Research"}
@STRING{kauf     = "Morgan Kaufmann"} 
@STRING{wil      = "Wiley"}
@STRING{spring   = "Springer-Verlag"}
@STRING{JWS = {Web Semantics: Science, Services and Agents on the World Wide Web}}

@INPROCEEDINGS{SchSar:structurallogrel,
  author={C. {Schürmann} and J. {Sarnat}},
  booktitle={2008 23rd Annual IEEE Symposium on Logic in Computer Science},
  title={Structural Logical Relations},
  year={2008},
  pages={69-80},
  doi={10.1109/LICS.2008.44},
  url={https://core.ac.uk/download/pdf/189668382.pdf},
  urldate = {2020-01-26}}

@article{Goedel:zia32,
  journal = {Anzeiger der Akademie der Wissenschaften in Wien},
  pages = {65--66},
  volume = {69},
  year = {1932},
  author = {Kurt G{\"o}del},
  title = {Zum Intuitionistischen Aussagenkalk\"ul}
}
@book{HugCre:acml84,
  author = {G. E. Hughes and M. M. Cresswell},
  title = {A companion to Modal Logic},
  series = {University Paperbacks},
  publisher = {Methuen},
  year = {1984}}

@book{Stalnaker:c14,
  author = {Stalnaker, Robert},
  year = {2014},
  title = {Context},
  publisher = {Oxford University Press}}

@book{Saeed:s03,
  author = {Saeed, John I.},
  year = {2003},
  title = {Semantics},
  edition = {2nd},
  publisher = {Blackwell}}
  
@book{Portner:wimffs04,
  author = {Portner, Paul},
  year = {2004},
  title = {What is Meaning? Fundamentals of Formal Semantics},
  publisher = {Blackwell}}
  
@book{Kearns:s11,
  author = {Kearns, Kate},
  year = {2011},
  title = {Semantics},
  edition = {2nd},
  publisher = {Palgrave Macmillan}}
  
@book{Jackendoff:sac83,
  author = {Jackendoff, Ray},
  year = {1983},
  title = {Semantics and Cognition},
  publisher = {MIT Press}}
  
@book{Cruse:milisp11,
  author = {Cruse, Alan},
  year = {2011},
  title = {Meaning in Language: An Introduction to Semantics and Pragmatics},
  series = {Oxford Textbooks in Linguistics},
  publishers = {OUP}}
  
@book{Ariel:dp10,
  author = {Ariel, Mira},
  year = {2010},
  title = {Defining Pragmatics},
  series = {Research Surveys in Linguistics},
  publisher = {Cambridge University Press}}
  
@book{ZimSte:its13,
  author = {Zimmermann, Thomas Ede and Wolfgang Sternefeld},
  year = {2013},
  title = {Introduction to Semantics},
  publisher = {de Gruyter Mouton}}

@book{Riemer:is10,
  author = {Riemer, Nick},
  year = {2010},
  title = {Introducing Semantics},
  series = {Cambridge Introductions to Language and Linguistics},
  publisher = {Cambridge University Press}}
  
@book{Birner:itp13,
  author = {Birner, Betty J.},
  year = {2013},
  title = {Introduction to Pragmatics},
  publisher = {Wiley-Blackwell}}
  
@book{HurHeaSmi:sac07,
  author = {Hurford, James R. and Brendan Heasley and Michael B. Smith},
  year = {2007},
  title = {Semantics: A coursebook},
  edition = {2nd},
  publisher = {Cambridge University Press}}
  
@book{CanKemGre:siml,
  author = {Cann, Ronnie and Kempson, Ruth and Gregoromichelaki, Eleni},
  title = {Semantics -- An Introduction to Meaning in Language},
  publisher = {Cambridge University Press},
  year = {2009},
  isbn = {0521819628}}
  
@inproceedings{levesque2012winograd,
  title={The {Winograd} Schema Challenge},
  author={Levesque, Hector and Davis, Ernest and Morgenstern, Leora},
  booktitle={Thirteenth International Conference on the Principles of Knowledge Representation and Reasoning},
  year={2012}}

@online{standlone:ctan:on,
  author = {Martin Scharrer},
  title = {\texttt{standalone} -- Compile {\TeX} pictures stand-alone or as part of a document},
  url = {https://ctan.org/pkg/standalone},
  urldate = {2020-10-16}}
  
@online{LabelMe:on,
  label = {LM},
  title = {{LabelMe}: the open annotation tool},
  url = {http://labelme.csail.mit.edu},
  urldate = {2020-08-28}}
  
@online{lod-cloud:on,
  label = {LOD},
  title = {The Linked Open Data Cloud},
  url = {https://lod-cloud.net/},
  urldate = {2020-08-19}}
  
@online{glforthel:on,
  title = {{GLForTheL} -- Implementing ForTheL in GLF},
  label = {GLF},
  url = {https://gl.mathhub.info/comma/glforthel},
  urldate = {2020-08-06}}

@inproceedings{kofler2012dyngenpar,
  title = {DynGenPar--a dynamic generalized parser for common mathematical language},
  author = {Kofler, Kevin and Neumaier, Arnold},
  pages = {386--401},
  crossref = {CICM12}}

@online{OpenDataCommons:on,
  label = {ODC},
  title = {Open Data Commons -- Legal Tools For Open Data},
  url = {https://opendatacommons.org/},
  urldate = {2020-07-29}}

@online{geonames:on,
  label = {GN},
  title = {Geonames},
  url = {https://www.geonames.org/},
  urldate = {2020-07-29}}

@online{GND:on,
  label = {GND},
  title = {{DNB} -- The Integrated Authority File ({GND})}, 
  url = {https://www.dnb.de/EN/Professionell/Standardisierung/GND/gnd_node.html},
  urldate = {2020-07-29}}
  
@online{WissKI-Handbuck:on,
  label = {WH},
  title = {{WissKI} Handbuch},
  url = {http://wiss-ki.eu/documentation/wisski_handbuch},
  urldate = {2020-07-23}}
  
@book{Glaman:d8dc17,
  title = {Drupal 8 Development Cookbook -- Harness the power of Drupal 8 with this recipe-based practical guide},
  edition = {2},
  author = {Matt Glaman},
  publisher = {Packt Publishing},
  year = {2-17},
  isbn = {9781788290401}}

@book{Tomlinson:ed8d17,
  title = {Enterprise Drupal 8 Development -- For Advanced Projects and Large Development Teams},
  author = {Todd Tomlinson},
  publisher = {Apress},
  year = {2017},
  isbn = {9781484202548}}
  
@online{ECRM:on,
  label = {ECRM},
  url = {http://erlangen-crm.org/},
  title = {{Erlangen CRM/OWL} - An {OWL DL 1.0} implementation of the {CIDOC} Conceptual Reference Model ({CIDOC CRM})},
  urldate = {2020-07-13}}

@online{ECRM:github,
  label = {ECRM},
  url = {https://github.com/erlangen-crm},
  title = {erlangen-crm},
  urldate = {2020-07-13}}
  
@book{BovHeuKai:MiDas16,
  author = {Bove, Jens and Heusinger, Lutz and Kailus, Angela}, 
  title = {Marburger Informations-, Dokumentations- und Administrations-System (MIDAS): Handbuch und CD},
  doi = {10.11588/artdok.00003770},
  edition = {4},
  year = {2016},
  publisher = {K.G.Saur}}
  
@online{HiDa:on,
  label = {HiDa},
  url = {https://www.startext.de/produkte/hida},
  title = {HiDa},
  urldate = {2020-07-12}}
  
@online{spec:on,
  label = {SPEC},
  author = {{Kestrel Institute}},
  title = {The Specware System},
  url = {https://www.kestrel.edu/home/projects/specware/index.html},
  urldate = {2020-05-27}}


@inproceedings{mossakowski2007heterogeneous,
  title={The heterogeneous tool set, Hets},
  author={Mossakowski, Till and Maeder, Christian and L{\"u}ttich, Klaus},
  booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  pages={519--522},
  year={2007},
  organization={Springer}}

@online{phet:on,
  label = {PhET},
  author = {{University of Colorado}},
  title = {PhET Interactive Simulations},
  url = {https://phet.colorado.edu},
  urldate = {2020-05-27}}

@online{GFM:on,
  key = {GFM},
  url = {https://github.github.com/gfm/},
  title = {GitHub Flavored Markdown Spec},
  urldate = {2020-05-10}}
  
@phdthesis{Cramer:pcmticnl,
    author = {Cramer, Marcos},
    title = {Proof-checking mathematical texts in controlled natural language},
    school = {Rheinische Friedrich-Wilhelms-Universit\"at Bonn},
    year = {2013},
    language = {eng},
    URL = {http://hss.ulb.uni-bonn.de/2013/3390/3390.pdf}}

@article{NautyTraces,
title = "Practical graph isomorphism, II",
journal = "Journal of Symbolic Computation",
volume = "60",
pages = "94 - 112",
year = "2014",
issn = "0747-7171",
doi = "10.1016/j.jsc.2013.09.003",
url = "http://www.sciencedirect.com/science/article/pii/S0747717113001193",
author = "Brendan D. McKay and Adolfo Piperno"}

@inproceedings{tishkovsky2012mettel2,
  title={MetTeL2: Towards a Tableau Prover Generation Platform},
  author={Tishkovsky, Dmitry and Schmidt, Renate A and Khodadadi, Mohammad},
  booktitle={PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning},
  pages={149}}

@online{zenodo:on,
  label = {ZRS},
  title = {Zenodo -- Research. Shared.},
  url = {https://zenodo.org},
  urldate = {2020-04-03}}

@online{GDS:on,
  label = {DS},
  title = {Dataset Search},
  url = {https://datasetsearch.research.google.com/},
  urldate = {2020-01-25}}

@inproceedings{FucSchSch:ace98,
author = {Fuchs, Norbert E. and Schwertel, Uta and Schwitter, Rolf},
title = {Attempto Controlled English - Not Just Another Logic Specification Language},
year = {1998},
isbn = {3540657657},
publisher = {Springer-Verlag},
booktitle = {Proceedings of the 8th International Workshop on Logic Programming Synthesis and Transformation},
pages = {1–20},
numpages = {20},
series = {LOPSTR ’98}}

@software{URL:Unity2019.3.6,
  title = {Unity Realtime Development Platform},
  author = {{Unity Technologies}},
  version = {2019.3.6},
  urldate = {2020-03-19},
  url = {https://unity.com/},
  howpublished = {\url{https://unity.com/}}}

@misc{paskevich2007syntax,
  title={The syntax and semantics of the ForTheL language},
  author={Paskevich, Andrei},
  year={2007},
  publisher={Citeseer}}

@online{tobii-pro-x3-120,
  label = {TX3},
  title = {Tobii Pro X3–120 Eye Tracker -- Product Description},
  url = {https://www.tobiipro.com/siteassets/tobii-pro/product-descriptions/tobii-pro-x3-120-product-description.pdf},
  urldate = {2020-03-09}}
@inproceedings{ChoDasEad:esrqs05,
  title = {An Efficient {SQL}-based {RDF} Querying Scheme},
  author = {Eugene Inseok Chong and Souripriya Das and George Eadon and Jagannathan Srinivasan},
  booktitle = {Proceedings of the 31. VLDB Conference},
  year = {2005}}
  
@online{drill:on,
  label = {AD},
  title = {Apache Drill -- Schema-free SQL Query Engine for Hadoop, NoSQL and Cloud Storage},
  url = {https://drill.apache.org},
  urldate = {2020-03-02}}
  
@book{DoaHalIve:podi12,
  title = {Principles of Data Integration},
  author = {AnHai Doan and Alon Halevy and Zachary Ives},
  year = {2012},
  publisher = {Elsevier}}
  
@inproceedings{StaBakRei:vtamvmt18,
    title = "Variable Typing: Assigning Meaning to Variables in Mathematical Text",
    author = "Stathopoulos, Yiannos  and Baker, Simon  and Rei, Marek  and Teufel, Simone",
    booktitle = "NAACL 2018 Proceedings",
    year = "2018",
    publisher = "ACL",
    url = "https://www.aclweb.org/anthology/N18-1028",
    doi = "10.18653/v1/N18-1028",
    pages = "303--312",
    abstract = "Information about the meaning of mathematical variables in text is useful in NLP/IR tasks such as symbol disambiguation, topic modeling and mathematical information retrieval (MIR). We introduce \textit{variable typing}, the task of assigning one \textit{mathematical type} (multi-word technical terms referring to mathematical concepts) to each variable in a sentence of mathematical text. As part of this work, we also introduce a new annotated data set composed of 33,524 data points extracted from scientific documents published on arXiv. Our intrinsic evaluation demonstrates that our data set is sufficient to successfully train and evaluate current classifiers from three different model architectures. The best performing model is evaluated on an extrinsic task: MIR, by producing a \textit{typed formula index}. Our results show that the best performing MIR models make use of our typed index, compared to a formula index only containing raw symbols, thereby demonstrating the usefulness of variable typing."}

@inproceedings{StaTeu:mirbteqe16,
    title = "Mathematical Information Retrieval based on Type Embeddings and Query Expansion",
    author = "Stathopoulos, Yiannos  and Teufel, Simone",
    booktitle = "Proceedings of {COLING} 2016",
    year = "2016",
    publisher = "ACL",
    url = "https://www.aclweb.org/anthology/C16-1221",
    pages = "2344--2355",
    abstract = "We present an approach to mathematical information retrieval (MIR) that exploits a special kind of technical terminology, referred to as a mathematical type. In this paper, we present and evaluate a type detection mechanism and show its positive effect on the retrieval of research-level mathematics. Our best model, which performs query expansion with a type-aware embedding space, strongly outperforms standard IR models with state-of-the-art query expansion (vector space-based and language modelling-based), on a relatively new corpus of research-level queries."}

@book{Swanson:mit99,
  author = {Ellen Swanson},
  title = {Mathematics into Type},
  edition = {updated edition},
  url  = {https://www.ams.org/publications/authors/mit-2.pdf},
  publisher = {AMS}}

@online{breqn:on,
  title = {The breqn package},
  author = {Michael J. Downes and Morten H{\o}gholm and  Will Robertson},
  url = {http://mirrors.ctan.org/macros/latex/contrib/breqn/breqn.pdf},
  urldate = {2020-02-25}}
  
@online{Epic:ue4,
  label = {UE},
  author = {Epic Games Inc.},
  title = {{Unreal} {Engine} 4},
  urldate = {2020-02-27},
  url = {https://www.unrealengine.com/}}

@inproceedings{Deterding:FGDEGDG,
	author = {Deterding, Sebastian and Dixon, Dan and Khaled, Rilla and Nacke, Lennart},
	title = {From Game Design Elements to Gamefulness: Defining ``Gamification''},
	booktitle = {Proceedings of the 15th International Academic MindTrek Conference},
	series = {MindTrek '11},
	year = {2011},
	isbn = {978-1-4503-0816-8},
	pages = {9--15},
	numpages = {7},
	doi = {10.1145/2181037.2181040},
	acmid = {2181040},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {alternate reality games, game-based technologies, gameful design, gamefulness, games, gamification, pervasive games, play, playful design, playfulness, serious games}}

@online{FABstracts:on,
  label = {FA},
  title = {Formal Abstracts},
  url = {https://formalabstracts.github.io/},
  urldate = {2020-02-15}}
  
@online{coq-opam,
  title = {{OPAM} archive for {Coq}},
  label = {COA},
  url = {https://github.com/coq/opam-coq-archive},
  urldate = {2020-02-12}}
  
@online{HOLLight-Library:on,
  label = {HLL},
  url = {https://github.com/jrh13/hol-light/tree/master/Library},
  title = {{HOL Light} Library},
  urldate = {2020-02-07}}
  
@online{ETC:on,
  label = {ETC},
  title = {Encyclopedia of Triangle Centers -- {ETC}},
  url = {https://faculty.evansville.edu/ck6/encyclopedia/ETC.html},
  urldate = {2020-02-07}}
  
@inproceedings{Israel:tviods93,
  author = {David J. Israel},
  title = {The Very Idea of Dynamic Semantics},
  booktitle = {Proceedings of the Ninth Amsterdam Colloquium},
  year = {1993},
  url = {https://arxiv.org/pdf/cmp-lg/9406026.pdf}}
  
@InProceedings{AspSacTasZac:capa06,
  title =	"{Crafting a Proof Assistant}",
  author =	"A. Asperti and C. Sacerdoti Coen and E. Tassi and S. Zacchiroli",
  publisher =	"Springer",
  year = 	2006,
  booktitle =	"TYPES",
  editor =	"T. Altenkirch and C. McBride",
  pages =	"18--32"}

@online{octave:on,
  label = {GU},
  title = {GNU Octave},
  url = {https://gnu.org/software/octave/},
  urldate = {2020-01-20}}

@online{simulink:on,
  label = {MS},
  title = {Simulation and Model-Based Design -- {MatLab} \& {Simulink}},
  url = {https://www.mathworks.com/products/simulink.html},
  urldate = {2020-01-20}}

@online{R:on,
  title = {The {R} Project for Statistical Computing},
  label = {R},
  url = {https://r-project.org},
  urldate = {2020-01-20}}

@online{stan:on,
  title = {Stan},
  label = {Stan},
  url = {https://mc-stan.org/},
  urldate = {2020-01-20}}

@article{Quinlan:lldfr90,
 author = {J. Ross Quinlan},
 title = {Learning Logical Definitions from Relations},
 journal = {Machine Learning},
 volume = {5},
 number = {3},
 year = {1990},
 pages = {239--266}}
 
@online{MGP:on,
  label = {MGP},
  title = {The Mathematics Genealogy Project},
  url = {https://genealogy.math.ndsu.nodak.edu/},
  urldate = {2020-01-20}}
  
@online{Royle:list:on,
  label = {MO},
  title = {What are some early examples of creation of lists / catalogues of (particularly) combinatorial objects? -- MathOverflow},
  author = {Gordon Royle},
  url = {https://mathoverflow.net/questions/47044/what-are-some-early-examples-of-creation-of-lists-catalogues-of-particularly},
  urldate = {2020-01-09}}
  
  
@misc{Abdulaziz:plimpton10,
  title = {The Plimpton 322 Tablet and the Babylonian Method of Generating Pythagorean Triples},
  author = {Abdulaziz, Abdulrahman Ali},
  year = {2010},
  eprint={1004.0025},
  archivePrefix={arXiv}}
  
@inproceedings{GorNgu:atrmlab08,
  author = {Gore, R. and Nguyen, L.},
  year = {2008},
  title = {Analytic cut-free Tableaux for regular modal logics of agent beliefs},
  editor = {F. Sadri and K. Satoh},
  booktitle = {Computational Logic in Multi-Agent Systems},
  publisher = {Springer},
  pages = {268--287}}

@online{w3c:css-allspecs:on,
  label = {CSS},
  title = {All {CSS} Specifications},
  url = {https://www.w3.org/Style/CSS/specs.en.html},
  urldate = {2020-01-12}}
  
@online{lxml:on,
  label = {LXML},
  title = {lxml -- {XML} and {HTML} with Python},
  url = {https://lxml.de},
  urldate = {2019-12-09}}

@online{lxml:API:on,
  label = {LXML},
  title = {lxml API},
  url = {https://lxml.de/api/},
  urldate = {2019-12-09}}

@online{lxml:tutorial:on,
  label = {LXML},
  title = {The lxml.etree Tutorial},
  url = {https://lxml.de/tutorial.html},
  urldate = {2019-12-09}}

@online{OBO:on,
  label = {OBO},
  title = {The OBO Foundry},
  url = {http://www.obofoundry.org/},
  urldate = {2019-12-13}}

@incollection{KamWelZen:cmt14,
  title = {Computerising Mathematical Text},
  author = {Fairouz Kamareddine and  Joe Wells and Christoph Zengler and Henk Barendregt},
  pages = {343--396},
  crossref = {GabSieWoo:cl14}}
  
@techreport{OOXML:spec:on,
  label = {OOXML},
  title = {Standard {ECMA-376} - {Office Open XML File Formats}},
  url = {http://www.ecma-international.org/publications/standards/Ecma-376.htm},
  year = {2006}}
  
@online{writer2xhtml:on,
  label = {W2X},
  title = {Writer2xhtml -- Apache OpenOffice Extensions},
  urldate = {2019-12-01},
  url = {https://extensions.openoffice.org/fr/project/writer2xhtml}}

@online{mit-ocw:line-drawings,
  label = {ILD},
  url = {https://www.youtube.com/watch?v=l-tzjenXrvI&t=2037s},
  title = {7. Constraints: Interpreting Line Drawings},
  urldate = {2019-11-19}}

@online{SWIPL-manual:on,
  label = {SWI},
  title = {{SWI Prolog} Reference Manual},
  url = {https://www.swi-prolog.org/pldoc/refman/},
  urldate = {2019-10-10}}
  
@online{LPN:on,
  label = {LPN},
  title = {Learn Prolog Now!},
  url = {http://lpn.swi-prolog.org/},
  urldate = {2019-10-10}}

@book{Flach:SL94,
  author = {Peter Flach},
  publisher = {Wiley},
  year = {1994},
  isbn = {0471 94152 2},
  url = {https://github.com/simply-logical/simply-logical/releases/download/v1.0/SL.pdf}}
  
@online{Fisher:pt:on,
  title = {prolog :- tutorial},
  author = {John R. Fisher},
  url = {https://www.cpp.edu/~jrfisher/www/prolog_tutorial/},
  urldate = {2019-10-10}}
  
@misc{TasMah:mc:url,crossref={TasMah:mc:base},
 howpublished = {\url{https://math-comp.github.io/mcb/book.pdf}}}
@online{TasMah:mc,crossref={TasMah:mc:base},
 urldate =  {2018-12-18}}
@misc{TasMah:mc:base,
 author = {Assia Mahboubi and Enrico Tassi},
 title =  {Mathematical Components},
 url = {https://math-comp.github.io/mcb/book.pdf},
 note = {online book}}

@online{NorKueRob:lcprs18,
  title = {Lecture capture: Practical recommendations for students and lecturers},
  url = {https://osf.io/huydx/download},
  year = {2018},
  author = {Emily Nordmann and Kuepper-Tetzel, Carolina E. and Louise Robson and Stuart Phillipson and Gabi Lipan
 and Peter McGeorge}}

@online{NorKueRob:vnas18,
  url = {https://osf.io/e6r7a/download},
  title = {Vorlesungsaufzeichnungen nutzen: Eine Anleitung für Studierende},
  year = {2018},
  author = {Emily Nordmann and Kuepper-Tetzel, Carolina E. and Louise Robson and Stuart Phillipson and Gabi Lipan
 and Peter McGeorge}}

 
@techreport{PROV:W3C0,
  url = {https://www.w3.org/TR/prov-overview/},
  date = {2013-04-30},
  title = {{PROV-Overview} -- An Overview of the PROV Family of Documents},
  author = {Paul Groth and Luc Moreau},
  institution = {World Wide Web Consortium ({W3C})},
  type = {{W3C} Recommendation}}
  
@online{OMG:on,
  label = {OMG},
  title = {OMG - Object Management Group},
  url = {https://www.omg.org/},
  urldate = {2019-10-06}}
  
@TechReport{CommonLogic:ISO,
  url = {http://iso-commonlogic.org},
  label = {CL},
  title = {Information technology --- {Common Logic} ({CL}): a framework for a family of logic-based languages},
  institution = {ISO/IEC},
  number = {24707:2007},
  year = 2007}

@techreport{DOL:OMG,
  label = {DOL},
  title = {Distributed Ontology, Model, and Specification Language Specification Version 1.0},
  url = {https://www.omg.org/spec/DOL/1.0/PDF},
  type = {OMG Specification},
  year = {2018},
  institution = {Object Management Group}}
  
  
@online{django:on,
  label = {DJ},
  title = {Django -- the Web Framework for Perfectionists with Deadlines},
  url= {https://www.djangoproject.com/},
  urldate = {2019-08-29}}

@inproceedings{Wenzel:2014:ITP-PIDE,
  author    = {Makarius Wenzel},
  title     = {Asynchronous User Interaction and Tool Integration in {Isabelle/PIDE}},
  booktitle = {Interactive Theorem Proving (ITP 2014)},
  editor    = {Gerwin Klein and Ruben Gamboa},
  year      = {2014},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {8558}}

@InCollection{pitts93,
  author =       {A. Pitts},
  title =        {The {HOL} Logic},
  editor =       {M. J. C. Gordon and T. F. Melham},
  booktitle  =   {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
  pages =        {191--232},
  publisher	= {Cambridge University Press},
  year		= 1993}

@InProceedings{Nipkow-Prehofer:1993,
  author =       {T. Nipkow and C. Prehofer},
  title =        {Type checking type classes},
  booktitle =    {ACM Symp.\ Principles of Programming Languages},
  year =         {1993}}

@inproceedings{Wenzel:2019:MKM,
  author = {Makarius Wenzel},
  url = {https://arxiv.org/abs/1905.01735},
  title = {Interaction with Formal Mathematical Documents in {Isabelle/PIDE}},
  pages = {1--15},
  crossref = {CICM19}}

@TechReport{Gordon:1985:HOL,
  author =       {M. J. C. Gordon},
  title =        {{HOL}: A machine oriented formulation of higher order logic},
  institution =  {University of Cambridge Computer Laboratory},
  year =         1985,
  number =       68}

@online{ISO:MathML3,
  label = {ISO},
  title = {ISO/IEC 40314:2016(en) Information technology — Mathematical Markup Language (MathML) Version 3.0 2nd Edition},
  url = {https://www.iso.org/obp/ui/#iso:std:iso-iec:40314:ed-1:v1:en},
  urldate = {2019-08-04}}

@book{Kahnemann:tfs11,
 author = {Kahneman, Daniel},
 year = {2011},
 title = {Thinking, fast and slow},
 publisher = {Penguin Books},
 isbn = {9780141033570}}
 
@incollection{Hayes:snpm90,
 author = {Hayes, Patrick J.},
 chapter = {The Second Naive Physics Manifesto},
 title = {Readings in Qualitative Reasoning About Physical Systems},
 editor = {Weld, Daniel S. and Kleer, Johan de},
 year = {1990},
 isbn = {1-55860-095-7},
 pages = {46--63},
 numpages = {18},
 url = {http://dl.acm.org/citation.cfm?id=93913.93941},
 acmid = {93941},
 publisher = {Morgan Kaufmann}}

@incollection{Suppes:wiast67,
  author = {Patrick Suppes},
  editor = {Sidney Morgenbesser},
  booktitle = {Philosophy of Science Today},
  year = {1967},
  publisher = {Basic Books Inc.},
  pages = {55--67}}
  
@article{SidTah:fagosh16,
 author = {Siddique, Umair and Tahar, Sofi\&\#232;ne},
 title = {On the Formal Analysis of Gaussian Optical Systems in HOL},
 journal = {Formal Aspects of Computation},
 issue_date = {September 2016},
 volume = {28},
 number = {5},
 month = sep,
 year = {2016},
 issn = {0934-5043},
 pages = {881--907},
 numpages = {27},
 doi = {10.1007/s00165-016-0367-1},
 acmid = {2990408},
 publisher = {Springer-Verlag}} 

@article{google:neuralmath,
  author    = {David Saxton and
               Edward Grefenstette and
               Felix Hill and
               Pushmeet Kohli},
  title     = {Analysing Mathematical Reasoning Abilities of Neural Models},
  journal   = {CoRR},
  volume    = {abs/1904.01557},
  year      = {2019},
  url       = {http://arxiv.org/abs/1904.01557},
  archivePrefix = {arXiv},
  eprint    = {1904.01557},
  timestamp = {Wed, 24 Apr 2019 12:21:25 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1904-01557},
  bibsource = {dblp computer science bibliography, https://dblp.org}}

@online{google:neuralmathfail:on,
  url = {https://www.zdnet.com/article/ai-aint-no-a-student-deepmind-flunks-high-school-math/},
  title = {AI ain't no A student: DeepMind nearly flunks high school math},
  urldate = {2019-06-04}}

@InProceedings{Bibel:ehpad07,
  author =      {Wolfgang Bibel},
  title =      {Early History and Perspectives of Automated Deduction},
  booktitle =     {Proceedings of the 30th Annual German Conference on Artificial Intelligence (KI-2007)},
  pages =     {2--18},
  year =     2007,
  editor =     {J. Hertzberg and M. Beetz and R. Englert},
  volume =     4667,
  series =     {LNAI},
  address =     {Berlin},
  publisher =     {Springer}}

@Book{BibFur:ffkiitum18,
  author =     {Wolfgang Bibel and Ulrich Furbach},
  title =      {Formierung eines Forschungsgebiets -- K{\"u}nstliche Intelligenz und Intellektik an der Technischen Universit{\"a}t M{\"u}nchen},
  publisher =      {Deutsches Museum Verlag},
  year =      2018,
  series =     {Preprint 21},
  address =     {M{\"u}nchen},
  url = {https://www.deutsches-museum.de/verlag/aus-der-forschung/preprint/}}

@Book{GabHogRob:1,
  title =     "Handbook of Logic in Artificial Intelligence and Logic Programming",
  publisher =     "Oxford University Press",
  year =     "1991",
  editor =     "Dov Gabbay and Chris Hogger and J. A. Robinson",
  address =     "Oxford"}

@phdthesis{Norell:tppldtt07,
 author = "Ulf Norell",
 title = "{Towards a practical programming language based on dependent type theory}",
 school = "{Chalmers University of Technology and G{\"o}teborg University}",
 year = "2007"}

@online{AgdaWiki:on,crossref={AgdaWiki:base},urldate={2019-04-12}}
@misc{AgdaWiki:url,crossref={AgdaWiki:base},
  howpublished = {\url{http://wiki.portal.chalmers.se/agda}}}
@misc{AgdaWiki:base,
 author = "Ulf. Norell",
 title = "{The Agda WiKi}",
 url = {http://wiki.portal.chalmers.se/agda}}


@article{CarFarJer:mlspe11,
  Author    = {Jacques Carette and
               William M. Farmer and
               Filip Jeremic and
               Vincent Maccio and
               Russell O'Connor and
               Quang M. Tran},
  title     = {The MathScheme Library: Some Preliminary Experiments},
  journal   = {CoRR},
  volume    = {abs/1106.1862},
  year      = {2011},
  url       = {http://arxiv.org/abs/1106.1862}}
  
@online{MathematicaNB:on,
  label = {MNB},
  url = {http://www.wolfram.com/notebooks/},
  title = {Wolfram Notebooks},
  urldate = {2019-03-29}}

@online{marsorbiter:on,
  url = {https://www.wired.com/2010/11/1110mars-climate-observer-report/},
  title = {Metric Math Mistake Muffed Mars Meteorology Mission},
  urldate = {2019-06-04}}
  
@book{FibSig:fla02,
 title = {Fibonacci's Liber Abaci: A Translation into Modern English of Leonardo Pisano's Book of Calculation},
 author = {Laurence Sigler},
 year = {2002},
 publisher = {Springer}}
 
@article{HOG,
  author = {Brinkmann, Gunnar and Coolsaet, Kris and Goedgebeur, Jan and M\'{e}lot, Hadrien},
  title = {House of {G}raphs: a database of interesting graphs},
  journal = {Discrete Appl. Math.},
  fjournal = {Discrete Applied Mathematics. The Journal of Combinatorial Algorithms, Informatics and Computational Sciences},
  volume = {161},
  year = {2013},
  number = {1-2},
  pages = {311--314},
  issn = {0166-218X},
  mrclass = {05C75},
  mrnumber = {2973372},
  doi = {10.1016/j.dam.2012.07.018}}

@inproceedings{BaLuCanonical,
  Acmid = {808746},
  Address = {New York, NY, USA},
  Author = {Babai, L\'{a}szl\'{o} and Luks, Eugene M.},
  Booktitle = {Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing},
  Date-Modified = {2018-05-17 21:39:53 +0000},
  Isbn = {0-89791-099-0},
  Numpages = {13},
  Pages = {171--183},
  Publisher = {ACM},
  Series = {STOC '83},
  Title = {Canonical Labeling of Graphs},
  DOI = {10.1145/800061.808746},
  Year = {1983}}	
	
@online{MATLAB:on,
  label = {MLB},
  title = {MATLAB},
  url = {https://www.mathworks.com/products/matlab.html},
  urldate = {2019-01-25}}

@online{MUMPS:on,
  label = {MPS},
  title = {MUltifrontal Massively Parallel sparse direct Solver},
  url = {http://mumps.enseeiht.fr/},
  urldate = {2019-01-25}}

@online{LAPACK:on,
  label = {LPK},
  title = {LAPACK — Linear Algebra PACKage},
  url = {https://www.netlib.org/lapack/},
  urldate = {2019-01-25}}

@online{SNOMEDCT:on,
  label = {SCT},
  title = {{SNOMED} Clinical Terms},
  url = {https://bioportal.bioontology.org/ontologies/SNOMEDCT},
  urldate = {2019-01-25}}

@online{OBI:on,
  label = {OBI},
  title = {Ontology for Biomedical Investigations},
  url = {http://obi-ontology.org/},
  urldate = {2019-01-25}}

@online{SUMO:on,
  label = {SUMO},
  title = {Suggested Upper Merged Ontology},
  url = {http://www.adampease.org/OP/},
  urldate = {2019-01-25}}

@online{SageDB:on,
  label = {SDB},
  title = {{SageMath} Databases},
  url = {http://doc.sagemath.org/html/en/reference/databases/index.html},
  urldate = {2019-01-25}}

@online{FAIR,
  label = {FAIR},
  author    = {European Commission Expert Group on FAIR Data},
  title     = {Turning {FAIR} into reality},
  year      = {2018},
  doi       = {10.2777/1524}}

@online{RADAR:on,
  label = {RR},
  title = {RADAR},
  url = {https://www.radar-service.eu},
  urldate = {2019-01-25}}

@online{GDML:on,
  label = {GDML},
  title = {GDML},
  url = {https://en.wikipedia.org/wiki/Global_Digital_Mathematics_Library},
  urldate = {2019-01-28}}

@online{WanlessData:on,
  author = {Ian Wanless},
  title = {Combinatorial Data},
  url = {http://users.monash.edu.au/~iwanless/data/},
  urldate = {2019-01-25}}

@online{RoyleData:on,
  author = {Gordon Royle},
  title = {Combinatorial Catalogues},
  url = {http://staffhome.ecm.uwa.edu.au/~00013890/data.html},
  urldate = {2019-01-25}}

@online{McKayData:on,
  author = {Brendan McKay},
  title = {Combinatorial Data},
  url = {http://users.cecs.anu.edu.au/~bdm/data/},
  urldate = {2019-01-25}}

@online{gender-gap-science:on,
  label = {GGS},
  title = {Gender Gap in Science},
  url = {https://gender-gap-in-science.org/},
  urldate = {2019-02-24}}
  
@online{digraph6issue:on,
  label = {DG},
  title = {Digraph6 file format incompatibility},
  url = {https://github.com/gap-packages/Digraphs/issues/158},
  urldate = {2019-01-25}}

@online{GAPDigraphFormat:on,
  author = {Jan De Beule and Julius Jonusas and James Mitchell and Michael Torpey and Wilf Wilson},
  title = {GAP package Digraphs},
  url = {https://www.gap-system.org/Packages/digraphs.html},
  urldate = {2019-01-25}}

@online{McKay:gf6:on,
  label = {McF},
  Author = {Brendan McKay},
  Title = {Description of graph6, sparse6 and digraph6 encodings},
  Url = {http://users.cecs.anu.edu.au/~bdm/data/formats.txt},
  urldate = {2019-03-22}}

@online{McKayFormats:on,
  author = {Brendan McKay},
  title = {Graph formats},