% Encoding: UTF-8
@COMMENT{BibTeX export based on data in FAU CRIS: https://cris.fau.de/}
@COMMENT{For any questions please write to cris-support@fau.de}
@inproceedings{faucris.111531684,
author = {Benzmüller, Christoph and Brown, Chad and et al.},
author_hint = {Benzmüller C., Brown C., Kohlhase M.},
booktitle = {Third International Joint Conference on Automated Reasoning, IJCAR 2006},
faupublication = {no},
isbn = {9783540371878},
pages = {220-234},
peerreviewed = {Yes},
publisher = {Springer Verlag},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Cut}-simulation in impredicative logics},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-33749556449&origin=inward},
venue = {Seattle, WA},
year = {2006}
}
@inproceedings{faucris.106186124,
author = {Kohlhase, Michael and Kohlhase, Andrea and et al.},
author_hint = {Kohlhase A., Kohlhase M., Lange C.},
booktitle = {6th International Conference on Semantic Systems, I-SEMANTICS '10},
doi = {10.1145/1839707.1839712},
faupublication = {no},
isbn = {9781450300148},
keywords = {annotation; formalization; LATEX; linked data; metadata; ontologies; RDFa; semantic authoring; software engineering; vocabularies},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{STEX}+: {A} system for flexible formalization of linked data},
venue = {Graz},
year = {2010}
}
@article{faucris.120599864,
author = {Kohlhase, Michael and et al.},
author_hint = {Siekmann J., Hess S., Benzmüller C., Cheikhrouhou L., Fiedler A., Horacek H., Kohlhase M., Konrad K., Meier A., Melis E., Pollet M., Sorge V.},
faupublication = {no},
journal = {Formal Aspects of Computing},
keywords = {Agents; Automated deduction; Distributed Artificial Intelligence; Human Computer Interaction; Mathematics; User interface},
pages = {326-342},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{ℒΩUI}: {ℒovely} {ΩMEGA} {User} {Interface}},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-0345829693&origin=inward},
volume = {11},
year = {1999}
}
@inproceedings{faucris.106429884,
author = {Kohlhase, Andrea and Kohlhase, Michael and Lange-Bever, Christoph},
booktitle = {10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010},
doi = {10.1007/978-3-642-14128-7_31},
faupublication = {no},
isbn = {9783642141270},
pages = {355-369},
peerreviewed = {Yes},
title = {{Dimensions} of formality: {A} case study for {MKM} in software engineering},
venue = {Paris},
year = {2010}
}
@inproceedings{faucris.213999946,
author = {Müller, Dennis and Kohlhase, Michael and Rabe, Florian},
booktitle = {11th International Conference on Intelligent Computer Mathematics, CICM 2018},
doi = {10.1007/978-3-319-96812-4_18},
faupublication = {yes},
isbn = {9783319968117},
pages = {209-224},
peerreviewed = {unknown},
publisher = {Springer Verlag},
title = {{Automatically} finding theory morphisms for knowledge management},
year = {2018}
}
@article{faucris.111687004,
author = {Stamerjohanns, Heinrich and Kohlhase, Michael and Ginev, Deyan and David, Catalin and Miller, Bruce},
doi = {10.1007/s11786-010-0024-7},
faupublication = {no},
journal = {Mathematics in Computer Science},
pages = {299-307},
peerreviewed = {Yes},
title = {{Transforming} large collections of scientific publications to {XML}},
volume = {3},
year = {2010}
}
@inproceedings{faucris.106200864,
author = {Kohlhase, Andrea and Kohlhase, Michael},
booktitle = {27th ACM International Conference on Design of Communication, SIGDOC'09},
doi = {10.1145/1621995.1622021},
faupublication = {no},
isbn = {9781605585598},
keywords = {Spreadsheets; Task experience; User assistance},
pages = {135-141},
peerreviewed = {Yes},
title = {{Modeling} task experience in user assistance systems},
venue = {Bloomington, IN},
year = {2009}
}
@article{faucris.120001464,
author = {Kohlhase, Michael and Brown, Chad and Benzmüller, Christoph},
doi = {10.2168/LMCS-5(1:6)2009},
faupublication = {no},
journal = {Logical Methods in Computer Science},
keywords = {Abstract consisteny; Acceptability conditions; Cut-elimination and cut-simulation; Higher-order proof automation in the presence of axioms; Impredicativity; One-sided sequent calculus; Saturation; Simple type theory},
pages = {1-21},
peerreviewed = {Yes},
title = {{Cut}-simulation and impredicativity},
volume = {5},
year = {2009}
}
@inproceedings{faucris.111666984,
author = {Lange-Bever, Christoph and Kohlhase, Michael and David, Catalin and Ginev, Deyan and Kohlhase, Andrea and Matican, Bogdan and Zholudev, Vyacheslav and et al.},
author_hint = {Lange C., Kohlhase M., David C., Ginev D., Kohlhase A., Matican B., Mirea S., Zholudev V.},
booktitle = {8th Extended Semantic Web Conference, ESWC 2011},
doi = {10.1007/978-3-642-21064-8_37},
faupublication = {no},
isbn = {9783642210631},
pages = {471-475},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{The} planetary system: {Executable} science, technology, engineering and math papers},
venue = {Heraklion, Crete},
year = {2011}
}
@inproceedings{faucris.106423504,
author = {Kerber, Manfred and Kohlhase, Michael and Sorge, Volker},
booktitle = {4th International Symposium on Design and Implementation of Symbolic Computation Systems, DISCO 1996},
faupublication = {no},
isbn = {9783540616979},
pages = {204-215},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Integrating} computer algebra with proof planning},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-21444434314&origin=inward},
volume = {1128},
year = {1996}
}
@inproceedings{faucris.110968484,
abstract = {In this paper we present the Active Documents Paradigm (semantically annotated documents associated with a content commons that holds the corresponding background ontologies) and the Planetary system (as an active document player). We show that the current Planetary system gives a solid foundation and can be extended modularly to address most of the criteria of the Executable Papers Challenge.},
author = {Kohlhase, Michael and Corneli, Joe and David, Catalin and Ginev, Deyan and Jucovschi, Constantin and Kohlhase, Andrea and Lange-Bever, Christoph and Matican, Bogdan and Zholudev, Vyacheslav and et al.},
author_hint = {Kohlhase M., Corneli J., David C., Ginev D., Jucovschi C., Kohlhasea A., Lange C., Matican B., Mirea S., Zholudev V.},
booktitle = {11th International Conference on Computational Science, ICCS 2011},
doi = {10.1016/j.procs.2011.04.063},
faupublication = {no},
keywords = {Active documents; Content commons; Executable paper challenge; Ontologies; Semantic annotation},
month = {Jan},
pages = {598-607},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{The} planetary system: {Web} 3.0 & active documents for {STEM}},
venue = {Singapore},
volume = {4},
year = {2011}
}
@article{faucris.111502644,
author = {Rabe, Florian and Kohlhase, Michael},
doi = {10.1016/j.ic.2013.06.001},
faupublication = {no},
journal = {Information and Computation},
pages = {1-54},
peerreviewed = {Yes},
title = {{A} scalable module system},
volume = {230},
year = {2013}
}
@inproceedings{faucris.106442204,
author = {Kohlhase, Andrea and Kohlhase, Michael},
booktitle = {16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009},
doi = {10.1007/978-3-642-02614-0_28},
faupublication = {no},
isbn = {9783642026133},
pages = {341-356},
peerreviewed = {Yes},
title = {{Spreadsheet} interaction with frames: {Exploring} a mathematical practice},
venue = {Grand Bend, ON},
year = {2009}
}
@inproceedings{faucris.111504624,
author = {Kohlhase, Michael and Sucan, Ioan},
booktitle = {8th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2006},
faupublication = {no},
isbn = {9783540397281},
pages = {241-253},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{A} search engine for mathematical formulae},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-33749635061&origin=inward},
venue = {Beijing},
year = {2006}
}
@inproceedings{faucris.106426364,
author = {Codescu, Silvestru Mihai and Horozal, Fulya and Kohlhase, Michael and Mossakowski, Till and Rabe, Florian},
booktitle = {20th International Workshop on Algebraic Development Techniques, WADT 2010},
doi = {10.1007/978-3-642-28412-0_9},
faupublication = {no},
isbn = {9783642284113},
pages = {118-138},
peerreviewed = {Yes},
title = {{A} proof theoretic interpretation of model theoretic hiding},
venue = {Etelsen},
year = {2012}
}
@inproceedings{faucris.111703504,
author = {Codescu, Silvestru Mihai and Horozal, Fulya and Kohlhase, Michael and Mossakowski, Till and Rabe, Florian and Sojakova, Kristina},
booktitle = {20th International Workshop on Algebraic Development Techniques, WADT 2010},
doi = {10.1007/978-3-642-28412-0_10},
faupublication = {no},
isbn = {9783642284113},
pages = {139-159},
peerreviewed = {Yes},
title = {{Towards} logical frameworks in the heterogeneous tool set hets},
venue = {Etelsen},
year = {2012}
}
@inproceedings{faucris.111724404,
author = {Kohlhase, Michael},
booktitle = {International Conference on Logic Programming and Automated Reasoning, LPAR 1992},
doi = {10.1007/BFb0013080},
faupublication = {no},
isbn = {9783540557272},
pages = {421-432},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Unification} in order-sorted type theory},
year = {1992}
}
@article{faucris.111731664,
author = {Kohlhase, Michael and Scheja, Ortwin},
doi = {10.1080/11663081.1999.10510980},
faupublication = {no},
journal = {Journal of Applied Non-Classical Logics},
keywords = {δ-Calculus; Higher-Order Logic; Multi-Valued; Resolution},
pages = {455-477},
peerreviewed = {Yes},
title = {{Higher}-order multi-valued resolution},
volume = {9},
year = {1999}
}
@inproceedings{faucris.111733424,
author = {Lange-Bever, Christoph and Kohlhase, Michael and et al.},
author_hint = {Lange C., Ion P., Dimou A., Bratsas C., Sperber W., Kohlhase M., Antoniou I.},
booktitle = {9th Extended Semantic Web Conference, ESWC 2012},
doi = {10.1007/978-3-642-30284-8_58},
faupublication = {no},
isbn = {9783642302831},
pages = {763-777},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Bringing} mathematics to the web of data: {The} case of the mathematics subject classification},
venue = {Heraklion, Crete},
year = {2012}
}
@inproceedings{faucris.111174624,
author = {Kohlhase, Andrea and Kohlhase, Michael and Jucovschi, Constantin and Toader, Alexandru},
booktitle = {14th IFIP TC 13 International Conference on Human-Computer Interaction, INTERACT 2013},
doi = {10.1007/978-3-642-40477-1_25},
faupublication = {no},
isbn = {9783642404764},
keywords = {CAD systems; frame shifts; Full semantic transparency; multi-application Semantic Alliance; semantic services; spreadsheets},
pages = {406-423},
peerreviewed = {Yes},
title = {{Full} semantic transparency: {Overcoming} boundaries of applications},
venue = {Cape Town},
year = {2013}
}
@inproceedings{faucris.111774344,
abstract = {Starting from the observation that many concrete realizations of mathematical knowledge objects are considered equivalent, we propose a conceptual model of the space of (mathematical) knowledge objects graded by levels of abstraction and presentational explicitness and draw conclusions for MKM markup formats.},
author = {Kohlhase, Andrea and Kohlhase, Michael},
faupublication = {no},
month = {Jan},
pages = {17-32},
peerreviewed = {Yes},
title = {{An} exploration in the space of mathematical knowledge},
volume = {3863},
year = {2006}
}
@inproceedings{faucris.111729904,
abstract = {We propose an analysis of corrections which models some of the requirements corrections place on context. We then show that this analysis naturally extends to the interaction of corrections with pronominal anaphora on the one hand, and (in)definiteness on the other. The analysis builds on previous unification-based approaches to NL semantics and relies on Higher-Order Unification with Equivalences (HOUE), a form of unification which takes into account not only syntactic beta eta-identity but also denotational equivalence.},
author = {Gardent, Claire and Kohlhase, Michael and van Leusen, Noor},
faupublication = {no},
month = {Jan},
pages = {268-279},
peerreviewed = {Yes},
title = {{Corrections} and higher-order unification},
year = {1996}
}
@article{faucris.111775444,
abstract = {In this case study, the constants in the universe are given saliences, that are maintained across the model generation process. This additional data serves as one important source of information for model quality and resource cost estimation.},
author = {Kohlhase, Michael and Koller, Alexander},
faupublication = {no},
journal = {Logic Journal of the Igpl},
keywords = {model generation;natural language understanding;bounded optimality;performance models},
month = {Jan},
pages = {435-456},
peerreviewed = {Yes},
title = {{Resource}-adaptive model generation as a performance model},
volume = {11},
year = {2003}
}
@inproceedings{faucris.111738704,
abstract = {In this paper we revisit Pustejovsky's proposal to treat ontologically complex word meaning by so-called dotted pairs. We use a higher-order feature logic based on Ohori's record lambda-calculus to model the semantics of words like book and library, in particular their behavior in the context of quantification and cardinality statements.},
author = {Pinkal, Manfred and Kohlhase, Michael},
booktitle = {Proceedings of the 38th Annual Meeting of the Association for Computational
Linguistics},
faupublication = {no},
month = {Jan},
pages = {521-528},
peerreviewed = {Yes},
title = {{Feature} logic for dotted types: {A} formalism for complex word meanings},
year = {2000}
}
@inproceedings{faucris.111162744,
author = {Kohlhase, Michael and de Feo, Luca and Müller, Dennis and Pfeiffer, Marcus and Rabe, Florian and Wiesing, Tom and et al.},
author_hint = {Kohlhase M., De Feo L., Müller D., Pfeiffer M., Rabe F., Thiéry N., Vasilyev V., Wiesing T.},
booktitle = {7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017},
doi = {10.1007/978-3-319-72453-9_14},
faupublication = {no},
isbn = {9783319724522},
pages = {195-210},
peerreviewed = {Yes},
publisher = {Springer Verlag},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Knowledge}-based interoperability for mathematical software systems},
year = {2017}
}
@article{faucris.106764724,
author = {Kohlhase, Michael and Rabe, Florian},
faupublication = {no},
journal = {Journal of Formalized Reasoning},
pages = {201-234},
peerreviewed = {unknown},
title = {{QED} reloaded: {Towards} a pluralistic formal library of mathematical knowledge},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84957079748&origin=inward},
volume = {9},
year = {2016}
}
@incollection{faucris.111734524,
author = {Lange-Bever, Christoph and Kohlhase, Michael},
booktitle = {Semantic Mashups: Intelligent Reuse of Web Resources},
doi = {10.1007/978-3-642-36403-7_6},
editor = {Brigitte Endres-Niggemeyer},
faupublication = {no},
isbn = {9783642364020},
pages = {171-204},
peerreviewed = {Yes},
publisher = {Springer Berlin Heidelberg},
title = {{Mashups} using mathematical knowledge: {Why} formulas are different},
year = {2013}
}
@inproceedings{faucris.106445064,
author = {Stamerjohanns, Heinrich and Kohlhase, Michael},
booktitle = {9th Int. Conf. Artificial Intelligence and Symbolic Computation, AISC 2008 - 15th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2008 - 7th Int. Conf. Mathematical Knowledge Management, MKM 2008},
doi = {10.1007/978-3-540-85110-3_46},
faupublication = {no},
isbn = {9783540851097},
pages = {574-582},
peerreviewed = {Yes},
title = {{Transforming} the arχiv to {XML}},
venue = {Birmingham},
year = {2008}
}
@inproceedings{faucris.213996894,
author = {Schaefer, Jan Frederik and Kohlhase, Michael},
booktitle = {Joint 2018 Computer Mathematics in Education - Enlightenment or Incantation, CME-EI 2018, Formal Mathematics for Mathematicians, FMM 2018, Computer Algebra in the Age of Types, CAAT 2018, Formal Verification of Physical Systems, FVPS 2018, Mathematical Models and Mathematical Software as Research Data 2018, M3SRD 2018 and 29th OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS 2018},
faupublication = {yes},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{Syntactic}/semantic analysis for high-precision math linguistics},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-85060658105&origin=inward},
volume = {2307},
year = {2018}
}
@inproceedings{faucris.106433184,
author = {Luzhnica, Enxhell and Iancu, Mihnea and Kohlhase, Michael},
booktitle = {Learning, Knowledge, Adaptation Workshops, LWA 2015: Knowledge Discovery, Data Mining and Machine Learning, KDML 2015, Knowledge Management, FGWM 2015, Information Retrieval, IR 2015 and Database Systems, FGDB 2015},
faupublication = {no},
pages = {296-303},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{Importing} the {OEIS} library into {OMDoc}},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84944342791&origin=inward},
volume = {1458},
year = {2015}
}
@inproceedings{faucris.106436044,
abstract = {We present a tableaux-based model generation calculus for DRT, which gives us an incremental approach to discourse processing in the presence of world knowledge. We show the usefulness of such as system for several discourse phenomena.},
author = {Kohlhase, Michael},
booktitle = {Proceedings of of the 14th European Conference on Artifical Intelligence},
editor = {Werner Horn},
faupublication = {no},
month = {Jan},
pages = {441-445},
peerreviewed = {Yes},
title = {{Model} generation for discourse representation theory},
volume = {54},
year = {2000}
}
@article{faucris.106186344,
author = {Tranh, Ha Man and Lange-Bever, Christoph and Chulkov, Georgi and Schönwälder, Jürgen and Kohlhase, Michael},
doi = {10.1007/s10922-009-9134-4},
faupublication = {no},
journal = {Journal of Network and Systems Management},
keywords = {Bug tracking system; Fault management; Ontology; Resource description framework; Semantic indexing; Semantic search},
pages = {285-308},
peerreviewed = {Yes},
title = {{Applying} semantic techniques to search and analyze bug tracking data},
volume = {17},
year = {2009}
}
@inproceedings{faucris.106438024,
author = {Kohlhase, Michael and Müller, Christine and Rabe, Florian},
booktitle = {9th Int. Conf. Artificial Intelligence and Symbolic Computation, AISC 2008 - 15th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2008 - 7th Int. Conf. Mathematical Knowledge Management, MKM 2008},
doi = {10.1007/978-3-540-85110-3_41},
faupublication = {no},
isbn = {9783540851097},
pages = {504-519},
peerreviewed = {Yes},
title = {{Notations} for living mathematical documents},
venue = {Birmingham},
year = {2008}
}
@inproceedings{faucris.111602524,
abstract = {Omega MEGA is a mixed-initiative system with the ultimate purpose of supporting theorem proving in main-stream mathematics and mathematics education. The current system consists of a proof planner and an integrated collection of tools for formulating problems, proving subproblems, and proof presentation.},
author = {Benzmüller, Christoph and Huang, Xiaorong and Kohlhase, Michael and Kerber, Manfred and Melis, Erica and Siekmann, Jörg and Sorge, Volker and et al.},
author_hint = {Benzmuller C, Cheikhrouhou L, Fehrer D, Fiedler A, Huang XR, Kerber M, Kohlhase M, Konrad K, Meier A, Melis E, Schaarschmidt W, Siekmann J, Sorge V},
faupublication = {no},
month = {Jan},
pages = {252-255},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Omega} {MEGA}: {Towards} a mathematical assistant},
volume = {1249},
year = {1997}
}
@article{faucris.111210484,
author = {Kerber, Manfred and Kohlhase, Michael and Sorge, Volker},
faupublication = {no},
journal = {Journal of Automated Reasoning},
keywords = {Computer algebra; Hierarchical proof planning; Mechanized reasoning; Proof checking},
pages = {327-355},
peerreviewed = {Yes},
title = {{Integrating} {Computer} {Algebra} into {Proof} {Planning}},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-0032287894&origin=inward},
volume = {21},
year = {1998}
}
@inproceedings{faucris.106423944,
author = {Huang, Xiaorong and Kerber, Manfred and Kohlhase, Michael and Richts, Jörn},
booktitle = {18th Annual German Conference on Artificial Intelligence, KI 1994},
faupublication = {no},
isbn = {9783540584674},
pages = {379-390},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Adapting} methods to novel tasks in proof planning},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-2342658424&origin=inward},
year = {1994}
}
@inproceedings{faucris.106183044,
author = {Kohlhase, Andrea and Kohlhase, Michael},
booktitle = {29th ACM International Conference on Design of Communication, SIGDOC'11},
doi = {10.1145/2038476.2038510},
faupublication = {no},
isbn = {9781450309363},
keywords = {change management; consistency management; knowledge management; links; references},
pages = {167-174},
peerreviewed = {Yes},
title = {{Maintaining} islands of consistency via versioned links},
venue = {Pisa},
year = {2011}
}
@inproceedings{faucris.106427024,
author = {Toader, Alexandru and Kohlhase, Michael and Kohlhase, Andrea},
booktitle = {2nd Workshop on Software Engineering Methods in Spreadsheets, SEMS 2015, Co-located with the 37th International Conference on Software Engineering, ICSE 2015},
faupublication = {no},
pages = {14-20},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{Assessment} for spreadsheets},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84930336641&origin=inward},
volume = {1355},
year = {2015}
}
@inproceedings{faucris.111726164,
author = {Stamerjohanns, Heinrich and Ginev, Deyan and David, Catalin and Misev, Dimitar and Kohlhase, Michael and et al.},
author_hint = {Stamerjohanns H., Ginev D., David C., Misev D., Zamdzhiev V., Kohlhase M.},
booktitle = {2nd Workshop on Towards a Digital Mathematics Library, DML 2009},
faupublication = {no},
isbn = {9788021047815},
pages = {109-120},
peerreviewed = {Yes},
publisher = {Masaryk University},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{MathML}-aware article conversion from {LATEX} a comparison study},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84896692132&origin=inward},
venue = {Grand Bend, ON},
year = {2009}
}
@inproceedings{faucris.106428784,
author = {Kohlhase, Michael and Kohlhase, Andrea and et al.},
author_hint = {Kohlhase A., Kohlhase M., Guseva A.},
booktitle = {2nd Workshop on Software Engineering Methods in Spreadsheets, SEMS 2015, Co-located with the 37th International Conference on Software Engineering, ICSE 2015},
faupublication = {no},
pages = {21-27},
peerreviewed = {Yes},
publisher = {CEUR-WS},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Context} in spreadsheet comprehension},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84930355041&origin=inward},
volume = {1355},
year = {2015}
}
@inproceedings{faucris.111571064,
author = {Freksa, Christian and Kohlhase, Michael and Schill, Kerstin},
booktitle = {29th Annual German Conference on Artificial Intelligence (KI 2006)},
faupublication = {no},
isbn = {9783540699118},
peerreviewed = {No},
title = {{Lecture} {Notes} in {Comuter} {Science} ({Including} {Subseries} {Lecture} {Notes} in {Artificial} {Intelligence} and {Lecture} {Notes}: {Preface}},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-35448943067&origin=inward},
venue = {Bremen},
year = {2007}
}
@inproceedings{faucris.106548024,
author = {Kohlhase, Michael and Sperber, Wolfram},
booktitle = {10th International Conference on Intelligent Computer Mathematics, CICM 2017},
doi = {10.1007/978-3-319-62075-6_8},
faupublication = {yes},
isbn = {9783319620749},
pages = {99-114},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Software} citations, information systems, and beyond},
year = {2017}
}
@inproceedings{faucris.111710984,
author = {Kohlhase, Andrea and Kohlhase, Michael},
booktitle = {5th International Conference on Mathematical Knowledge Management, MKM 2006},
faupublication = {no},
isbn = {9783540371045},
pages = {179-193},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Communities} of practice in {MKM}: {An} extensional model},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-33749542803&origin=inward},
venue = {Wokingham},
year = {2006}
}
@inproceedings{faucris.106423724,
author = {Kohlhase, Michael and Kohlhase, Andrea},
booktitle = {27th ACM International Conference on Design of Communication, SIGDOC'09},
doi = {10.1145/1621995.1622013},
faupublication = {no},
isbn = {9781605585598},
keywords = {Interaction; Semantic transparency; User assistance; User interface},
pages = {89-95},
peerreviewed = {Yes},
title = {{Semantic} transparency in user assistance systems},
venue = {Bloomington, IN},
year = {2009}
}
@article{faucris.106201304,
author = {Kohlhase, Michael and Kohlhase, Andrea},
doi = {10.1109/JPROC.2008.921606},
faupublication = {no},
journal = {Proceedings of the IEEE},
keywords = {ELearning; Interaction; Knowledge management; Knowledge representation; Ontology; Semantics},
pages = {970-989},
peerreviewed = {Yes},
title = {{Semantic} knowledge management for education},
volume = {96},
year = {2008}
}
@inproceedings{faucris.111734304,
author = {Hutter, Dieter and Kohlhase, Michael},
booktitle = {14th International Conference on Automated Deduction, CADE 1997},
faupublication = {no},
isbn = {9783540631040},
pages = {291-305},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{A} colored version of the λ-calculus},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-35048867096&origin=inward},
volume = {1249},
year = {1997}
}
@inproceedings{faucris.214003860,
author = {Kohlhase, Michael},
booktitle = {2018 Conference "Learning, Knowledge, Data, Analytics", LWDA 2018},
faupublication = {yes},
pages = {203-214},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{Towards} context graphs for argumentation logics},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-85053594694&origin=inward},
volume = {2191},
year = {2018}
}
@inproceedings{faucris.223104904,
abstract = {Formal libraries are treasure troves of detailed mathematical knowledge, but this treasure is usually locked into system- and logic-specific representations that can only be understood by the respective theorem prover system. In this paper we present an ontology for using relational information on mathematical knowledge and a corresponding data set generated from the Isabelle and Coq libraries. We show the utility of the generated data by setting a relational query engine that provides easy access to certain library information that was previously hard or impossible to determine.},
author = {Condoluci, Andrea and Kohlhase, Michael and Müller, Dennis and Rabe, Florian and Sacerdoti Coen, Claudio and Wenzel, Makarius},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
date = {2019-07-08/2019-07-12},
doi = {10.1007/978-3-030-23250-4_5},
editor = {Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk},
faupublication = {yes},
isbn = {9783030232498},
note = {CRIS-Team Scopus Importer:2019-07-26},
pages = {61-76},
peerreviewed = {unknown},
publisher = {Springer Verlag},
title = {{Relational} {Data} {Across} {Mathematical} {Libraries}},
venue = {Prague},
volume = {11617 LNAI},
year = {2019}
}
@inproceedings{faucris.111260644,
author = {Kohlhase, Michael and Pfenning, Frank},
booktitle = {Proceedings of the International Logic Programming Symposion ILPS'93},
faupublication = {no},
month = {Jan},
pages = {488-505},
peerreviewed = {Yes},
title = {{UNIFICATION} {IN} {A} {LAMBDA}-{CALCULUS} {WITH} {INTERSECTION} {TYPES}},
year = {1993}
}
@inproceedings{faucris.111728804,
author = {Autexier, Serge and David, Catalin and Kohlhase, Michael and Zholudev, Vyacheslav and et al.},
author_hint = {Autexier S., David C., Dietrich D., Kohlhase M., Zholudev V.},
booktitle = {18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011},
doi = {10.1007/978-3-642-22673-1_12},
faupublication = {no},
isbn = {9783642226724},
pages = {164-179},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Workflows} for the management of change in science, technologies, engineering and mathematics},
venue = {Bertinoro},
year = {2011}
}
@inproceedings{faucris.111689644,
author = {Kohlhase, Michael},
booktitle = {18th Annual German Conference on Artificial Intelligence, KI 1994},
faupublication = {no},
isbn = {9783540584674},
pages = {331-342},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Unification} in a sorted λ-calculus with term declarations and function sorts},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-85028712606&origin=inward},
year = {1994}
}
@inproceedings{faucris.214002392,
author = {Wiesing, Tom and Kohlhase, Michael and Rabe, Florian},
booktitle = {7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017},
doi = {10.1007/978-3-319-72453-9_17},
faupublication = {yes},
isbn = {9783319724522},
pages = {243-257},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Virtual} theories – {A} uniform interface to mathematical knowledge bases},
year = {2017}
}
@book{faucris.111740904,
author = {Ginev, Deyan and Jucovschi, Constantin and Kohlhase, Andrea and Kohlhase, Michael and Wiesing, Tom and et al.},
author_hint = {Ginev D., Iancu M., Jucovshi C., Kohlhase A., Kohlhase M., Oripov A., Schefter J., Sperber W., Teschke O., Wiesing T.},
doi = {10.1007/978-3-319-42432-3_58},
faupublication = {no},
isbn = {9783319424316},
pages = {451-457},
peerreviewed = {Yes},
publisher = {Springer Verlag},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{The} {SMGloM} project and system: {Towards} a terminology and ontology for mathematics},
volume = {9725},
year = {2016}
}
@inproceedings{faucris.111655104,
author = {Franke, Andreas and Kohlhase, Michael},
booktitle = {16th International Conference on Automated Deduction, CADE 1999},
doi = {10.1007/3-540-48660-7_17},
faupublication = {no},
isbn = {9783540662228},
pages = {217-221},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{System} description: {MathWeb}, an agent-based communication layer for distributed automated theorem proving},
volume = {1632},
year = {1999}
}
@inproceedings{faucris.106428344,
abstract = {Although much has been said about parallelism in discourse, a formal, computational theory of parallelism structure is still outstanding. in this paper, we present a theory which given two parallel utterances predicts which are the parallel elements. The theory consists of a sorted, higher-order abductive calculus and we show that it reconciles the insights of discourse theories of parallelism with those of Higher-Order Unification approaches to discourse semantics, thereby providing a natural framework in which to capture the effect of parallelism on discourse semantics.},
author = {Kohlhase, Michael and Gardent, Claire},
booktitle = {Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI)},
editor = {Martha E. Pollack},
faupublication = {no},
month = {Jan},
pages = {1016-1021},
peerreviewed = {Yes},
title = {{Computing} parallelism in discourse},
year = {1997}
}
@inproceedings{faucris.106424824,
author = {Kohlhase, Michael and Lange-Bever, Christoph},
booktitle = {LWA 2009 - Workshop-Woche: Lernen-Wissen-Adaptivitat - Learning, Knowledge and Adaptivity},
faupublication = {no},
peerreviewed = {Yes},
title = {{A} mathematical approach to ontology authoring and documentation},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84874182293&origin=inward},
venue = {Darmstadt},
year = {2009}
}
@inproceedings{faucris.106435604,
author = {Kohlhase, Michael and Matican, Bogdan and Prodescu, Corneliu Claudiu},
booktitle = {Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012},
doi = {10.1007/978-3-642-31374-5_23},
faupublication = {no},
isbn = {9783642313738},
pages = {342-357},
peerreviewed = {Yes},
title = {{MathWebSearch} 0.5: {Scaling} an open formula search engine},
venue = {Bremen},
year = {2012}
}
@inproceedings{faucris.106440664,
author = {David, Catalin and Kohlhase, Michael and Lange-Bever, Christoph and Zhiltsov, Nikita and Zholudev, Vyacheslav and et al.},
author_hint = {David C., Kohlhase M., Lange C., Rabe F., Zhiltsov N., Zholudev V.},
booktitle = {7th Extended Semantic Web Conference, ESWC 2010},
doi = {10.1007/978-3-642-13489-0_26},
faupublication = {no},
isbn = {9783642134883},
pages = {370-375},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Publishing} math lecture notes as linked data},
venue = {Heraklion, Crete},
year = {2010}
}
@inproceedings{faucris.223104650,
abstract = {Data plays an increasing role in applied and even pure mathematics: datasets of concrete mathematical objects proliferate and increase in size, reaching upÂ to 1Â TB of uncompressed data and millions of objects. Most of the datasets, especially the many smaller ones, are maintained and shared in an ad hoc manner. This approach, while easy to implement, suffers from scalability and sustainability problems as well as a lack of interoperability both among datasets and with computation systems. In this paper we present another substantial step towards a unified infrastructure for mathematical data: a storage and sharing system with math-level APIs and UIs that makes the various collections findable, accessible, interoperable, and re-usable. Concretely, we provide a high-level data description framework from which database infrastructure and user interfaces can be generated automatically. We instantiate this infrastructure with several datasets previously collected by mathematicians. The infrastructure makes it relatively easy to add new datasets.},
author = {Bercic, Katja and Kohlhase, Michael and Rabe, Florian},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
date = {2019-07-08/2019-07-12},
doi = {10.1007/978-3-030-23250-4_3},
editor = {Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk},
faupublication = {yes},
isbn = {9783030232498},
note = {CRIS-Team Scopus Importer:2019-07-26},
pages = {28-43},
peerreviewed = {unknown},
publisher = {Springer Verlag},
title = {{Towards} a {Unified} {Mathematical} {Data} {Infrastructure}: {Database} and {Interface} {Generation}},
venue = {Prague},
volume = {11617 LNAI},
year = {2019}
}
@inproceedings{faucris.106441544,
author = {David, Catalin and Jucovschi, Constantin and Kohlhase, Andrea and Kohlhase, Michael},
booktitle = {Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012},
doi = {10.1007/978-3-642-31374-5_4},
faupublication = {no},
isbn = {9783642313738},
pages = {49-64},
peerreviewed = {Yes},
title = {{Semantic} alliance: {A} framework for semantic allies},
venue = {Bremen},
year = {2012}
}
@inproceedings{faucris.106433844,
author = {Huang, Xiaorong and Kerber, Manfred and Kohlhase, Michael and Melis, Erica and Siekmann, Jörg and et al.},
author_hint = {Huang X., Kerber M., Kohlhase M., Melis E., Nesmith D., Richts J., Siekmann J.},
booktitle = {12th International Conference on Automated Deduction, CADE-12 1994},
faupublication = {no},
isbn = {9783540581567},
pages = {807-810},
peerreviewed = {Yes},
publisher = {Springer Verlag},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Keim}: {A} toolkit for automated deduction},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84943317064&origin=inward},
year = {1994}
}
@inproceedings{faucris.106770004,
author = {Wiesing, Tom and Kohlhase, Michael and Rabe, Florian and Kohlhase, Michael},
booktitle = {MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences},
doi = {10.1007/978-3-319-72453-9_17},
editor = {Johannes Blömer and Temur Kutsia and Dimitris Simos},
faupublication = {yes},
isbn = {978-3-319-72453-9},
pages = {243-257},
peerreviewed = {Yes},
publisher = {Springer},
title = {{Virtual} {Theories} -- {A} {Uniform} {Interface} to {Mathematical} {Knowledge} {Bases}},
year = {2017}
}
@inproceedings{faucris.111585584,
author = {Prodescu, Corneliu Claudiu and Kohlhase, Michael},
booktitle = {Symposium on Learning, Knowledge, and Adaptivity 2011, LWA 2011},
faupublication = {no},
pages = {257-264},
peerreviewed = {Yes},
title = {{Mathwebsearch} 0.5 an open formula search engine},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84874016713&origin=inward},
venue = {Magdeburg},
year = {2011}
}
@article{faucris.106204164,
author = {Huang, Xiaorong and Kerber, Manfred and Kohlhase, Michael and Melis, Erica and Richts, Jörn and Siekmann, Jörg and et al.},
author_hint = {Huang X., Kerber M., Kohlhase M., Melis E., Nesmith D., Richts J., Siekmann J.},
doi = {10.1007/s004500050036},
faupublication = {no},
journal = {Informatik - Forschung und Entwicklung},
pages = {20-26},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{The} proof development environment {Ω}-{MKRP}},
volume = {11},
year = {1996}
}
@inproceedings{faucris.111548624,
author = {Kohlhase, Michael and Schröder, Lutz and et al.},
author_hint = {Kohlhase M., Lemburg J., Schröder L., Schulz E.},
booktitle = {2nd World Congress on Formal Methods, FM 2009},
doi = {10.1007/978-3-642-05089-3_15},
faupublication = {yes},
isbn = {9783642050886},
pages = {223-238},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Formal} management of {CAD}/{CAM} processes},
venue = {Eindhoven},
year = {2009}
}
@inproceedings{faucris.214000221,
author = {Müller, Dennis and Wiesing, Tom and Thiery, Nicolas and Dehaye, Paul and Iancu, Mihnea and Kohlhase, Michael and Konovalov, Alexander and Lelièvre, Samuel and Pfeiffer, Markus and Rabe, Florian},
booktitle = {9th International Conference on Intelligent Computer Mathematics, CICM 2016},
doi = {10.1007/978-3-319-42547-4_9},
faupublication = {no},
isbn = {9783319425467},
pages = {117-131},
peerreviewed = {unknown},
publisher = {Springer Verlag},
title = {{Interoperability} in the {OpenDreamKit} project: {The} math-in-the-middle approach},
volume = {9791},
year = {2016}
}
@article{faucris.213996510,
abstract = {Mathematical models are the foundation of numerical simulation of optoelectronic devices. We present a concept for a machine-actionable as well as human-understandable representation of the mathematical knowledge they contain and the domainspecific knowledge they are based on. We propose to use theory graphs to formalize mathematical models and model pathway diagrams to visualize them. We illustrate our approach by application to the van Roosbroeck system describing the carrier transport in semiconductors by drift and diffusion. We introduce an approach for the block-based composition of models from simpler components.},
author = {Müller, Dennis and Kohlhase, Michael and Koprucki, Thomas and Tabelow, Karsten and Rabe, Florian},
doi = {10.1007/s11082-018-1321-7},
faupublication = {yes},
journal = {Optical and Quantum Electronics},
keywords = {Mathematical models;Research data;Model pathway diagrams;Drift-diffusion equations},
peerreviewed = {Yes},
title = {{Model} pathway diagrams for the representation of mathematical models},
volume = {50},
year = {2018}
}
@inproceedings{faucris.111692944,
author = {Benzmüller, Christoph and Huang, Xiaorong and Kohlhase, Michael and Melis, Erica and Siekmann, Jörg and Sorge, Volker and et al.},
author_hint = {Benzmüller C., Cheikhrouhou L., Fehrer D., Fiedler A., Huang X., Kerber M., Kohlhase M., Konrad K., Meier A., Melis E., Schaarschmidt W., Siekmann J., Sorge V.},
booktitle = {14th International Conference on Automated Deduction, CADE 1997},
faupublication = {no},
isbn = {9783540631040},
pages = {252-255},
peerreviewed = {Yes},
publisher = {Springer Verlag},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{ΩMEGA}: {Towards} a mathematical assistant},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84860987429&origin=inward},
volume = {1249},
year = {1997}
}
@inproceedings{faucris.214003582,
author = {Pollinger, Theresa and Kohlhase, Michael and Köstler, Harald},
booktitle = {11th International Conference on Intelligent Computer Mathematics, CICM 2018},
doi = {10.1007/978-3-319-96812-4_20},
faupublication = {yes},
isbn = {9783319968117},
pages = {232-247},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Knowledge} amalgamation for computational science and engineering},
year = {2018}
}
@inproceedings{faucris.214004132,
author = {Kohlhase, Michael and Betzendahl, Jonas},
booktitle = {11th International Conference on Intelligent Computer Mathematics, CICM 2018},
doi = {10.1007/978-3-319-96812-4_2},
faupublication = {yes},
isbn = {9783319968117},
pages = {7-22},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Translating} the {IMPS} theory library to {MMT}/{OMDoc}},
year = {2018}
}
@inproceedings{faucris.111731444,
author = {Codescu, Silvestru Mihai and Horozal, Fulya and Kohlhase, Michael and Mossakowski, Till and Rabe, Florian},
booktitle = {18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011},
doi = {10.1007/978-3-642-22673-1_24},
faupublication = {yes},
isbn = {9783642226724},
pages = {289-291},
peerreviewed = {Yes},
title = {{Project} abstract: {Logic} atlas and integrator ({LATIN})},
venue = {Bertinoro},
year = {2011}
}
@inproceedings{faucris.106426144,
author = {Ginev, Deyan and Jucovschi, Constantin and Anca, Stefan and Grigore, Mihai and David, Catalin and Kohlhase, Michael},
booktitle = {39th Jahrestagung der Gesellschaft fur Informatik e.V. (GI): Im Focus das Leben, INFORMATIK 2009 39th Annual Meeting of the German Informatics Society (GI): Focus on Life, INFORMATIK 2009},
faupublication = {no},
isbn = {9783885792482},
pages = {3147-3161},
peerreviewed = {Yes},
title = {{An} architecture for linguistic and semantic analysis on the {ARXMLIV} corpus},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84874316647&origin=inward},
venue = {Lubeck},
year = {2009}
}
@inproceedings{faucris.111606924,
author = {Kohlhase, Michael},
booktitle = {Joint of the 9th Workshop on Mathematical User Interfaces, MathUI 2014, 26th OpenMath Workshop, OpenMath 2014, 2014 Workshop on Theorem Proving Components for Educational Software, ThEdu 2014 and the Work in Progress Section of Conference on Intelligent Computer Mathematics, CICM 2014},
faupublication = {no},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{OpenMath} language extensions},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84924873356&origin=inward},
volume = {1186},
year = {2014}
}
@inproceedings{faucris.214004410,
author = {Wiesing, Tom and Kohlhase, Michael and Rabe, Florian},
booktitle = {7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017},
doi = {10.1007/978-3-319-72453-9_17},
faupublication = {yes},
isbn = {9783319724522},
pages = {243-257},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Virtual} theories – {A} uniform interface to mathematical knowledge bases},
year = {2017}
}
@inproceedings{faucris.111543564,
author = {Hambasan, Radu and Kohlhase, Michael},
booktitle = {Learning, Knowledge, Adaptation Workshops, LWA 2015: Knowledge Discovery, Data Mining and Machine Learning, KDML 2015, Knowledge Management, FGWM 2015, Information Retrieval, IR 2015 and Database Systems, FGDB 2015},
faupublication = {no},
pages = {33-44},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{Faceted} search for mathematics},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84944340107&origin=inward},
volume = {1458},
year = {2015}
}
@article{faucris.111691404,
author = {Kohlhase, Michael},
doi = {10.1007/s11786-008-0055-5},
faupublication = {no},
journal = {Mathematics in Computer Science},
keywords = {Elision; Knowledge representation; Semantics; Typography},
pages = {279-304},
peerreviewed = {unknown},
title = {{Using} {LATEX} as a semantic markup format},
volume = {2},
year = {2008}
}
@inproceedings{faucris.111742884,
author = {Kohlhase, Andrea and Kohlhase, Michael},
booktitle = {14th Symposium on Calculemus 2007 and 6th International Conference on Mathematical Knowledge Management, MKM 2007},
faupublication = {no},
isbn = {9783540730835},
pages = {313-326},
peerreviewed = {Yes},
title = {{Reexamining} the {MKM} value proposition: {From} math web search to math web research},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-38049042760&origin=inward},
venue = {Hagenberg},
year = {2007}
}
@inproceedings{faucris.111728144,
author = {Franke, Andreas and Kohlhase, Michael},
booktitle = {17th International Conference on Automated Deduction, CADE 2000},
faupublication = {no},
isbn = {9783540676645},
pages = {455-459},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{System} description: {MBASE}, an open mathematical knowledge base},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84937429345&origin=inward},
volume = {1831},
year = {2000}
}
@inproceedings{faucris.106432744,
author = {Kohlhase, Michael},
booktitle = {4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, TABLEAUX 1995},
faupublication = {no},
isbn = {9783540593386},
pages = {294-309},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Higher}-order tableaux},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84949190517&origin=inward},
volume = {918},
year = {1995}
}
@inproceedings{faucris.111713184,
author = {Acevedo, Carmela and Kohlhase, Michael},
booktitle = {Joint of the 9th Workshop on Mathematical User Interfaces, MathUI 2014, 26th OpenMath Workshop, OpenMath 2014, 2014 Workshop on Theorem Proving Components for Educational Software, ThEdu 2014 and the Work in Progress Section of Conference on Intelligent Computer Mathematics, CICM 2014},
faupublication = {no},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{Open} math map: {Interaction}},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84924891544&origin=inward},
volume = {1186},
year = {2014}
}
@inproceedings{faucris.106435384,
author = {Iancu, Mihnea and Kohlhase, Michael},
booktitle = {International Conference on Intelligent Computer Mathematics, CICM 2015},
doi = {10.1007/978-3-319-20615-8_12},
faupublication = {no},
isbn = {9783319206141},
pages = {187-202},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Math} literate knowledge management via induced material},
volume = {9150},
year = {2015}
}
@inproceedings{faucris.111730124,
author = {Davenport, James and Kohlhase, Michael},
booktitle = {16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009},
doi = {10.1007/978-3-642-02614-0_23},
faupublication = {no},
isbn = {9783642026133},
pages = {263-278},
peerreviewed = {Yes},
title = {{Unifying} math ontologies: {A} tale of two standards},
venue = {Grand Bend, ON},
year = {2009}
}
@article{faucris.106201744,
author = {Kohlhase, Michael and et al.},
author_hint = {Kohlhase M., Franke A.},
doi = {10.1006/jsco.2000.0468},
faupublication = {no},
journal = {Journal of Symbolic Computation},
pages = {365-402},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{MBase}: {Representing} knowledge and context for the integration of mathematical software systems},
volume = {32},
year = {2001}
}
@inproceedings{faucris.214000495,
author = {Müller, Dennis and Kohlhase, Michael and Rabe, Florian},
booktitle = {9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018},
doi = {10.1007/978-3-319-94205-6_38},
faupublication = {yes},
isbn = {9783319942049},
pages = {575-590},
peerreviewed = {unknown},
publisher = {Springer Verlag},
title = {{Theories} as {Types}},
year = {2018}
}
@inproceedings{faucris.109360504,
author = {Kohlhase, Michael and Koprucki, Thomas and Müller, Dennis and Tabelow, Karsten},
booktitle = {10th International Conference on Intelligent Computer Mathematics, CICM 2017},
doi = {10.1007/978-3-319-62075-6_16},
faupublication = {yes},
isbn = {9783319620749},
pages = {224-238},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Mathematical} models as research data via flexiformal theory graphs},
year = {2017}
}
@inproceedings{faucris.106427464,
author = {Kohlhase, Andrea and Kohlhase, Michael},
booktitle = {16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009},
doi = {10.1007/978-3-642-02614-0_29},
faupublication = {no},
isbn = {9783642026133},
pages = {357-372},
peerreviewed = {Yes},
title = {{Compensating} the computational bias of spreadsheets with {MKM} techniques},
venue = {Grand Bend, ON},
year = {2009}
}
@article{faucris.106203504,
author = {Kohlhase, Michael and Franke, Andreas},
doi = {10.1016/S1571-0661(05)80615-2},
faupublication = {no},
journal = {Electronic Notes in Theoretical Computer Science},
pages = {451-468},
peerreviewed = {Yes},
title = {{MBase}: {Representing} mathematical knowledge in a relational data base},
volume = {23},
year = {1999}
}
@inproceedings{faucris.106424384,
author = {David, Catalin and Ginev, Deyan and Kohlhase, Michael and Matican, Bogdan and et al.},
author_hint = {David C., Ginev D., Kohlhase M., Matican B., Mirea S.},
booktitle = {1st Workshop on Semantic Publishing 2011, SePublica 2011 - Co-located with the 8th Extended Semantic Web Conference, ESWC 2011},
faupublication = {no},
pages = {18-29},
peerreviewed = {Yes},
publisher = {CEUR-WS},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{A} framework for semantic publishing of modular content objects},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84890730016&origin=inward},
venue = {Hersonissos, Crete},
volume = {721},
year = {2011}
}
@article{faucris.111160544,
author = {Kohlhase, Michael and Benzmüller, Christoph and Brown, Chad},
doi = {10.2178/jsl/1102022211},
faupublication = {no},
journal = {Journal of Symbolic Logic},
pages = {1027-1088},
peerreviewed = {Yes},
title = {{Higher}-order semantics and extensionality},
volume = {69},
year = {2004}
}
@inproceedings{faucris.106423284,
author = {Iancu, Mihnea and Kohlhase, Michael},
booktitle = {International Conference on Intelligent Computer Mathematics, CICM 2015},
doi = {10.1007/978-3-319-20615-8_9},
faupublication = {no},
isbn = {9783319206141},
pages = {137-152},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{A} flexiformal model of knowledge dissemination and aggregation in mathematics},
volume = {9150},
year = {2015}
}
@inproceedings{faucris.120851544,
author = {Kohlhase, Michael},
booktitle = {Lernen, Wissen, Daten, Analyse - 2017 Learning. Knowledge. Data. Analytics, LWDA 2017},
faupublication = {yes},
pages = {241-252},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{Math} object identifiers - {Towards} research data in mathematics},
url = {https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85030126012&origin=inward},
venue = {Rostock},
volume = {1917},
year = {2017}
}
@inproceedings{faucris.111169784,
author = {Rabe, Florian and Kohlhase, Michael},
booktitle = {LPAR 2008 Workshops on Knowledge Exchange: Automated Provers and Proof Assistants, KEAPPA 2008 and the 7th International Workshop on the Implementation of Logics, IWIL 2008},
faupublication = {no},
pages = {50-66},
peerreviewed = {Yes},
title = {{An} exchange format for modular knowledge},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84885598893&origin=inward},
venue = {Doha},
volume = {418},
year = {2008}
}
@inproceedings{faucris.111673584,
author = {Kohlhase, Michael and Zholudev, Vyacheslav},
booktitle = {Balisage: The Markup Conference 2009},
doi = {10.4242/BalisageVol3.Zholudev01},
faupublication = {no},
isbn = {9780982434420},
peerreviewed = {Yes},
title = {{TNTBase}: {Versioned} storage for {XML}},
venue = {Montreal, QC},
volume = {3},
year = {2009}
}
@article{faucris.106187004,
author = {Müller, Christine and Kohlhase, Michael},
doi = {10.1080/10580530903017583},
faupublication = {no},
journal = {Information Systems Management},
keywords = {Mathematical knowledge management; Practice-oriented hypermedia adaptation; User modeling},
pages = {215-230},
peerreviewed = {Yes},
title = {{Context}-aware adaptation: {A} case study on mathematical notations},
volume = {26},
year = {2009}
}
@inproceedings{faucris.106441104,
author = {Carette, Jacques and Farmer, William and Kohlhase, Michael},
booktitle = {2014 International Conference on Intelligent Computer Mathematics, CICM 2014},
doi = {10.1007/978-3-319-08434-3_19},
faupublication = {no},
isbn = {9783319084336},
pages = {252-266},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Realms}: {A} structure for consolidating knowledge about mathematical theories},
venue = {Coimbra},
year = {2014}
}
@inproceedings{faucris.106443524,
author = {Kohlhase, Michael and Benzmüller, Christoph},
booktitle = {15th International Conference on Automated Deduction, CADE 1998},
faupublication = {no},
isbn = {9783540646754},
pages = {139-143},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{System} description: {Leo}— {A} higher-order theorem prover},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84872799915&origin=inward},
volume = {1421},
year = {1998}
}
@inproceedings{faucris.106430984,
author = {Normann, Immanuel and Kohlhase, Michael},
booktitle = {14th Symposium on Calculemus 2007 and 6th International Conference on Mathematical Knowledge Management, MKM 2007},
faupublication = {no},
isbn = {9783540730835},
pages = {356-370},
peerreviewed = {Yes},
title = {{Extended} formula normalization for e-retrieval and sharing of mathematical knowledge},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-38049028250&origin=inward},
venue = {Hagenberg},
year = {2007}
}
@inproceedings{faucris.111208944,
author = {Luzhnica, Enxhell and Kohlhase, Michael},
booktitle = {5th International Conference on Mathematical Software, ICMS 2016},
doi = {10.1007/978-3-319-42432-3_60},
faupublication = {no},
isbn = {9783319424316},
pages = {467-475},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Formula} semantification and automated relation finding in the on-line encyclopedia for integer sequences},
volume = {9725},
year = {2016}
}
@inproceedings{faucris.106434944,
author = {Kohlhase, Michael and Mahnke, Achim and Müller, Christine},
booktitle = {Workshop on Learning, Knowledge, and Adaptivity, LWA 2007},
faupublication = {no},
isbn = {9783860109076},
pages = {324-329},
peerreviewed = {Yes},
title = {{Managing} variants in document content and narrative structures},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84869721576&origin=inward},
venue = {Halle},
year = {2007}
}
@article{faucris.106163464,
author = {Kerber, Manfred and Kohlhase, Michael},
doi = {10.1080/11663081.2012.705962},
faupublication = {no},
journal = {Journal of Applied Non-Classical Logics},
keywords = {many-valued logics; presuppositions; resolution calculus; undefinedness},
pages = {295-317},
peerreviewed = {Yes},
title = {{Reasoning} without believing: {On} the mechanisation of presuppositions and partiality},
volume = {22},
year = {2012}
}
@book{faucris.119542104,
author = {Kohlhase, Michael},
faupublication = {no},
month = {Jan},
pages = {1-+},
peerreviewed = {Yes},
title = {{OMDoc} - {An} open markup format for mathematical documents [version 1.2]},
volume = {4180},
year = {2006}
}
@inproceedings{faucris.213997567,
author = {Kohlhase, Andrea and Kohlhase, Michael and Ouypornkochagorn, Taweechai},
booktitle = {11th International Conference on Intelligent Computer Mathematics, CICM 2018},
doi = {10.1007/978-3-319-96812-4_14},
faupublication = {yes},
isbn = {9783319968117},
pages = {147-163},
peerreviewed = {unknown},
publisher = {Springer Verlag},
title = {{Discourse} phenomena in mathematical documents},
year = {2018}
}
@inproceedings{faucris.111634864,
author = {Iancu, Mihnea and Kohlhase, Michael and Prodescu, Corneliu Claudiu},
booktitle = {4th International Congress on Mathematical Software, ICMS 2014},
doi = {10.1007/978-3-662-44199-2_5},
faupublication = {no},
isbn = {9783662441985},
pages = {26-30},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Representing}, archiving, and searching the space of mathematical knowledge},
venue = {Seoul},
year = {2014}
}
@inproceedings{faucris.106181724,
author = {Kohlhase, Michael},
booktitle = {14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012},
doi = {10.1109/SYNASC.2012.78},
faupublication = {no},
isbn = {9780769549347},
pages = {30-35},
peerreviewed = {Yes},
title = {{The} flexiformalist manifesto},
venue = {Timisoara},
year = {2012}
}
@inproceedings{faucris.111163404,
author = {Kohlhase, Michael and Urban, Josef and et al.},
author_hint = {Alama J., Kohlhase M., Mamane L., Naumowicz A., Rudnicki P., Urban J.},
booktitle = {18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011},
doi = {10.1007/978-3-642-22673-1_11},
faupublication = {no},
isbn = {9783642226724},
keywords = {formal mathematics; free culture; free licensing; mizar; open data},
pages = {149-163},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Licensing} the {Mizar} mathematical library},
venue = {Bertinoro},
year = {2011}
}
@inproceedings{faucris.106430104,
author = {Kohlhase, Michael and Iancu, Mihnea},
booktitle = {4th International Congress on Mathematical Software, ICMS 2014},
doi = {10.1007/978-3-662-44199-2_7},
faupublication = {no},
isbn = {9783662441985},
pages = {36-40},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Discourse}-level parallel markup and meaning adoption in flexiformal theory graphs},
venue = {Seoul},
year = {2014}
}
@inproceedings{faucris.111164504,
author = {Dörrie, Jan Wilken and Kohlhase, Michael},
booktitle = {Joint Workshops of the 8th Workshop on Mathematical User Interfaces, MathUI 2013, 25th OpenMath Workshop, OpenMath 2013, 5th International Workshop on Programming Languages for Mechanised Mathematical Systems, PLMMS 2013 and the 2nd International Workshop on Theorem Proving Components for Educational Software, ThEdu 2013 and Work in Progress at Conference on Intelligent Computer Mathematics, CICM 2013},
faupublication = {no},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{OpenMathMap}: {Accessing} {Math} via {Interactive} {Maps}},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84924872163&origin=inward},
volume = {1010},
year = {2013}
}
@inproceedings{faucris.121785224,
abstract = {Among the standard stages of the engineering design process, the principle solution can be regarded as an analogue of the design specification, fixing the way the final product works. It is usually constructed as an abstract sketch where the functional parts of the product are identified, and geometric and topological constraints are formulated. Here, we outline a semantic approach where the principle solution is annotated with ontological assertions, thus making the intended requirements explicit and available for further machine processing; this includes the automated detection of design errors in the final CAD model, making additional use of a background ontology of engineering knowledg},
author = {Breitsprecher, Thilo and Codesci, Mihai and Jucovaschi, Constantin and Kohlhase, Michael and Schröder, Lutz and Wartzack, Sandro},
booktitle = {8th International Conference on Formal Ontology in Information Systems},
doi = {10.3233/978-1-61499-438-1-427},
faupublication = {yes},
keywords = {document-oriented processes; Knowledge-based engineering},
note = {UnivIS-Import:2015-04-16:Pub.2014.tech.FT.FT-KLMEFK.toward_5},
pages = {427-432},
peerreviewed = {Yes},
publisher = {IOS Press},
title = {{Towards} {Ontological} {Support} for {Principle} {Solutions} in {Mechanical} {Engineering}},
venue = {Rio de Janeiro},
year = {2014}
}
@inproceedings{faucris.111729684,
author = {Rabe, Florian and Kohlhase, Michael and Sacerdoti Coen, Claudio},
booktitle = {18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011},
doi = {10.1007/978-3-642-22673-1_8},
faupublication = {no},
isbn = {9783642226724},
pages = {107-122},
peerreviewed = {Yes},
title = {{A} foundational view on integration problems},
venue = {Bertinoro},
year = {2011}
}
@inproceedings{faucris.106443964,
author = {Zimmer, Jürgen and Kohlhase, Michael},
booktitle = {18th International Conference on Automated Deduction, CADE 2002},
faupublication = {no},
isbn = {9783540439318},
pages = {139-143},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{System} description: {The} mathweb software bus for distributed mathematical reasoning},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84948958841&origin=inward},
volume = {2392},
year = {2002}
}
@inproceedings{faucris.106431864,
author = {Kohlhase, Michael},
booktitle = {Joint of the 9th Workshop on Mathematical User Interfaces, MathUI 2014, 26th OpenMath Workshop, OpenMath 2014, 2014 Workshop on Theorem Proving Components for Educational Software, ThEdu 2014 and the Work in Progress Section of Conference on Intelligent Computer Mathematics, CICM 2014},
faupublication = {no},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{Extension} proposal: {Records} in pragmatic open math},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84924891647&origin=inward},
volume = {1186},
year = {2014}
}
@inproceedings{faucris.109595244,
author = {Koprucki, Thomas and Kohlhase, Michael and Müller, Dennis and Tabelow, Karsten},
booktitle = {17th International Conference on Numerical Simulation of Optoelectronic Devices, NUSOD 2017},
doi = {10.1109/NUSOD.2017.8010073},
faupublication = {yes},
isbn = {9781509053230},
pages = {225-226},
peerreviewed = {Yes},
publisher = {IEEE Computer Society},
title = {{Mathematical} models as research data in numerical simulation of opto-electronic devices},
year = {2017}
}
@inproceedings{faucris.106445284,
author = {Kohlhase, Michael and et al.},
author_hint = {Johann P., Kohlhase M.},
booktitle = {12th International Conference on Automated Deduction, CADE-12 1994},
faupublication = {no},
isbn = {9783540581567},
pages = {620-634},
peerreviewed = {unknown},
publisher = {Springer Verlag},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Unification} in an extensional lambda calculus with ordered function sorts and constant overloading},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84945308194&origin=inward},
year = {1994}
}
@inproceedings{faucris.111175284,
author = {Lange-Bever, Christoph and Kohlhase, Michael and et al.},
author_hint = {Dumitrache A., Lange C., Kohlhase M., Aschenbeck N.},
booktitle = {5th Workshop on Semantic Wikis - Linking Data and People, SemWiki 2010 - 7th Extended Semantic Web Conference, ESWC 2010},
faupublication = {no},
pages = {175-177},
peerreviewed = {Yes},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Prototyping} a browser for a listed buildings database* with semantic {MediaWiki}},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84873471498&origin=inward},
venue = {Hersonissos, Heraklion, Crete},
volume = {632},
year = {2010}
}
@inproceedings{faucris.106425264,
author = {Lange-Bever, Christoph and Kohlhase, Michael},
booktitle = {16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009},
doi = {10.1007/978-3-642-02614-0_31},
faupublication = {no},
isbn = {9783642026133},
pages = {389-404},
peerreviewed = {Yes},
title = {{A} mathematical approach to ontology authoring and documentation},
venue = {Grand Bend, ON},
year = {2009}
}
@inproceedings{faucris.111742664,
author = {Kaliszyk, Cezary and Kohlhase, Michael and Müller, Dennis and Rabe, Florian},
booktitle = {2016 Joint Formal Mathematics for Mathematicians, FM4M 2016, 11th Workshop on Mathematical User Interfaces, MathUI 2016, and 2016 Workshop on Theorem Proving Components for Educational Software, ThEdu 2016, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS-WIP 2016},
faupublication = {yes},
pages = {229-244},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{A} standard for aligning mathematical concepts},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-85018973947&origin=inward},
volume = {1785},
year = {2017}
}
@inproceedings{faucris.110974864,
author = {Ginev, Deyan and Stamerjohanns, Heinrich and Kohlhase, Michael and Miller, Bruce},
booktitle = {Symposium on Learning, Knowledge, and Adaptivity 2011, LWA 2011},
faupublication = {no},
month = {Jan},
pages = {292-294},
peerreviewed = {Yes},
title = {{The} {LaTeXML} daemon: {Editable} math on the collaborative web},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84874005493&origin=inward},
venue = {Magdeburg},
year = {2011}
}
@inproceedings{faucris.106549124,
author = {Kohlhase, Michael and Kohlhase, Andrea and Fürsich, Michael},
booktitle = {10th International Conference on Intelligent Computer Mathematics, CICM 2017},
doi = {10.1007/978-3-319-62075-6_15},
faupublication = {yes},
isbn = {9783319620749},
pages = {208-223},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Visual} structure in mathematical expressions},
year = {2017}
}
@inproceedings{faucris.111738044,
author = {Kohlhase, Michael and Mance, Felix and Rabe, Florian},
booktitle = {Conference on Intelligent Computer Mathematics, CICM 2013, Co-located with the MKM 2013, Calculemus 2013, DML 2013, and Systems and Projects 2013},
doi = {10.1007/978-3-642-39320-4_6},
faupublication = {no},
isbn = {9783642393198},
pages = {82-97},
peerreviewed = {Yes},
title = {{A} universal machine for biform theory graphs},
venue = {Bath},
year = {2013}
}
@inproceedings{faucris.106425924,
author = {Kerber, Manfred and Kohlhase, Michael},
booktitle = {12th International Conference on Automated Deduction, CADE-12 1994},
faupublication = {no},
isbn = {9783540581567},
pages = {371-385},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{A} mechanization of strong {Kleene} logic for partial functions},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84956993662&origin=inward},
year = {1994}
}
@inproceedings{faucris.106444844,
author = {Kohlhase, Michael and Rabe, Florian and Zholudev, Vyacheslav},
booktitle = {10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010},
doi = {10.1007/978-3-642-14128-7_32},
faupublication = {no},
isbn = {9783642141270},
pages = {370-384},
peerreviewed = {Yes},
title = {{Towards} {MKM} in the large: {Modular} representation and scalable software architecture},
venue = {Paris},
year = {2010}
}
@inproceedings{faucris.111694264,
author = {Huang, Xiaorong and Kerber, Manfred and Kohlhase, Michael and Melis, Erica and Siekmann, Jörg and et al.},
author_hint = {Huang X., Kerber M., Kohlhase M., Melis E., Nesmith D., Richts J., Siekmann J.},
booktitle = {12th International Conference on Automated Deduction, CADE-12 1994},
faupublication = {no},
isbn = {9783540581567},
pages = {788-792},
peerreviewed = {Yes},
publisher = {Springer Verlag},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Ω}-{MKRP}: {A} proof development environment},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84961346097&origin=inward},
year = {1994}
}
@inproceedings{faucris.118780904,
author = {Breitsprecher, Thilo and Codescu, Silvestru Mihai and Schröder, Lutz and Wartzack, Sandro and jucovschi, Constantin and Kohlhase, Michael},
booktitle = {In Proc. 13th International Design Conference, DESIGN 2014},
faupublication = {yes},
keywords = {design knowledge;ontology;semantics in product development},
note = {UnivIS-Import:2015-04-17:Pub.2014.tech.IMMD.profes_1.semant},
pages = {1723-1732},
peerreviewed = {Yes},
publisher = {Faculty of Mechanical Engineering and Naval Architecture},
series = {DESIGN},
title = {{Semantic} {Support} for {Engineering} {Design} {Processes}},
url = {https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=84924387161&origin=inward},
venue = {Dubrovnik},
year = {2014}
}
@inproceedings{faucris.106427244,
author = {Horozal, Fulya and Iacob, Alin and Jucovschi, Constantin and Kohlhase, Michael and Rabe, Florian},
booktitle = {18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011},
doi = {10.1007/978-3-642-22673-1_15},
faupublication = {no},
isbn = {9783642226724},
pages = {212-227},
peerreviewed = {Yes},
title = {{Combining} source, content, presentation, narration, and relational representation},
venue = {Bertinoro},
year = {2011}
}
@article{faucris.106182384,
author = {Kohlhase, Michael and Rabe, Florian},
doi = {10.1007/s11786-012-0113-x},
faupublication = {no},
journal = {Mathematics in Computer Science},
keywords = {MathML; OpenMath; Semantics},
pages = {235-260},
peerreviewed = {Yes},
title = {{Semantics} of {OpenMath} and {MathML3}},
volume = {6},
year = {2012}
}
@inproceedings{faucris.111597024,
author = {Kohlhase, Michael and et al.},
author_hint = {Toloaca I., Kohlhase M.},
booktitle = {MathUI 2016},
faupublication = {no},
pages = {73-81},
peerreviewed = {unknown},
publisher = {CEUR-WS},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Notation}-based semantification},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-85018973557∨igin=inward},
volume = {1785},
year = {2017}
}
@inproceedings{faucris.119603044,
author = {Kohlhase, Michael and Müller, Dennis and Rabe, Florian and Kaliszyk, Cezary and Gauthier, Thibault},
booktitle = {10th International Conference on Intelligent Computer Mathematics, CICM 2017},
doi = {10.1007/978-3-319-62075-6_7},
faupublication = {yes},
isbn = {9783319620749},
pages = {83-98},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Classification} of alignments between concepts of formal mathematical systems},
year = {2017}
}
@inproceedings{faucris.106185464,
author = {Kohlhase, Michael and Kohlhase, Andrea},
booktitle = {29th ACM International Conference on Design of Communication, SIGDOC'11},
doi = {10.1145/2038476.2038512},
faupublication = {no},
isbn = {9781450309363},
keywords = {flexiforms; formality; formalization; informality; knowledge management},
pages = {181-188},
peerreviewed = {unknown},
title = {{Towards} a flexible notion of document context},
venue = {Pisa},
year = {2011}
}
@inproceedings{faucris.214003303,
author = {Kohlhase, Michael and Kohlhase, Andrea and Ouypornkochagorn, Taweechai},
booktitle = {11th International Conference on Intelligent Computer Mathematics, CICM 2018},
doi = {10.1007/978-3-319-96812-4_14},
faupublication = {yes},
isbn = {9783319968117},
pages = {147-163},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Discourse} phenomena in mathematical documents},
year = {2018}
}
@inproceedings{faucris.120849344,
author = {Kohlhase, Michael and Müller, Dennis and Owre, Sam and Rabe, Florian},
booktitle = {8th International Conference on Interactive Theorem Proving, ITP 2017},
doi = {10.1007/978-3-319-66107-0_21},
faupublication = {yes},
isbn = {9783319661063},
pages = {319-335},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Making} {PVS} accessible to generic services by interpretation in a universal format},
year = {2017}
}
@book{faucris.111555004,
editor = {Bos, Johan and Kohlhase, Michael},
faupublication = {no},
pages = {381-384},
peerreviewed = {automatic},
publisher = {OXFORD UNIV PRESS},
title = {{ICoS}-2 {Inference} in {Computational} {Semantics}. {Workshop} {Proceedings}},
volume = {11},
year = {2000}
}
@inproceedings{faucris.119978804,
author = {Kohlhase, Michael and Müller, Dennis and Pfeiffer, Markus and Rabe, Florian and Thiery, Nicolas and Vasilyev, Victor and Wiesing, Tom},
booktitle = {MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences},
editor = {Johannes Blömer and Temur Kutsia and Dimitris Simos},
faupublication = {yes},
pages = {195-210},
peerreviewed = {Yes},
publisher = {Springer},
title = {{Knowledge}-{Based} {Interoperability} for {Mathematical} {Software} {Systems}},
year = {2017}
}
@inproceedings{faucris.106445504,
author = {Kohlhase, Michael and et al.},
author_hint = {Wolska M., Grigore M., Kohlhase M.},
booktitle = {4th Workshop Towards a Digital Mathematics Library, DML 2011},
faupublication = {no},
isbn = {9788021055421},
pages = {85-101},
peerreviewed = {Yes},
publisher = {Masaryk University},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Using} discourse context to interpret object-denoting mathematical expressions},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84870532306&origin=inward},
year = {2011}
}
@inproceedings{faucris.111153724,
author = {Kohlhase, Michael and Kohlhase, Andrea},
booktitle = {LWA 2009 - Workshop-Woche: Lernen-Wissen-Adaptivitat - Learning, Knowledge and Adaptivity},
faupublication = {no},
pages = {22-29},
peerreviewed = {Yes},
title = {{What} you understand is what you get: {Assessment} in spreadsheets},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84874134110&origin=inward},
venue = {Darmstadt},
year = {2009}
}
@article{faucris.111664124,
author = {Iancu, Mihnea and Kohlhase, Michael and Rabe, Florian and Urban, Josef},
doi = {10.1007/s10817-012-9271-4},
faupublication = {no},
journal = {Journal of Automated Reasoning},
keywords = {Logical frameworks; Math search; Mizar; OMDoc; Representation; Translation},
pages = {191-202},
peerreviewed = {Yes},
title = {{The} {Mizar} mathematical library in {OMDoc}: {Translation} and applications},
volume = {50},
year = {2013}
}
@inproceedings{faucris.111704384,
author = {Kohlhase, Michael},
booktitle = {5th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2000},
faupublication = {no},
isbn = {9783540449904},
pages = {32-52},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{OMDoc}: {Towards} an internet standard for the administration, distribution, and teaching of mathematical knowledge},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84974687882&origin=inward},
volume = {1930},
year = {2001}
}
@inproceedings{faucris.111653564,
author = {Kohlhase, Lukas and Kohlhase, Michael},
booktitle = {2014 International Conference on Intelligent Computer Mathematics, CICM 2014},
doi = {10.1007/978-3-319-08434-3_35},
faupublication = {no},
isbn = {9783319084336},
pages = {440-443},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{System} description: {A} semantics-aware {LATEX}-to-office converter},
venue = {Coimbra},
year = {2014}
}
@inproceedings{faucris.111724184,
author = {Hambasan, Radu and Kohlhase, Michael},
booktitle = {6th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2015},
doi = {10.1007/978-3-319-32859-1_35},
faupublication = {no},
isbn = {9783319328584},
pages = {406-420},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Faceted} search for mathematics},
volume = {9582},
year = {2016}
}
@inproceedings{faucris.111538724,
author = {Benzmüller, Christoph and Kohlhase, Michael},
booktitle = {15th International Conference on Automated Deduction, CADE 1998},
faupublication = {no},
isbn = {9783540646754},
pages = {56-71},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Extensional} higher-order resolution},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84858341103&origin=inward},
volume = {1421},
year = {1998}
}
@inproceedings{faucris.111702844,
author = {Jucovschi, Constantin and Kohlhase, Michael},
booktitle = {10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010},
doi = {10.1007/978-3-642-14128-7_29},
faupublication = {no},
isbn = {9783642141270},
pages = {336-344},
peerreviewed = {Yes},
title = {{STEXIDE}: {An} integrated development environment for {STEX} collections},
venue = {Paris},
year = {2010}
}
@inproceedings{faucris.106185684,
author = {Kohlhase, Michael and Zholudev, Vyacheslav},
booktitle = {Balisage: The Markup Conference 2010},
doi = {10.4242/BalisageVol5.Zholudev01},
faupublication = {no},
isbn = {9781935958017},
peerreviewed = {Yes},
title = {{Scripting} documents with {XQuery}: {Virtual} documents in {TNTBase}},
venue = {Montreal, QC},
volume = {5},
year = {2010}
}
@inproceedings{faucris.111621444,
author = {Kohlhase, Michael and Siekmann, Jörg and Benzmüller, Christoph and Franke, Andreas and Melis, Erica and Normann, Immanuel and Sorge, Volker and et al.},
author_hint = {Siekmann J., Benzmüller C., Brezhnev V., Cheikhrouhou L., Fiedler A., Franke A., Horacek H., Kohlhase M., Meier A., Melis E., Moschner M., Normann I., Pollet M., Sorge V., Ullrich C., Wirth C., Zimmer J.},
booktitle = {18th International Conference on Automated Deduction, CADE 2002},
faupublication = {no},
isbn = {9783540439318},
pages = {144-149},
peerreviewed = {Yes},
publisher = {Springer Verlag},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Proof} development with {Ωmega}},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84948980176&origin=inward},
volume = {2392},
year = {2002}
}
@inproceedings{faucris.119973964,
author = {Kohlhase, Michael and Müller, Dennis and Rochau, Denis},
booktitle = {2016 Joint Formal Mathematics for Mathematicians, FM4M 2016, 11th Workshop on Mathematical User Interfaces, MathUI 2016, and 2016 Workshop on Theorem Proving Components for Educational Software, ThEdu 2016, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS-WIP 2016},
faupublication = {no},
pages = {245-259},
peerreviewed = {Yes},
publisher = {CEUR-WS},
title = {{FrameIT} reloaded: {Serious} math games from modular math ontologies},
volume = {1785},
year = {2017}
}
@inproceedings{faucris.106444624,
author = {Kohlhase, Michael},
booktitle = {Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012},
doi = {10.1007/978-3-642-31374-5_34},
faupublication = {no},
isbn = {9783642313738},
pages = {448-452},
peerreviewed = {Yes},
title = {{The} {Planetary} project: {Towards} {eMath3}.0},
venue = {Bremen},
year = {2012}
}
@inproceedings{faucris.106439784,
author = {Kohlhase, Michael and Müller, Christine},
booktitle = {Workshop on Learning, Knowledge, and Adaptivity, LWA 2007},
faupublication = {no},
isbn = {9783860109076},
pages = {318-323},
peerreviewed = {Yes},
title = {{Panta} rhei},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84874010902&origin=inward},
venue = {Halle},
year = {2007}
}
@inproceedings{faucris.106431204,
author = {Horozal, Fulya and Kohlhase, Michael and Rabe, Florian},
booktitle = {Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012},
doi = {10.1007/978-3-642-31374-5_5},
faupublication = {no},
isbn = {9783642313738},
pages = {65-80},
peerreviewed = {Yes},
title = {{Extending} {MKM} formats at the statement level},
venue = {Bremen},
year = {2012}
}
@inproceedings{faucris.111515624,
abstract = {The material presented in this paper is a first exploratory step towards the definition of the interaction level in OMRS, supplies a concrete syntax based on the OPENMATH standard, and gives a semantics to communication of mathematical services in distributed theorem proving and symbolic computation environments.},
author = {Kohlhase, Michael and Armando, Alessandro and Ranise, Silvio},
faupublication = {no},
month = {Jan},
pages = {33-48},
peerreviewed = {Yes},
title = {{Communication} {Protocols} for mathematical services based on {KQML} and {OMRS}},
year = {2001}
}
@inproceedings{faucris.106432084,
author = {Horozal, Fulya and Rabe, Florian and Kohlhase, Michael},
booktitle = {2014 International Conference on Intelligent Computer Mathematics, CICM 2014},
doi = {10.1007/978-3-319-08434-3_23},
faupublication = {no},
isbn = {9783319084336},
pages = {312-327},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Flexary} operators for formalized mathematics},
venue = {Coimbra},
year = {2014}
}
@inproceedings{faucris.111275604,
author = {Hilf, Eberhard and Kohlhase, Michael and Stamerjohanns, Heinrich},
booktitle = {5th International Conference on Mathematical Knowledge Management, MKM 2006},
faupublication = {no},
isbn = {9783540371045},
pages = {165-178},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{Capturing} the content of physics: {Systems}, observables, and experiments},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-33749546748&origin=inward},
venue = {Wokingham},
year = {2006}
}
@inproceedings{faucris.111529924,
author = {Kohlhase, Michael and Kohlhase, Andrea},
faupublication = {no},
pages = {175-189},
peerreviewed = {Yes},
title = {{CPOINT}: {Dissolving} the author's dilemma},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-35048892955&origin=inward},
volume = {3119},
year = {2004}
}
@inproceedings{faucris.111168024,
author = {Iancu, Mihnea and Jucovschi, Constantin and Kohlhase, Michael and Wiesing, Tom},
booktitle = {2014 International Conference on Intelligent Computer Mathematics, CICM 2014},
doi = {10.1007/978-3-319-08434-3_33},
faupublication = {no},
isbn = {9783319084336},
pages = {431-434},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{System} description: {MathHub}.info},
venue = {Coimbra},
year = {2014}
}
@inproceedings{faucris.111775004,
abstract = {We describe the API and the functionality needed to realize a CVS-like version control and distribution model. This architecture extends the CVS architecture in two ways, motivated by the specific needs of distributed management of structured mathematical knowledge on the Internet. On the one hand the one-level client/server model of CVS is generalized to a multi-level graph of client/server relations, and on the other hand the underlying change-detection tools take the math-specific structure of the data into account.},
author = {Kohlhase, Michael and Anghelache, Romeo},
faupublication = {no},
month = {Jan},
pages = {147-161},
peerreviewed = {Yes},
title = {{Towards} collaborative content management and version control for structured mathematical knowledge},
volume = {2594},
year = {2003}
}
@inproceedings{faucris.106424164,
author = {Kohlhase, Michael},
booktitle = {2014 International Conference on Intelligent Computer Mathematics, CICM 2014},
doi = {10.1007/978-3-319-08434-3_13},
faupublication = {no},
isbn = {9783319084336},
pages = {169-183},
peerreviewed = {Yes},
publisher = {Springer Verlag},
title = {{A} data model and encoding for a semantic, multilingual terminology of mathematics},
venue = {Coimbra},
year = {2014}
}
@inproceedings{faucris.111676004,
author = {Müller, Christine and Kohlhase, Michael},
booktitle = {1st World Summit on the Knowledge Society, WSKS 2008},
doi = {10.1007/978-3-540-87781-3_5},
faupublication = {no},
isbn = {9783540877806},
pages = {41-50},
peerreviewed = {Yes},
title = {{Towards} a community of practice toolkit based on semantically marked up artifacts},
venue = {Athens},
year = {2008}
}
@inproceedings{faucris.223104396,
abstract = {Mathematical software systems offer two major paradigms for interacting with mathematical knowledge. One is static files with semantically annotated representations that define mathematical knowledge and can be compiled into documents (PDF, html, etc.), and the other dynamically build mathematical objects in interactive read-eval-print loops (REPL) such as notebooks. Many author-facing interfaces offer both features in some way. However, reader-facing interfaces usually show only one or the other. In this paper we present an integration of the approaches in the context of the MMT system. Firstly, we present a Jupyter kernel for MMT which provides web-ready REPL functionality for MMT. Secondly, we integrate the resulting Jupyter notebooks into MathHub, a web-based frontend for mathematical documents. This allows users to context-sensitively open a Jupyter notebook as a dynamic subdocument anywhere inside a static MathHub document. Vice versa, any such highly interactive and often ephemeral notebook can be saved persistently in the MathHub backend at which point it becomes available as a static document. We also show how Jupyter widgets can be deeply integrated with the MMT knowledge management facilities to give semantics-aware interaction facilities.},
author = {Amann, Kai and Kohlhase, Michael and Rabe, Florian and Wiesing, Tom},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
date = {2019-07-08/2019-07-12},
doi = {10.1007/978-3-030-23250-4_19},
editor = {Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk},
faupublication = {yes},
isbn = {9783030232498},
note = {CRIS-Team Scopus Importer:2019-07-26},
pages = {275-290},
peerreviewed = {unknown},
publisher = {Springer Verlag},
title = {{Integrating} {Semantic} {Mathematical} {Documents} and {Dynamic} {Notebooks}},
venue = {Prague},
volume = {11617 LNAI},
year = {2019}
}
@inproceedings{faucris.111736284,
author = {Kohlhase, Michael and Lange-Bever, Christoph},
booktitle = {1st Workshop on Semantic Wikis - From Wiki to Semantics, SemWiki 2006 - Co-located with the ESWC 2006},
faupublication = {no},
pages = {188-201},
peerreviewed = {Yes},
title = {{A} semantic wiki for mathematical knowledge management},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-84873470933&origin=inward},
venue = {Budva},
volume = {206},
year = {2006}
}
@inproceedings{faucris.106443304,
author = {Kohlhase, Michael and Lange-Bever, Christoph},
booktitle = {1st Workshop on Semantic Wikis},
doi = {10.4018/978-1-59904-877-2.ch004},
faupublication = {no},
isbn = {9781599048772},
pages = {47-68},
peerreviewed = {Yes},
publisher = {IGI Global},
title = {{SWiM}: {A} semantic wiki for mathematical knowledge management},
year = {2008}
}
@inproceedings{faucris.214003036,
author = {Wiesing, Tom and Kohlhase, Michael},
booktitle = {Proceedings of the Joint 2018 Computer Mathematics in Education - Enlightenment or Incantation},
faupublication = {yes},
peerreviewed = {No},
publisher = {CEUR-WS},
title = {{A} proposal for an {openMath} {JSON} encoding},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-85060579045∨igin=inward},
volume = {2307},
year = {2018}
}
@article{faucris.106203064,
author = {Hutter, Dieter and Kohlhase, Michael},
doi = {10.1023/A:1006282725324},
faupublication = {no},
journal = {Journal of Automated Reasoning},
pages = {123-164},
peerreviewed = {Yes},
title = {{Managing} structural information by higher-order colored unification},
volume = {25},
year = {2000}
}
@inproceedings{faucris.107138504,
author = {Müller, Dennis and Kohlhase, Michael and Rupprecht, Marcel},
booktitle = {CICM 2017},
faupublication = {yes},
peerreviewed = {unknown},
title = {{A} {Flexible}, {Interactive} {Theory}-{Graph} {Viewer}},
year = {2017}
}
@article{faucris.111267244,
author = {Franke, Andreas and Kohlhase, Michael and Sorge, Volker and et al.},
author_hint = {Franke A., Hess S., Jung C., Kohlhase M., Sorge V.},
faupublication = {no},
journal = {Journal of Universal Computer Science},
pages = {156-187},
peerreviewed = {unknown},
support_note = {Author relations incomplete. You may find additional data in field 'author_hint'},
title = {{Agent}-oriented integration of distributed mathematical services},
url = {https://www.scopus.com/record/display.uri?eid=2-s2.0-0001536634&origin=inward},
volume = {5},
year = {1999}
}