@online{wikipedia:matroid,
label = {MWP},
title = {Matroid --- Wikipedia{,} The Free Encyclopedia},
urldate = {2018-04-4},
url = {https://en.wikipedia.org/w/index.php?title=Matroid}}
@Article{imps,
author = "W. Farmer and J. Guttman and F. Thayer",
title = "{IMPS: An Interactive Mathematical Proof System}",
journal = "{Journal of Automated Reasoning}",
pages = "213--248",
volume = "11",
number = "2",
year = "1993",
}
@Book{isabelle,
author = "L. Paulson",
title = "{Isabelle: A Generic Theorem Prover}",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = "828",
year = "1994",
}
@INPROCEEDINGS{NorKoh:efnrsmk07,
author = {Immanuel Normann and Michael Kohlhase},
title = {Extended Formula Normalization for $\epsilon$-Retrieval and
Sharing of Mathematical Knowledge},
pages = {266--279},
crossref = {MKM07},
keywords = {conference},
pubs = {mkohlhase,mws,omdoc}}
@inproceedings{KMOR:pvs:17,
author = "M. Kohlhase and D. M{\"u}ller and S. Owre and F. Rabe",
title = "{Making PVS Accessible to Generic Services by Interpretation in a Universal Format}",
year = "2017",
pages = "319--335",
booktitle = "Interactive Theorem Proving",
editor = "M. Ayala-Rincon and C. Munoz",
publisher = "Springer"
}
@inproceedings{hol_isahol_matching,
author = {T. Gauthier and C. Kaliszyk},
title = "{Matching concepts across HOL libraries}",
booktitle = {Intelligent Computer Mathematics},
editor = {S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban},
pages = {267--281},
year = 2014,
publisher = {Springer}
}
@online{OAFproject:on,
label = {OAF},
url = {https://kwarc.info/projects/oaf/},
title = {{OAF}: An Open Archive for Formalizations},
urldate = {2018-04-26}}
@Article{lf,
author = "R. Harper and F. Honsell and G. Plotkin",
title = "{A framework for defining logics}",
journal = "{Journal of the Association for Computing Machinery}",
year = 1993,
volume = 40,
number = 1,
pages = "143--184",
}
@inproceedings{KKMR:alignments:16,
author = "C. Kaliszyk and M. Kohlhase and D. M{\"u}ller and F. Rabe",
title = "{A Standard for Aligning Mathematical Concepts}",
year = "2016",
pages = "229--244",
booktitle = "Work in Progress at CICM 2016",
editor = "A. Kohlhase and M. Kohlhase and P. Libbrecht and B. Miller and F. Tompa and A. Naummowicz and W. Neuper and P. Quaresma and M. Suda",
publisher = "CEUR-WS.org"
}
@inproceedings{ODK:mitm:16,
author = "P. Dehaye and M. Iancu and M. Kohlhase and A. Konovalov and S. Leli{\`e}vre and D. M{\"u}ller and M. Pfeiffer and F. Rabe and N. Thi{\'e}ry and T. Wiesing",
title = "{Interoperability in the ODK Project: The Math-in-the-Middle Approach}",
year = "2016",
pages = "117--131",
booktitle = "Intelligent Computer Mathematics",
editor = "M. Kohlhase and L. {de Moura} and M. Johansson and B. Miller and F. Tompa",
publisher = "Springer"
}
@inproceedings{MRLR:alignments:17,
author = "D. M{\"u}ller and C. Rothgang and Y. Liu and F. Rabe",
title = "{Alignment-based Translations Across Formal Systems Using Interface Theories}",
year = "2017",
pages = "77--93",
booktitle = "Proof eXchange for Theorem Proving",
editor = "C. Dubois and B. {Woltzenlogel Paleo}",
publisher = "Open Publishing Association"
}
@INPROCEEDINGS{mathhub,
author = "M. Iancu and C. Jucovschi and M. Kohlhase and T. Wiesing",
title = "{System Description: MathHub.info}",
booktitle = "Intelligent Computer Mathematics",
editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
pages = "431--434",
publisher = "Springer",
year = {2014},
}
@inproceedings{RupKohMue:fitgv17,
author = {Marcel Rupprecht and Michael Kohlhase and Dennis M{\"u}ller},
title = {A Flexible, Interactive Theory-Graph Viewer},
crossref = {MathUI17},
url = {http://kwarc.info/kohlhase/papers/mathui17-tgview.pdf},
pubs = {dmueller,mkohlhase,mrupprecht,odk,mathhub,odkWP6}}
@book{omdoc,
author = "M. Kohlhase",
title = "{OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)}",
series = "{Lecture Notes in Artificial Intelligence}",
number = "4180",
publisher = "Springer",
year = "2006",
}
@PROCEEDINGS{MKM07,
title = {{MKM/Calculemus}},
booktitle = {Towards Mechanized Mathematical Assistants. {MKM/Calculemus}},
year = {2007},
isbn = {978-3-540-73083-5},
editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
number = {4573},
series = {LNAI},
keywords = {conference},
publisher = {Springer Verlag}}
@Proceedings{MathUI17,
editor = {Andrea Kohlhase and Marco Pollanen},
title = {MathUI 2017: The 12th Workshop on Mathematical User Interfaces},
booktitle = {MathUI 2017: The 12th Workshop on Mathematical User Interfaces},
SOONurl = {http://ceur-ws.org/Vol-1785/},
pubs = {akohlhase},
year = {2017}}
@article{RK:mmt:10,
author = "F. Rabe and M. Kohlhase",
title = "{A Scalable Module System}",
year = "2013",
pages = "1--54",
journal = "Information and Computation",
volume = "230",
number = "1"
}
@inproceedings{KR:hollight:14,
author = "C. Kaliszyk and F. Rabe",
title = "{Towards Knowledge Management for HOL Light}",
year = "2014",
pages = "357--372",
booktitle = "Intelligent Computer Mathematics",
editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
publisher = "Springer"
}
@Article{imps,
author = "W. Farmer and J. Guttman and F. Thayer",
title = "{IMPS: An Interactive Mathematical Proof System}",
journal = "{Journal of Automated Reasoning}",
pages = "213--248",
volume = "11",
number = "2",
year = "1993",
}
@article{RK:mmt:10,
author = "F. Rabe and M. Kohlhase",
title = "{A Scalable Module System}",
year = "2013",
pages = "1--54",
journal = "Information and Computation",
volume = "230",
number = "1"
}
@book{omdoc,
author = "M. Kohlhase",
title = "{OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)}",
series = "{Lecture Notes in Artificial Intelligence}",
number = "4180",
publisher = "Springer",
year = "2006",
}
@inproceedings{KMOR:pvs:17,
author = "M. Kohlhase and D. M{\"u}ller and S. Owre and F. Rabe",
title = "{Making PVS Accessible to Generic Services by Interpretation in a Universal Format}",
year = "2017",
pages = "319--335",
booktitle = "Interactive Theorem Proving",
editor = "M. Ayala-Rincon and C. Munoz",
publisher = "Springer"
}
@inproceedings{KR:hollight:14,
author = "C. Kaliszyk and F. Rabe",
title = "{Towards Knowledge Management for HOL Light}",
year = "2014",
pages = "357--372",
booktitle = "Intelligent Computer Mathematics",
editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
publisher = "Springer"
}
@inproceedings{hol_isahol_matching,
author = {T. Gauthier and C. Kaliszyk},
title = "{Matching concepts across HOL libraries}",
booktitle = {Intelligent Computer Mathematics},
editor = {S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban},
pages = {267--281},
year = 2014,
publisher = {Springer}
}
@Article{lf,
author = "R. Harper and F. Honsell and G. Plotkin",
title = "{A framework for defining logics}",
journal = "{Journal of the Association for Computing Machinery}",
year = 1993,
volume = 40,
number = 1,
pages = "143--184",
}
@inproceedings{pvs,
AUTHOR = {S. Owre and J. Rushby and N. Shankar},
TITLE = "{PVS: A Prototype Verification System}",
BOOKTITLE = "{11th International Conference on Automated Deduction (CADE)}",
YEAR = {1992},
EDITOR = {D. Kapur},
PAGES = {748--752},
PUBLISHER = {Springer},
}
@online{PVSlibraries:on,crossref={PVSlibraries:base},
urldate = {2014-12-17},
label = {PVS}}
@MISC{PVSlibraries:url,crossref={PVSlibraries:base},key = {PVS},
howpublished = {\url{http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/}}}
@MISC{PVSlibraries:base,
title = {{NASA} {PVS} Library},
url = {http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/}}
@BOOK{Graf:ti96,
title = {Term Indexing},
publisher = {Springer Verlag},
year = {1996},
author = {Graf, Peter},
number = {1053},
series = {LNCS}}
@inproceedings{am:doceng10,crossref={DOCENG10},
author = {Serge Autexier and Normen M{\"u}ller},
title = {Semantics-based Change Impact Analysis for Heterogeneous Collections of Documents},
pages = {97--106},
numpages = {10},
url = {http://doi.acm.org/10.1145/1860559.1860580},
doi = {http://doi.acm.org/10.1145/1860559.1860580},
acmid = {1860580},
keywords = {change impact analysis, document collections, document management, graph rewriting, semantics},
pubs = {nmueller,omoc,omdoc}}
@mastersthesis{iancu:msc,
author = "Mihnea Iancu",
title = "{Management of Change in Declarative Languages}",
year = "2012",
school = "Jacobs University Bremen",
pubs={mscthesis}
}
@proceedings{DOCENG10,
editor = {Michael Gormish and Rolf Ingold},
title = {Proceedings of the 10\textsuperscript{th} {ACM} symposium on Document engineering},
booktitle = {Proceedings of the 10\textsuperscript{th} {ACM} symposium on Document engineering},
series = {DocEng '10},
year = {2010},
isbn = {978-1-4503-0231-9},
location = {Manchester, United Kingdom},
publisher = {ACM},
keywords = {conference},
address = {New York, NY, USA}}