12 Result(s)

Article

Project VoLL-KI

“Learning from Learners” (“Von Lernenden Lernen”, “VoLL-KI ” for short) is a is collaborative research project with the goal of creating a practical toolbox of instruments at different levels of abstraction to...

Michael Kohlhase, Marc Berges, Jens Grubert, Andreas Henrich… in KI - Künstliche Intelligenz (2024)

Article

Experiences from Exporting Major Proof Assistant Libraries

The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the l...

Michael Kohlhase, Florian Rabe in Journal of Automated Reasoning (2021)

Article

Erratum zu: Editorial

Philipp Cimiano, Gerhard Heyer, Michael Kohlhase, Benno Stein… in Datenbank-Spektrum (2021)

Article

Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge

Jacques Carette, William M. Farmer, Michael Kohlhase… in The Mathematical Intelligencer (2021)

Chapter

Mathematical Information Retrieval

present an overview of the NTCIR Math Tasks organized during NTCIR-10, 11, and 12. These tasks are primarily dedicated to techniques for searching mathematical content with formula expressions. In this chap...

Akiko Aizawa, Michael Kohlhase in Evaluating Information Retrieval and Access Tasks (2021)

Article

Editorial

Philipp Cimiano, Gerhard Heyer, Michael Kohlhase, Benno Stein… in Datenbank-Spektrum (2020)

Chapter and Conference Paper

Logic-Independent Proof Search in Logical Frameworks

Logical frameworks like LF allow to specify the syntax and (natural deduction) inference rules for syntax/proof-checking a wide variety of logical systems. A crucial feature that is missing for prototy** log...

Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen… in Automated Reasoning (2020)

Chapter and Conference Paper

Prototy** Controlled Mathematical Languages in Jupyter Notebooks

The Grammatical Logical Framework (GLF) is a framework for prototy** the translation of natural language sentences into logic. The motivation behind GLF was to apply it to mathematical language, as the classica...

Jan Frederik Schaefer, Kai Amann, Michael Kohlhase in Mathematical Software – ICMS 2020 (2020)

Chapter and Conference Paper

Full Semantic Transparency: Overcoming Boundaries of Applications

Complex workflows require intelligent interactions. In this paper we attack the problem of combining user interfaces of specialized applications that support different aspects of objects in scientific/technica...

Andrea Kohlhase, Michael Kohlhase… in Human-Computer Interaction – INTERACT 2013 (2013)

Chapter and Conference Paper

Bringing Mathematics to the Web of Data: The Case of the Mathematics Subject Classification

The Mathematics Subject Classification (MSC), maintained by the American Mathematical Society’s Mathematical Reviews (MR) and FIZ Karlsruhe’s Zentralblatt für Mathematik (Zbl), is a scheme for classifying publ...

Christoph Lange, Patrick Ion… in The Semantic Web: Research and Applications (2012)

Chapter and Conference Paper

The Planetary System: Executable Science, Technology, Engineering and Math Papers

Executable scientific papers contain not just layouted text for reading. They contain, or link to, machine-comprehensible representations of the scientific findings or experiments they describe. Client-side pl...

Christoph Lange, Michael Kohlhase… in The Semanic Web: Research and Applications (2011)

Chapter and Conference Paper

Publishing Math Lecture Notes as Linked Data

We mark up a corpus of \({\mbox{\LaTeX}}\) lecture notes semantically and expose them as Linked Data in XHTML+MathML+RD...

Catalin David, Michael Kohlhase… in The Semantic Web: Research and Applications (2010)