Publications

TitleAuthorsPublication Status
Injecting Formal Mathematics Into LaTeXD. Müller, M. KohlhaseCICM 2022
System Description: sTeX3 – A LaTeX-based Ecosystem for Semantic/Active Mathematical DocumentsM. Kohlhase, D. MüllerCICM 2022
sTeX3 – A LaTeX-based Ecosystem for Semantic/Active Mathematical DocumentsD. Müller, M. KohlhaseTUG 2022
Explaining Image Classifications with Near Misses, Near Hits and PrototypesM. Herchenbach, D. Müller, S. Scheele, U. SchmidICPRAI 2022
An Interactive Explanatory AI System for Industrial Quality ControlD. Müller, M. März, S. Scheele, U. SchmidAAAI 2022
Disambiguating Symbolic Expressions in Informal DocumentsD. Müller, C. KaliszykICLR 2021
Representing Structural Language Features in Formal Meta-languagesD. Müller, F. Rabe, C. R, M. KohlhaseCICM 2020
FrameIT: Detangling Knowledge Management from Game Design in Serious GamesM. Kohlhase, B. Bösl, R. Marcus, D. Müller, D. Rochau, N. Roux, J. Schihada, M. StammingerCICM 2020
The Space of Mathematical Software Systems — A Survey of Paradigmatic SystemsK. Bercic, J. Carette, W. Farmer, M. Kohlhase, D. Müller, F. Rabe, Y. SharodaPreprint (2020)
Mathematical Knowledge Management Across Formal LibrariesD. MüllerPh.D. Thesis (2019)
Relational Data Across Mathematical LibrariesA. Condoluci, M. Kohlhase, D. Müller, F. Rabe, C. Sacerdoti Coen, M. WenzelCICM 2019
The Coq Library as a Theory GraphD. Müller, F. Rabe, C. Sacerdoti CoenCICM 2019
Rapid Prototyping Formal Systems in MMTD. Müller, F. RabeLFMTP 2019
How to Leverage a Large Dataset of Formalized Mathematics with Machine Learning?D. Müller, F. Rabe, M. KohlhaseAITP 2019
Structuring Theories with Implicit MorphismsF. Rabe, D. MüllerWADT 2018
Automatically Finding Theory Morphisms for Knowledge ManagementD. Müller, M. Kohlhase, F. RabeCICM 2018
Theories as TypesD. Müller, F. Rabe, M. Kohlhase

IJCAR 2018

Model Pathway Diagrams for the Representation of Mathematical ModelsT. Koprucki, M. Kohlhase, K. Tabelow, D. Müller, F. RabeJournal of Optical and Quantum Electronics 50 (2018)
Knowledge-Based Interoperability for Mathematical Software SystemsM. Kohlhase, D. Müller, M. Pfeiffer, F. Rabe, N. Thiéry, V. Vasilyev, T. WiesingMACIS 2017
Alignment-based Translations Across Formal Systems Using
Interface Theories
D. Müller, C. Rothgang, Y. Liu, F. RabePxTP 2017
A Flexible, Interactive Theory-Graph ViewerM. Rupprecht, M. Kohlhase, D. MüllerCICM 2017
Making PVS accessible to generic services by interpretation in a universal formatM. Kohlhase, D. Müller, S. Owre, F. RabeITP 2017
Classification of alignments between concepts of formal mathematical systemsD. Müller, T. Gauthier, C. Kaliszyk, M. Kohlhase, F. RabeCICM 2017
Mathematical models as research data via flexiformal theory graphsM. Kohlhase, T. Kboprucki, D. Müller, K. TabelowCICM 2017
Interoperability in the OpenDreamKit Project: The Math-in-the-Middle ApproachP. Dehaye, M. Iancu, M. Kohlhase, A. Konovalov, S. Lelièvre, D. Müller, M. Pfeiffer, F. Rabe, N. Thiéry, T. WiesingCICM 2016
FrameIT Reloaded: Serious Math Games from Modular Math OntologiesD. Rochau, M. Kohlhase, D. MüllerCICM 2016
A Standard for Aligning Mathematical ConceptsC. Kaliszyk, M. Kohlhase, D. Müller, F. RabeCICM 2016
Understanding Mathematical Theory Formation via Theory Intersections in MMTD. Müller, M. KohlhaseCICM 2015
Knowledge Management across Formal LibrariesD. MüllerPh.D. Proposal
Die Konsistenz der P-Ideal-Dichotomie (German)D. MüllerM.Sc. Thesis
The model completion for the theory of Heyting algebrasD. MüllerB.Sc. Thesis

Unpublished old stuff; lecture scripts, summaries etc. (almost all in german):

ThemaTyp
ForcingEinführung
Abstract NonsenseMitschrift CdE Winterakademiekurs
Logik für Nicht-MathematikerEinführung
FunktionalanalysisZusammenfassung
Forcingaxiome – IdealdichotomienSeminarvortrag
Game Theory – Wadge and Lipschitz GamesSeminarvortrag
Mengenlehre und Große KardinalzahlenZusammenfassung
Große Kardinalzahlen – Unbeschreibbare KardinalzahlenSeminarvortrag
Mengenlehre (Vorlesung zu 0#)Vorlesungsmitschrift
Model Theory and ApplicationsVolesungsmitschrift
Modelltheorie I,IIZusammenfassung
Nichtstandard AnalysisVorlesungsmitschrift
Descriptive Set TheoryVorlesungsmitschrift
Kommutative AlgebraVorlesungsmitschrift
TopologieVorlesungsmitschrift
Logik – “Intuitionismus III – Modallogische Interpretation”Proseminarvortrag
Algebra und ZahlentheorieZusammenfassung
Analysis I,II,IIIZusammenfassung
Analysis IZusammenfassung
Lineare Algebra I,IIZusammenfassung
Experimentalphysik IIKlausurhilfe
Experimentalphysik IZusammenfassung

Insert math as
Block
Inline
Additional settings
Formula color
Text color
#333333
Type math using LaTeX
Preview
\({}\)
Nothing to preview
Insert