kwarcpubs.bib

@string{kpmessage = "READ the README please!!!!!!!!!!!!!!"}
@STRING{stexyear = 2020}
@STRING{testing = 16}

@unpublished{RabRou:modlog21,
  title = {Modular Formalization of Formal Systems},
  author = {Florian Rabe and Navid Roux},
  year = {2021},
  note = {under review},
  url = {https://kwarc.info/people/frabe/Research/RR_modlog_21.pdf},
  pubs = {frabe,nroux,mmt,oaf,latin}}

@mastersthesis{Cerny:bsc20,
  title = {Generating Expressions in MMT},
  author = {Christian Cerny},
  school = {FAU Erlangen-N{\"u}rnberg},
  date = {2020-12-04},
  type = {B.Sc. Thesis},
  url =  {https://gl.kwarc.info/supervision/BSc-archive/blob/master/2020/CernyChristian.pdf},
  pubs = {bscthesis}}

@mastersthesis{Dreier:bsc20,
  title = {Syntax und Semantik von Funktionalen Konzepten in der Mathematik},
  author = {Marcel Nicolas Dreier},
  school = {FAU Erlangen-N{\"u}rnberg},
  date = {2020-12-04},
  type = {B.Sc. Thesis},
  url = {https://gl.kwarc.info/supervision/BSc-archive/blob/master/2020/DreierMarcel.pdf},
  pubs = {bscthesis}}

@MastersThesis{Schaefer:msc20,
  author =   {Jan Frederik Schaefer},
  title =    {Prototyping {NLU} Pipelines -- A Type-Theoretical Framework},
  school =   {Informatik, FAU Erlangen-N\"urnberg},
  type =     {Master's Thesis},
  url =      {https://gl.kwarc.info/supervision/MSc-archive/blob/master/2020/Schaefer_Jan_Frederik.pdf},
  pubs =     {jfschaefer,mscthesis},
  year =     {2020}}

@MastersThesis{Banken:msc20,
  author =   {Michael Banken},
  title =    {Theory Intersection},
  school =   {Informatik, FAU Erlangen-N\"urnberg},
  type =     {Master's Thesis},
  url =      {https://gl.kwarc.info/supervision/MSc-archive/-/blob/master/2020/Banken_Michael.pdf},
  pubs =     {mscthesis},
  year =     {2020}}

@mscthesis{Schaefer:ifigac20,
  title = {Implementing {ForTheL} in {GLIF} -- A case study},
  author = {Jan Frederik Schaefer},
  url = {https://gl.kwarc.info/supervision/projectarchive/-/blob/master/2020/Schaefer_Frederik.pdf},
  type  = {Master Project Report},
  date = {2020},
  pubs = {jfschaefer,mscproject}}

@mscthesis{Schaertl:iqodml20,
  title = {ulo-storage -- Indexing and Querying Organizational Data in Mathematical Libraries},
  author = {Andreas Sch{\"a}rtl},
  url = {https://gl.kwarc.info/supervision/projectarchive/-/blob/master/2020/Schaertl_Andreas.pdF},
  type  = {Master Project Report},
  date = {2020},
  pubs = {mscproject}}

@mscthesis{Roux:spdo20,
  title = {Structure-Preserving Diagram Operators},
  author = {Navid Roux},
  url = {https://gl.kwarc.info/supervision/projectarchive/-/blob/master/2020/Roux_Navid.pdf},
  type  = {Master Project Report},
  school = {FAU Erlangen-N{\"u}rnberg},
  date = {2020-07-17},
  pubs = {nroux,mscproject}}

@mscthesis{Schihada:f20,
  title = {{FameIT}},
  author = {John Schihada},
  url = {https://gl.kwarc.info/supervision/projectarchive/-/blob/master/2020/Schihada_John.pdf},
  type  = {Master Project Report},
  date = {2020},
  pubs = {mscproject,frameit}}

@incollection{AizKoh:mir20,
  author = {Aizawa, Akiko and Kohlhase, Michael},
  title = {Mathematical Information Retrieval},
  pages = {169--185},
  crossref = {NTCIR:eirat20},
  pubs = {mkohlhase}}
  
@online{Betzendahl:jkid20,
  label = {JKI},
  author = {Jonas Betzendahl},
  title = {\texttt{juptyter.kwarc.info} Documentation},
  url = {https://kwarc.info/teaching/IWGS/jupyter-documentation.pdf},
  urldate = {2020-08-29},
  pubs = {jbetzendahl}}


@inproceedings{RouRab:wadt20,
  title = {{Structure-Preserving Diagram Operators}},
  author = {Navid Roux and Florian Rabe},
  year = {2020},
  note = {to appear},
  url = {https://kwarc.info/people/frabe/Research/RR_diagops_20.pdf},
  booktitle = "Recent Trends in Algebraic Development Techniques",
  editor = "A. Corradini and M. Huisman and A. Knapp and M. Roggenbach",
  publisher = "Springer",
  pubs = {nroux,frabe,mmt,oaf}}

@unpublished{RouRab:wadt20abstract,
  title = {{Functorial Diagram Operators}},
  author = {Navid Roux and Florian Rabe},
  year = {2020},
  type = {Extended Abstract},
  note = {Extended abstract accepted as \cite{RouRab:wadt20}},
  pubs = {nroux,frabe,mmt,oaf}}

@unpublished{RouRab:lfmtp20abstract,
  author = {Navid Roux and Florian Rabe},
  title = {{Diagram Operators in a Logical Framework}},
  eventtitle = {Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2020)},
  eventdate = {2020-06-29/2020-06-30},
  year = {2020},
  series = {Frontiers in Artificial Intelligence and Applications},
  keywords = {conference},
  type = {Extended Abstract},
  url = {https://lfmtp.org/workshops/2020/inc/papers/LFMTP_2020_paper_9.pdf},
  pubs = {nroux,frabe,mmt,oaf}}
  
@online{glif:on,
  label = {GLIF},
  title = {{GLIF} Kernel},
  url = {https://github.com/KWARC/GLIF},
  urldate = {2020-06-09}}

@unpublished{KohRab:avdg20,
 title = {Argumentation via Context Graphs},
 author = {Michael Kohlhase and Max Rapp},
 year = {2020},
 pubs = {mrapp,mkohlhase}}
 

@misc{popovhayashi:url,crossref={popovhayashi:base},
  howpublished = {\url{https://gl.mathhub.info/jlogic/pvh}}}
@online{popovhayashi:on,crossref={popovhayashi:base},
  label = {PvH},
  url = {https://gl.mathhub.info/jlogic/pvh},
  year = 2020}
@misc{popovhayashi:base,
  key = {PvH},
  year = 2020,
  title = {{Popov v. Hayashi} as a Context Graph}}

@misc{jlogic:url,crossref={jlogic:base},
  key = {PvH},
  howpublished = {\url{https://gl.mathhub.info/jlogic/course}}}
@online{jlogic:on,crossref={jlogic:base},
  label = {PvH},
  url = {https://gl.mathhub.info/jlogic/course},
  year = 2020}
@misc{jlogic:base,
  title = {{Popov v. Hayashi} as a Context Graph}}

@MastersThesis{Meier:msc97,
  author =   {Andreas Meier},
  title =    {Proof Transformation, Universtät des Saarlandes},
  school =   {Computer Science, Saarland University},
  year =     {1997},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Sorge:msc96,
  author =   {Volker Sorge},
  title =    {Integrating a Computer Algebra System into a Logical Proof Development Environement},
  school =   {Computer Science, Saarland University},
  year =     {1996},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Klein:msc95,
  author =   {Gerald Klein},
  title =    {Unification for a lambda-Calculus with Term Declarations and Intersection Sorts},
  school =   {Computer Science, Saarland University},
  year =     {1995},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Bozkurt:msc,
  author =   {Ahmet Bozkurt},
  title =    {Strategies for Resolution Theorem Provers in Higher-Order Logic},
  school =   {Computer Science, Saarland University},
  year =     {199},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Kuschert:msc95,
  author =   {Susanna Kuschert},
  title =    {An Extension of the lambda-Calculus by Discourse Representation Structures},
  school =   {Computer Science, Saarland University},
  year =     {1995},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Scheja:msc93,
  author =   {Ortwin Scheja},
  title =    {Resolution for Higher-Order Multi-Valued Logics},
  school =   {Computer Science, Saarland University},
  year =     {199},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Klein:msc97,
  author =   {Lars Klein},
  title =    {Intexing Techniques for Higher-Order Logic},
  school =   {Computer Science, Saarland University},
  year =     {1997},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Baur:msc99,
  author =   {Judith Baur},
  title =    {Syntax and Semantics of Mathematical Texts – a Prototype},
  school =   {Computational Linguistics, Saarland University},
  year =     {1999},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Hess:msc99,
  author =   {Stephan Hess},
  title =    {Human Computer Interaction in a Proof Development Environment},
  school =   {Computer Science, Saarland University},
  year =     {1999},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Burkard:msc01,
  author =   {Aljoscha Burkard},
  title =    {Resource-adaptive Model Generation for Natural Language Understanding},
  school =   {Computational Linguistics, Saarland University},
  year =     {2001},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Walther:msc01,
  author =   {Stephan Walther},
  title =    {Model Generation and Dynamic Semantics},
  school =   {Computational Linguistics, Saarland University},
  year =     {2001},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Franke:msc03,
  author =   {Andreas Franke},
  title =    {{MBase}, A Mathematical Knowledge Base},
  school =   {Computer Science, Saarland University},
  year =     {2003},
  type =     {Master's Thesis},
  pubs={mscthesis}}


@MastersThesis{Tayson:msc04,
  author =   {William Tayson},
  title =    {Treating Quantifier Scope by Model Generation},
  school =   {Carnegie Mellon University},
  year =     {2004},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Eisenhardt:msc04,
  author =   {Sarah Eisenhardt},
  title =    {Model Generation for Negations in Natural Language},
  school =   {Carnegie Mellon University},
  year =     {2004},
  type =     {Master's Thesis},
  pubs={mscthesis}}

@MastersThesis{Anca:NLMPforATS09,
  author =   {{\c S}tefan Anca},
  title =    {Natural Language and Mathematics Processing for Applicable Theorem Search},
  school =   {Jacobs University Bremen},
  year =     {2009},
  pubs = {sanca,comma,mws},
  type =     {Master's Thesis},
  keywords = {lamapunbibs},
  url = {https://kwarc.info/people/archive/pubs/msc-2009/aanca.pdf},
  pubs={mscthesis}}

@MastersThesis{Rachev:msc13,
  author =   {Damiel Rachev},
  title =    {{FrameIT}: An User Interface for Applying Mathematical Theories to Real World Problems},
  school =   {Jacobs University Bremen},
  year =     {2013},
  pubs = {bscthesis},
  type =     {Bachelor's Thesis},
  url = {https://gl.kwarc.info/supervision/BSc-archive/blob/master/2013/rachev_daniel.pdf},
  doi = {978-3-030-53518-6_11},
  pubs={mscthesis,frameit}}

@mastersthesis{Makaveeva:msc09,
  title = {Management of Change in Common Criteria IT Security Documentation},
  author = {Milena Makaveeva},
  school = {Jacobs University},
  year = {2009},
  type = {M.Sc. Thesis},
  url = {https://gl.kwarc.info/supervision/MSc-archive/blob/master/2009/makaveeva_milena.pdf},
  pubs = {mscthesis}}

@mastersthesis{Jakubauskas:msc13,
  title = {Reflecting Declarative Rule Implementations},
  author = {Aivaras Jakubauskas},
  school = {Jacobs University},
  year = {2013},
  type = {M.Sc. Thesis},
  url = {https://gl.kwarc.info/supervision/MSc-archive/blob/master/2013/jakubauskas_aivaras.pdf},
  pubs = {mscthesis}}

@mastersthesis{Jucovschi:msc10,
  title = {Editing Knowledge in Large Mathematical Corpora. A case study with Semantic {\LaTeX} ({sTeX})},
  author = {Constantin Jucovschi},
  school = {Jacobs University},
  year = {2010},
  type = {M.Sc. Thesis},
  url = {https://gl.kwarc.info/supervision/MSc-archive/blob/master/2010/jucovschi_constantin.pdf},
  pubs = {mscthesis,cjucovschi}}
  
@mastersthesis{Grigore:msc10,
  title = {Knowledge-poor Interpretation of Mathematical Expressions in Context},
  author = {Mihai Grigore},
  school = {Jacobs University},
  year = {2010},
  type = {M.Sc. Thesis},
  url = {https://gl.kwarc.info/supervision/MSc-archive/blob/master/2010/grigore_mihai.pdf},
  pubs = {mscthesis}}

@mastersthesis{Holsten:msc10,
  title = {Smart Management of Change on {OMDoc} Documents},
  author = {S{\"o}nke Holsten},
  school = {Jacobs University},
  year = {2010},
  type = {M.Sc. Thesis},
  url = {https://gl.kwarc.info/supervision/MSc-archive/blob/master/2010/grigore_mihai/thesis/thesis_template.pdf},
  pubs = {mscthesis}}

@mastersthesis{Roux:bsc19,
  title = {{Refactoring of Theory Graphs in Knowledge Representation Systems}},
  author = {Navid Roux},
  school = {FAU Erlangen-N{\"u}rnberg},
  date = {2019-07-01},
  type = {B.Sc. Thesis},
  url = {https://gl.kwarc.info/supervision/BSc-archive/blob/master/2019/Roux_Navid.pdf},
  pubs = {bscthesis,nroux}}

@mastersthesis{Boesl:msc20,
  title = {Designing a Framework for Beneficial Serious Math Games Using the {FrameIt} Method},
  author = {Benjamin B{\"o}sl},
  school = {FAU Erlangen-N{\"u}rnberg},
  year = {2020},
  month = {3},
  type = {M.Sc. Thesis},
  url = {https://gl.kwarc.info/supervision/MSc-archive/blob/master/2020/Boesl_Benjamin.pdf},
  pubs = {mscthesis,frameit}}

@inproceedings{SchKoh:pcmljn20,
  author = {Jan Frederik Schaefer and Kai Amann and Michael Kohlhase},
  title = {Prototyping Controlled Mathematical Languages in Jupyter Notebooks},
  year = {2020},
  crossref = {ICMS20},
  pages = {406--415},
  url = {https://kwarc.info/kohlhase/papers/icms20-glf-jupyter.pdf},
  pubs = {jfschaefer,mkohlhase,mmt,comma}}
  
@inproceedings{MueRabRot:rslffml20,
  title = {Representing Structural Language Features in Formal Meta-Languages},
  author = {Dennis M{\"u}ller and Florian Rabe and Colin Rothgang and Michael Kohlhase},
  crossref = {CICM20},
  pages = {206--221},
  url = {https://kwarc.info/kohlhase/papers/cicm20-features.pdf},
  pubs = {mkohlhase,frabe,dmueller,oaf,mmt},
  keywords = {conference}}


@inproceedings{MarKohRab:tgview3D20,
  title = {TGView3D: a System  for 3-Dimensional Visualization of Theory Graphs},
  author = {Richard Marcus and Michael Kohlhase and Florian Rabe},
  crossref = {CICM20},
  pages = {290--296},
  url = {https://kwarc.info/kohlhase/papers/cicm20-tgview3d.pdf},
  pubs = {mkohlhase,frabe,rmarcus,mathhub,mmt},
  keywords = {conference}}

@inproceedings{KohBoeMar:frameit20,
  title = {{FrameIT}: Detangling Knowledge Management from Game Design in Serious Games},
  author = {Michael Kohlhase and Benjamin B{\"o}sl and Richard Marcus and Dennis M{\"u}ller and Denis Rochau and Navid Roux and John Schihada and Marc Stamminger}, 
  crossref = {CICM20},
  pages={173--189},
  XXdoi = {10.1007/978-3-030-53518-6_11},
  url = {https://kwarc.info/kohlhase/papers/cicm20-frameit.pdf},
  pubs = {mkohlhase,nroux,rmarcus,dmueller,frameit,mmt},
  keywords = {conference}}

@inproceedings{SchKoh:glif20,
  author = {Jan Frederik Schaefer and Michael Kohlhase},
  title = {{GLIF}: A Declarative Framework for Symbolic Natural Language Understanding},
  booktitle = {Proceedings of the 6th Workshop on Formal and Cognitive Reasoning},
  editor = {Beierle, Christoph and Ragni, Marco and Stolzenburg, Frieder and Thimm, Matthias},
  pages = {4--11},
  year = {2020},
  url = {http://ceur-ws.org/Vol-2680/paper1.pdf},
  pubs = {jfschaefer,mkohlhase,mmt,comma}}

@unpublished{KohKoh:lfaets20,
  author = {Andrea Kohlhase and Michael Kohlhase},
  title = {Linebreaking Formulae -- An Eye-Tracking Study},
  year = {2020},
  url = {https://kwarc.info/kohlhase/submit/cicm20-eyetracking.pdf},
  pubs = {akohlhase,mkohlhase}}

@inproceedings{BerKohRab:thqlmk20,
  author = {Katja Ber{\v c}i{\v c} and Michael Kohlhase and Florian Rabe},
  year = {2020},
  title = {Towards a Heterogeneous Query Language for Mathematical Knowledge},
  url = {https://kwarc.info/kohlhase/papers/cicm20-search.pdf},
  crossref = {CICM20},
  pages = {39--54},
  pubs = {kbercic,mkohlhase,frabe},
  keywords = {conference}}
  
@online{BerKohRab:thqlmker20,
  author = {Katja Ber{\v c}i{\v c} and Michael Kohlhase and Florian Rabe},
  year = {2020},
  title = {Towards a Heterogeneous Query Language for Mathematical Knowledge -- Extended Report},
  url = {https://kwarc.info/kohlhase/papers/tetrasearch.pdf},
  type = {Living Whitepaper},
  pubs = {mkohlhase,frabe,kbercic,mathhub,mmt},
  urldate = {2020-03-27}}

@online{ufmmt:on,
  label = {UFM},
  title = {Formalizations for UFrameIT FrameWorld},
  url = {https://gl.mathhub.info/FrameIT/FrameWorld},
  pubs = {frameit},
  urldate = {2020-03-19},
  pubs = {frameit}}

@inproceedings{Bercic:LWDA19,
  crossref = {LWDA19},
  author    = {Katja Bercic},
  title     = {Towards a Census of Relational Data in Mathematics},
  pages     = {207--217},
  url       = {http://ceur-ws.org/Vol-2454/paper_40.pdf},
  pubs = {kbercic,mathhub},
  pubs = {kbercic}}

@inproceedings{KohRapp:cgal19,
 author = {Michael Kohlhase and Max Rapp},
 title = {Context Graphs for Argumentation Logics},
 crossref = {LWDA19},
 pages = {265--279},
 url = {http://ceur-ws.org/Vol-2454/paper_63.pdf},
 pubs = {mkohlhase,mrapp,almanac}}
  
@unpublished{KohRab:eempal20,
  title = {Experiences from Exporting Major Proof Assistant Libraries},
  author = {Michael Kohlhase and Florian Rabe},
  url = {https://kwarc.info/kohlhase/submit/oaf-experiences.pdf},
  year = {2020},
  eprint = {2005.03089},
  eprinttype = {arxiv},
  eprintclass = {cs.SE},
  note = {under review},
  pubs = {mkohlhase,frabe,oaf}}
  
@online{ijcar2020demo:on,
  label = {GD},
  title = {GLIF Demo},
  url = {https://gl.kwarc.info/COMMA/glif-demo-ijcar-2020},
  pubs = {mkohlhase,jschaefer,comma},
  urldate = {2020-01-27}}

@online{elpiprovers:on,
  label = {GEP},
  title = {Generated ELPI Provers},
  url = {https://gl.mathhub.info/MMT/LATIN2/tree/devel/elpi},
  pubs = {frabe,mkohlhase,jschaefer,oaf},
  urldate = {2020-01-26}}
  
@unpublished{KohRabSacSch:lipslfer20,
  title = {Logic-Independent Proof Search in Logical Frameworks (extended report)},
  author = {Michael Kohlhase and Florian Rabe and Claudio Sacerdoti Coen and Jan Frederik Schaefer},
  url = {https://kwarc.info/kohlhase/submit/mmtelpi.pdf},
  note = {extended report of conference submission},
  year = {2020},
  pubs = {mkohlhase,frabe,jfschaefer,oaf}}

@inproceedings{KohRabSacSch:lipslfsp20,
  title = {Logic-Independent Proof Search in Logical Frameworks (short paper)},
  author = {Michael Kohlhase and Florian Rabe and Claudio Sacerdoti Coen and Jan Frederik Schaefer},
  crossref = {IJCAR20},
  pages = {395--401},
  pubs = {mkohlhase,frabe,jfschaefer,oaf,comma},
  keywords = {conference}}

@phdthesis{DMueller:phd:19,
  author = {Dennis M{\"u}ller},
  school = {Informatics, FAU Erlangen-N{\"u}rnberg},
  title = {Mathematical Knowledge Management Across Formal Libraries},
  url = {https://opus4.kobv.de/opus4-fau/files/12359/thesis.pdf},
  Month = {12},
  year = {2019},
  pubs = {dmueller,phdthesis,mmt,oaf}}

	
@inproceedings{KohRabWen:micakrf20,
  title = {Making {Isabelle} Content Accessible in Knowledge Representation Formats},
  author = {Michael Kohlhase and Florian Rabe and Makarius Wenzel},
  booktitle = {Proceedings of the 25th International Conference on Types for Proofs and Programs, TYPES 2019},
  editor = {Marc Bezem and Assia Mahboubi},
  publisher = {Dagstuhl Publishing},
  year = {2020},
  series ={Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN ={978-3-95977-158-0},
  ISSN ={1868-8969},
  volume ={175},
  URL ={https://drops.dagstuhl.de/opus/volltexte/2020/13065},
  URN ={urn:nbn:de:0030-drops-130651},
  doi ={10.4230/LIPIcs.TYPES.2019.1},
  pubs = {mkohlhase,oaf,frabe}}

@unpublished{KohRabWen:micakrf20,
  title = {Making {Isabelle} Content Accessible in Knowledge Representation Formats},
  author = {Michael Kohlhase and Florian Rabe and Makarius Wenzel},
  url = {https://arxiv.org/abs/2005.08884},
  eprint = {2005.08884},
  Eprinttype = {arxiv},
  eprintclass = {cs.LO},
  year = {2020},
  pubs = {mkohlhase,oaf,frabe}}

@mastersthesis{Alt:bsc19,
  title = {Diagram Chasing Done Meta -- Formula Search for {nLab}},
  author = {Christoph Alt},
  school = {FAU Erlangen-N{\"u}rnberg},
  year = {2019},
  type =     {B.Sc. Thesis},
  month = {12},
  url = {https://gl.kwarc.info/supervision/BSc-archive/blob/master/2019/Alt_Christoph.pdf},
  pubs = {bscthesis,mathhub,mws}}

@unpublished{CarFarSharBerKohMueRab:somss20,
 author = {Jacques Carette and William M. Farmer and Yasmine Sharoda and 
           Katja Ber{\v c}i{\v c} and Michael Kohlhase and Dennis M{\"u}ller and Florian Rabe},
 title = {The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems},
 note = {preprint; \url{http://arxiv.org/abs/2002.04955}},
 pubs = {mkohlhase,kbercic,dmueller,frabe},
 year = {2020}}
 
@online{DMH:cvt,
  label = {CVT},
  title = {DataMathHub - Census of Small, Connected, Cubic, Vertex-Transitive Graphs},
  url = {https://data.mathhub.info/collection/cvt/},
  pubs = {kbercic},
  urldate = {2019-12-14}}

@online{DMH:cvt-schema,
  label = {CVT},
  title = {\texttt{vt\_schema.mmt}},
  url = {https://gl.mathhub.info/ODK/mbgen/blob/master/source/cvt_schema.mmt},
  urldate = {2019-12-14}}

@online{MMT:namespaces:on,
  label = {MNS},
  title = {Documents and Namespaces},
  url = {https://uniformal.github.io/doc/language/namespaces},
  urldate = {2019-11-23}}
  
@online{data.mathhub:on,
 label = {DMH},
 title = {Datasets on MathHub.info},
 url = {https://data.mathhub.info},
 urldate = {2019-09-24}}
 
@online{ODK-WDM19,
  label = {WDM},
  title = {Workshop on Data in Mathematics},
  url = {https://opendreamkit.org/2019/08/17/WorkshopOnDataInMathematics/},
  urldate = {2019-08-27}}
  
@article{BerKohRab:dfm19,
  author = {Katja Ber{\v c}i{\v c} and Michael Kohlhase and Florian Rabe},
  title = {(Deep) FAIR Mathematics},
  journal = {it -- Information Technology},
  year = "2020",
  publisher = "De Gruyter Oldenbourg",
  volume = "62",
  number = "1",
  pages = "7--17",
  doi = {10.1515/itit-2019-0028},
  publisher = {De Gruyter},
  url = {https://kwarc.info/kohlhase/submit/it19.pdf},
  pubs = {mkohlhase,frabe,kbercic,mathhub,mdh}}

@article { DeepFAIRmathematics,
      author = "Katja Berčič and Michael Kohlhase and Florian Rabe",
      title = "(Deep) FAIR mathematics",
      journal = "it - Information Technology",
      year = "2020",
      publisher = "De Gruyter Oldenbourg",
      volume = "62",
      number = "1",
      pages = "7--17",
      url = "https://www.degruyter.com/view/journals/itit/62/1/article-p7.xml"
}
@mastersthesis{Plivelic:bsc,
  title = {Using machine learning to support annotating of keywords in mathematical texts},
  author = {Marian Plivelic},
  school = {FAU Erlangen-N{\"u}rnberg},
  year = {2018},
  type =     {B.Sc. Thesis},
  month = {2},
  url = {https://gl.kwarc.info/supervision/BSc-archive/blob/master/2018/Plivelic_Marian.pdf},
  pubs = {bscthesis,comma,stex}}

@mastersthesis{Gorolenkov:bsc,
  title = {Meaning Extraction in STEM-Documents by Machine-Learning Methods},
  author = {Dmitry Gorolenkov},
  school = {FAU Erlangen-N{\"u}rnberg},
  year = {2018},
  type =     {B.Sc. Thesis},
  month = {9},
  url = {https://gl.kwarc.info/supervision/BSc-archive/blob/master/2018/gorolenkov.pdf},
  pubs = {bscthesis,comma}}

@mastersthesis{Lohnert:bsc,
  author = {Patrick Lohnert},
  title = {Automatisches Ableiten von Steuerungsabl{\"a}ufen durch semantische Modellierung von Funktionen und Methoden der K{\"u}nstlichen Intelligenz},
  school = {FAU Erlangen-N{\"u}rnberg},
  year = {2018},
  type =     {B.Sc. Thesis},
  month = {9},
  url = {https://gl.kwarc.info/supervision/BSc-archive/blob/master/2018/Lohnert_Patrick.pdf},
  pubs = {bscthesis}}

@mastersthesis{Marcus:msc,
  author = {Richard Marcus},
  title = {{3D}-Visualization of Theory Graphs},
  school = {FAU Erlangen-N{\"u}rnberg},
  year = {2019},
  type = {M.Sc. Thesis},
  month = {4},
  url = {https://gl.kwarc.info/supervision/MSc-archive/blob/master/2019/Marcus_Richard.pdf},
  pubs = {mscthesis,odk,mathhub}}

@mastersthesis{Rupprecht:msc,
  author = {Marcel Rupprecht},
  title = {Visualization of Theory Graphs},
  school = {FAU Erlangen-N{\"u}rnberg},
  year = {2019},
  type = {M.Sc. Thesis}, 
  month = {5},
  url = {https://gl.kwarc.info/supervision/MSc-archive/blob/master/2019/Rupprecht_Marcel.pdf},
  pubs = {mscthesis,odk,mathhub}}

@article{CarFarKohRab:bmobb19,
 author = {Jacques Carette and William M. Farmer and Michael Kohlhase and Florian Rabe},
 title = {Big Math and the  One-Brain Barrier -- The Tetrapod Model of Mathematical Knowledge},
 year = 2020,
 doi = {10.1007/s00283-020-10006-0},
 journal = {Mathematical Intelligencer},
 pubisher = {Springer Verlag},
 pubs = {mkohlhase,frabe,tetrapod,odk,oaf}}
 
@unpublished{Kohhase:tpm19,
  title = {The Theorem Prover Museum -- Conserving the System Heritage of Automated Reasoning},
  author =   {Michael Kohlhase},
  url = {http://arxiv.org/abs/1904.10414},
  pubs = {mkohlhase}}

@inproceedings{KohSch:GLF19,
  title = {{GF + MMT = GLF} -- From Language to Semantics through {LF}},
  author =   {Michael Kohlhase and Jan Frederik Schaefer},
  booktitle = {Proceedings of the Fourteenth Workshop on
               Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2019},
  editor    = {Miller, Dale and Scagnetto, Ivan},
  year = {2019},
  volume    = {307},
  publisher = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
  pages     = {24-39},
  doi       = {10.4204/EPTCS.307.4},
  pubs = {mkohlhase,jfschaefer,comma}}

@inproceedings{SchKoh:ssahpml16,
  author =   {Jan Frederik Schaefer and Michael Kohlhase},
  title =    {Syntactic/Semantic Analysis for High-Precision Math Linguistics},
  crossref = {CICM18WIP},
  note = {CICM Work in Progress Paper},
  url = {http://ceur-ws.org/Vol-2307/WiP1.pdf},
  pubs = {mkohlhase,jfschaefer,comma}}

@inproceedings{MueRab:rpfsm19,
  year = {2019},
  title = {Rapid Prototyping Formal Systems in MMT: 5 Case Studies},
  author = {Dennis M{\"u}ller and Florian Rabe},
  booktitle = {LFMTP 2019},
  publisher = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
  url = {https://kwarc.info/people/frabe/Research/MR_prototyping_19.pdf},
  pubs = {dmueller,frabe,oaf,odk}}

@online{zbf:on,
  label = {ZBF},
  title = {{zbMATH} -- Formula Search},
  urldate = {2019-03-28},
  url = {https://zbmath.org/formulae/}}
  
@article{BerVid:DZ19,
  year = {2020},
  date = {2020/02/14},
  doi = {10.1007/s11786-020-00453-5},
  author = {Katja Ber\v{c}i\v{c} and Jano\v{s} Vidali},
  title = {DiscreteZOO: a Fingerprint Database of Discrete Objects},
  journal = {Mathematics in Computer Science},
  url = {https://doi.org/10.1007/s11786-020-00453-5},
  issn = {1661-8289},
  pubs={kbercic,odk}}

@inproceedings{MueRabSac:cltg19,
  author = "Dennis M{\"u}ller and Florian Rabe and Sacerdoti Coen, Claudio",
  title = "{The Coq Library as a Theory Graph}",
  crossref = {CICM19},
  keywords = {conference},
  pubs = {dmueller,oaf,frabe}
}

@online{ULODoc:on,
  label = {ULO},
  title = {ULO Documentation},
  url  = {https://ulo.mathhub.info/},
  urldate = {2019-03-11}}

@inproceedings{ConKohMue:rdaml19,
  crossref = {CICM19},
  keywords = {conference},
  title = {Relational Data Across Mathematical Libraries},
  author = {Andrea Condoluci and Michael Kohlhase and Dennis M{\"u}ller and Florian Rabe and Sacerdoti Coen, Claudio and Makarius Wenzel},
  pages = {61--76},
  url = {https://kwarc.info/kohlhase/papers/cicm19-ulo.pdf},
  pubs = {frabe,mkohlhase,dmueller}}

@inproceedings{BerKohRab:tumdi19,
  crossref = {CICM19},
  keywords = {conference},
  title = {Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation},
  author = {Katja Ber{\v c}i{\v c} and Michael Kohlhase and Florian Rabe},
  pages = {28--43},
  url = {https://kwarc.info/kohlhase/papers/cicm19-MDH.pdf},
  pubs = {frabe,mkohlhase,kbercic,odk}}

@unpublished{MarKohRab:tsddvtg19,
  title = {{TGView3D} System Description: 3-Dimensional Visualization of Theory Graphs},
  author = {Richard Marcus and Michael Kohlhase and Florian Rabe},
  url = {https://kwarc.info/kohlhase/submit/tgview3D.pdf},
  pubs = {frabe,mkohlhase,rmarcus,odk}}

@inproceedings{AmaKohRab:ismddn19,
  crossref = {CICM19},
  keywords = {conference},
  title = {Integrating Semantic Mathematical Documents and Dynamic Notebooks},
  author = {Kai Amann and Michael Kohlhase and Florian Rabe and Tom Wiesing},
  pages = {275--290},
  url = {https://kwarc.info/kohlhase/papers/cicm19-jupyter.pdf},
  pubs = {frabe,mkohlhase,twiesing,kamann,odk}}

@inproceedings{ShaRab:dcm19,
  crossref = {CICM19},
  keywords = {conference},
  title = {Diagram Operators in {MMT}},
  pages = {211--226},
  author = {Yasmine Sharoda and Florian Rabe},
  pubs = {frabe}}

@online{TGWiki:on,
	url = {https://github.com/UniFormal/TGView/wiki},
	title = {{Graph Format Description}},
	label = {TGWIKI},
	urldate = {2019-03-07}}

@online{TGW3DWEB:on,
	url = {https://tgview3d.mathhub.info},
	title = {{TGView3D Web Version}},
	label = {T3W},
	urldate = {2019-03-07}}

@online{TGView2D:on,
	url = {https://mmt.mathhub.info/graphs/tgview.html},
	title = {{TGView@MathHub}},
	label = {TGV},
	urldate = {2019-03-07}
}

@online{kwarc:datahost:on,
  label = {KDH},
  title = {{KWARC} Data Host},
  url = {https://datahost.kwarc.info/},
  urldate = {2019-01-25}}

@online{bercic:cmo:table,
  label = {MDT},
  author = {Katja Ber\v{c}i\v{c}},
  title = {Math Databases Table},
  url = {https://mathdb.mathhub.info/},
  urldate = {2020-01-15},
  pubs = {kbercic,cmo-survey}}

@online{Bercic:cmo:wiki,crossref={Bercic:cmo:wiki:base},urldate = {2019-01-15}}
@misc{Bercic:cmo:wiki:url,crossref={Bercic:cmo:wiki:base},
 howpublished = {\url{https://github.com/MathHubInfo/Documentation/wiki/Math-Databases}}}
@misc{Bercic:cmo:wiki:base,
  author = {Katja Ber\v{c}i\v{c}},
  title = {Math Databases wiki},
  url = {https://github.com/MathHubInfo/Documentation/wiki/Math-Databases},
  pubs = {kbercic,cmo-survey,odk}}

@phdthesis{Bercic:phd:15,
  author = {Katja Ber\v{c}i\v{c}},
  school = {Faculty of Mathematics and Physics, University of Ljubljana},
  title = {Constructions and catalogisation of symmetric graphs : PhD thesis (in slovenian)},
  month = {5},
  year = {2015},
  pubs = {kbercic}}

@article{BerGha:4AT2pq:17,
  author = {Katja Ber\v{c}i\v{c} and Mohsen Ghasemi},
  title = {Tetravalent arc-transitive graphs of order twice a product of two primes},
  volume = {312},
  number = {24},
  pages = {3643--3648},
  year = {2012},
  journal = {Discrete Mathematics},
  publisher = {Elsevier},
  doi = {10.1016/j.disc.2012.08.018},
  pubs = {kbercic}
}

@article{BerPot:4AT2pq:17,
  author = {Katja Ber\v{c}i\v{c} and Primo\v{z} Poto\v{c}nik},
  title = {Two-arc-transitive two-valent digraphs of certain orders},
  volume = {11},
  number = {1},
  pages = {127--146},
  year = {2016},
  journal = {Ars Mathematica Contemporanea},
  doi = {10.26493/1855-3974.747.2d3},
  pubs = {kbercic}
}

@incollection{BerIJS:3xl,
  author = {Evgenia Belyaeva and Jan Ber{\v c}i{\v c} and Katja Ber{\v c}i{\v c} and Flavio Fuart and Alja{\v z} Ko{\v s}merlj and Andrej Muhi{\v c} and Aljo{\v s}a Rehar and Jan Rupnik and Mitja Trampu{\v s}},
  title = {3XL News: A Cross-lingual News Aggregator and Reader},
  booktitle = {The Semantic Web: ESWC 2015 Satellite Events},
  publisher = {Springer International Publishing},
  series = {Lecture Notes in Computer Science},
  isbn = {978-3-319-25638-2},
  doi = {10.1007/978-3-319-25639-9_1},
  pages = {3-8},
  volume = {9341},
  year = {2015},
  pubs = {kbercic}}

@inproceedings{BerVid:DZ:18,
  title = {DiscreteZOO: Towards a Fingerprint Database of Discrete Objects},
  author = {Katja Ber\v{c}i\v{c} and Jano{\v{s}} Vidali},
  url = {https://link.springer.com/chapter/10.1007/978-3-319-96418-8_5},
  pages = {36--44},
  year = {2018},
  booktitle = {Mathematical Software -- ICMS 2018},
  isbn = {978-3-319-96418-8},
  publisher = {Springer International Publishing},
  pubs = {kbercic}}

@article{Costello:mopd09,
  title = {Motivating Online Publication of Data},
  author = {Mark J. Costello},
  journal =  {BioScience},
  volume = {59},
  number = {5},
  year = {2009},
  pages  = {418--427},
  url = {https://academic.oup.com/bioscience/article-lookup/doi/10.1525/bio.2009.59.5.9}}

@online{data-citation:usgs:on,
  label = {DC},
  url = {https://www.usgs.gov/products/data-and-tools/data-management/data-citation},
  title = {Data Citation},
  urldate = {2018-12-07}}
  
@online{SIGMathLing:on,
   label = {SML},
   title = {SIGMathLing -- Special Interest Group on Maths Linguistics},
   url = {http://sigmathling.kwarc.info},
   urldate = {2018-12-07}}
   
@thesis{rapp:bathesis,
  author =   {Max Rapp},
  title =    {{Braucht die {\"O}konomie einen Paradigmenwechsel? Methodische Vorschl{\"a}ge nach Elinor Ostrom}},
  school =   {Munich School of Philosophy},
  type =     {Bachelor's Thesis},
  pubs =     {mrapp},
  year =     {2013}}

@thesis{rapp:mscthesis1,
  author =   {Max Rapp},
  title =    {Is there an Ergodic Axiom in Economics?},
  school =   {London School of Economics and Political Science},
  type =     {Master's Thesis},
  pubs =     {mrapp},
  year =     {2016}}

@thesis{rapp:mscthesis2,
  author =   {Max Rapp},
  title =    {Hybrid Logics for Arguments, Beliefs, and their Dynamics},
  school =   {University of Amsterdam},
  type =     {Master's Thesis},
  url  = {https://eprints.illc.uva.nl/1631/1/MoL-2018-17.text.pdf},
  pubs =     {mrapp},
  year =     {2018}}

@inproceedings{rapp:socialchoice,
  title = {Social Choice and the Problem of Recommending Essential Readings},
  author = {Silvan Hungerb{\"u}hler and Haukur Páll J{\'o}hnsson and Grzegorz Lisowski and Max Rapp},
  crossref = {ESSLLI18},
  pubs={mrapp}}

@inproceedings{rapp:tagmsp,
  title = {Is the Triviality of AGM a Serious Possibility},
  author = {Grzegorz Lisowski and Max Rapp},
  booktitle = {Logic in the Wild: 6th workshop in the 'Logic, Reasoning \& Rationality' series},
  year =  {2017},
  url = {https://www.clps.ugent.be/sites/default/files/events/LogicInTheWild-Abstracts.pdf},
  urldate = {2018-10-13},
  keywords = {workshop},
  pubs={mrapp}}


@inproceedings{Rapp:opushorribilis,
  title = {Winning Questions: inquisitive semantics and the lottery paradox},
  author = {Grzegorz Lisowski and Dean McHugh and Max Rapp },
  booktitle = {5th LSE Graduate Conference in Philosophy of Probability},
  year =  {2016},
  url = {http://www.lse.ac.uk/philosophy/blog/2016/12/14/5th-lse-graduate-conference-in-philosophy-of-probability/},
  urldate = {2018-10-16},
  keywords = {conference},
  pubs={mrapp}}

@online{openmathjson:web, 
  title = {{OpenMath-JSON}},
  author = {Tom Wiesing},
  url = {https://omjson.kwarc.info/},
  urldate = {2018-10-13}}

@MISC{URL:openmathjson:github,
  key = {openmathjson},
  howpublished = {GitHub repository at \url{https://github.com/tkw1536/OpenMath-JSON}},
  note = {accessed 2018-10-14},
  title = {{tkw1536/OpenMath-JSON}},
  url = {https://github.com/tkw1536/OpenMath-JSON}}

@online{OSCAR:on,
  label = {OC},
  title = {{OSCAR} Computer Algebra System},
  url = {https://oscar.computeralgebra.de/},
  urldate = {2018-09-04}}
  
@online{moi.sty:on,
  label = {MOI},
  url = {https://gitlab.com/IMKT/MOI/tree/master/sty},
  title = {The {\LaTeX} package moi},
  urldate = {2018-07-20}}
  
@article{rabe:recon:17,
  author = "F. Rabe",
  title = "{A Modular Type Reconstruction Algorithm}",
  journal = "ACM Transactions on Computational Logic",
  year = "2018",
  pages = "1--43",
  volume = "19",
  number = "4"
}

@online{ALMANAC:on,
  label = {AL},
  url = {https://kwarc.info/projects/almanac/},
  title = {{ALMANAC}: Argumentation Logics Manager \& Argument Context Graph},
  note = {Project Home Page},
  urldate={2018-06-17}}

@online{impsMuseum:on,
  label = {TMI},
  title = {Theorem Prover Museum -- {IMPS}},
  url = {https://github.com/theoremprover-museum/imps},
  urldate = {2018-04-28}}

@inproceedings{BetKoh:titl18,