97 Result(s)
within
Conference Paper
Michael Kohlhase
-
Chapter and Conference Paper
Guided Tours in ALeA
In times of decreasingly homogeneous educational backgrounds and experiences and increasingly diverse educational target groups and circumstances, the need for educational content that caters to individuals an...
-
Chapter and Conference Paper
Learning Support Systems Based on Mathematical Knowledge Management
To cater to the increasingly diverse student bodies, higher education has to personalize education. In times of stagnant educational budgets and staffing problems, this can only be achieved via adaptive, inter...
-
Chapter and Conference Paper
Towards an Annotation Standard for STEM Documents
When publishing papers, researchers in mathematics and related disciplines typically focus on the presentation, i.e. type-setting, of their ideas and provide little semantic information. This impedes the devel...
-
Chapter and Conference Paper
System Description STEX3 – A LATEX-Based Ecosystem for Semantic/Active Mathematical Documents
We report on – a complete redesign and reimplementation (using ...
-
Chapter and Conference Paper
Injecting Formal Mathematics Into LaTeX
The paper presents the format for representing informal mathematics. acts as a surface language for two systems: the (presentation-ori...
-
Chapter and Conference Paper
TGView3D: A System for 3-Dimensional Visualization of Theory Graphs
We describe the TGView3D system, an interactive graph viewer optimized for exploring mathematical knowledge as 3D graphs. To exploit all three spatial dimensions, it extends the commonly-used force-directed la...
-
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...
-
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...
-
Chapter and Conference Paper
Towards a Heterogeneous Query Language for Mathematical Knowledge
With more than 120.000 articles published annually in mathematical journals alone, mathematical search has often been touted as a killer application of computer-supported mathematics. But the artefacts of math...
-
Chapter and Conference Paper
FrameIT: Detangling Knowledge Management from Game Design in Serious Games
Serious games are an attempt to leverage the inherent motivation in game-like scenarios for an educational application and to transpose the learning goals into real-world applications. Unfortunately, serious g...
-
Chapter and Conference Paper
Representing Structural Language Features in Formal Meta-languages
Structural language features are those that introduce new kinds of declarations as opposed to those that only add expressions. They pose a significant challenge when representing languages in meta-languages su...
-
Chapter and Conference Paper
Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation
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....
-
Chapter and Conference Paper
Relational Data Across Mathematical Libraries
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 theore...
-
Chapter and Conference Paper
Integrating Semantic Mathematical Documents and Dynamic Notebooks
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 b...
-
Chapter and Conference Paper
Discourse Phenomena in Mathematical Documents
Much of the wealth of industrialized societies is based on knowledge that is laid down and communicated in scientific/technical/engineering/mathematical documents: highly structured documents that contain diag...
-
Chapter and Conference Paper
Theories as Types
Theories are an essential structuring principle that enable modularity, encapsulation, and reuse in formal libraries and programs (called classes there). Similar effects can be achieved by dependent record typ...
-
Chapter and Conference Paper
Knowledge Amalgamation for Computational Science and Engineering
This paper addresses a knowledge gap that is commonly encountered in computational science and engineering: To set up a simulation, we need to combine domain knowledge (usually in terms of physical principles), m...
-
Chapter and Conference Paper
Automatically Finding Theory Morphisms for Knowledge Management
We present a method for finding morphisms between formal theories, both within as well as across libraries based on different logical foundations. As they induce new theorems in the target theory for any of th...
-
Chapter and Conference Paper
Translating the IMPS Theory Library to MMT/OMDoc
The IMPS system by Farmer, Guttman and Thayer was an influential automated reasoning system, pioneering mechanisations of features like theory morphisms, partial functions with subsorts, and the little theories a...
-
Chapter and Conference Paper
Mathematical Models as Research Data via Flexiformal Theory Graphs
Mathematical modeling and simulation (MMS) has now been established as an essential part of the scientific work in many disciplines. It is common to categorize the involved numerical data and to some extent th...
