2025
-
Michael Kohlhase
,
Florian Rabe ,
Marcel Schütz ;
Lightweight Realms;
in: Valeria de Paiva, Peter Koepke (eds.);
Intelligent Computer Mathematics;
CICM 2025,
Brasília, Brazil.
Article
PDFAbstract
During formalization – e.g. of Mathematics – we have to take many decisions that informal mathematics leaves (and can leave) open. In particular, often there are multiple isomorphic ways of formalizing a set of axioms between which mathematicians can switch seamlessly. But this can impede beginners from fully understanding a domain, and it has proved difficult to mimic the same seamlessness in formalized mathematics, hindering interoperability between systems and libraries.
Realms have been proposed as an explicit representation of collections of isomorphic theories and conservative extensions, but have proven difficult to implement and manage. Therefore, here we introduce a more specialized definition that, in our experience, covers a large set of practically relevant examples. The central concept is that of a base of a theory: a subtheory that uniquely determines the entire theory. This allows us to represent an entire realm as a single theory with multiple bases. We show that many foundational concepts can be elegantly represented as such basic realms. The resulting formalism offers a good abstraction level to deal with (the consequences of) differing choices in the literature and in formal libraries, thus reducing interoperability problems, while keeping the formalizations simple.
BibTEX
@InProceedings{KohRabSch2025:LigRea, author={Kohlhase, Michael and Rabe, Florian and Schütz, Marcel}, editor={de Paiva, Valeria and Koepke, Peter}, title={Lightweight Realms}, booktitle={Intelligent Computer Mathematics}, year={2025}, publisher={Springer}, pages={222--239} } -
Josefin Kelber ,
Michael Kohlhase ,
Jan Frederik Schaefer ,
Marcel Schütz ;
Reaping the Benefits of Modularization in Flexiformal Mathematics by GF-based AST Transformations;
in: Valeria de Paiva, Peter Koepke (eds.);
Intelligent Computer Mathematics;
CICM 2025,
Brasília, Brazil.
Abstract
Flexiformal documents – i.e. documents with embedded semantic annotations that make some aspects of their content machineactionable – can be instrumented to make interaction with the underlying knowledge more efficient and effective. Fostering such interactions via semantic services has proven very successful in university education, but the practical applicability is limited by the cost of flexiformalization. A method for lowering (flexi)-formalization costs is to use modular representations to profit from enhanced source sharing and induced (generated) content. In fully formal environments this is well-understood and implemented in many systems.
In this paper we show that many of the formal techniques carry over to the informal setting if we parse (rigorous) natural language with a semantically optimized grammar and work on abstract syntax trees instead of formulae.
We present i) a set of use cases for generating learning material to be used in an educational setting – concretely in the field of theoretical computer science, ii) a GF grammar that allows to syntactically analyze the underlying language fragment, iii) a set of AST-to-AST simplifications that can be used to fine-tune the wording and formulae of the generated content and adapt it to the scientific jargon, and iv) a prototypical implementation that shows the technique in action.
BibTEX
@InProceedings{KelKohSchSch2025:RepTheBenOfModInFleMatByGfBasAstTra, author={Kelber, Josefin and Kohlhase, Michael and Schaefer, Jan Frederik and Schütz, Marcel}, editor={de Paiva, Valeria and Koepke, Peter}, title={Reaping the Benefits of Modularization in Flexiformal Mathematics by GF-based AST Transformations}, booktitle={Intelligent Computer Mathematics}, year={2025}, publisher={Springer}, pages={191--207} }
2024
-
Michael Kohlhase ,
Marcel Schütz ;
Reusing Learning Objects via Theory Morphisms;
in: Andrea Kohlhase, Laura Kovács (eds.);
Intelligent Computer Mathematics;
CICM 2024,
Montreal, Quebec, Canada.
Abstract
One of the most important motivations of module systems for formal systems is that statements and objects can be re-purposed in other contexts via the inheritance pathways. In this paper, we show that this idea can be extended to informal settings using an adaptive learning assistant (ALeA) as a concrete use case.
Specifically, we concentrate on repurposing informal definitions, quiz questions, and explanations between the contexts given by different theories in a flexiformal theory graph. Using this, we can now refactor (transport backwards over a theory morphism) e.g. quiz questions like “Is the following formula satisfiable?” to be logic-independent and utilize them in any logic via forward morphism transport.
This goes a large step towards solving the biggest practical problem in ALeA-like systems: provisioning enough targeted semantically annotated learning objects.
BibTEX
@InProceedings{KohSch2024:ReuLeaObjViaTheMor, author={Kohlhase, Michael and Schütz, Marcel}, editor={Kohlhase, Andrea and Kovács, Laura}, title={Reusing Learning Objects via Theory Morphisms}, booktitle={Intelligent Computer Mathematics}, year={2024}, publisher={Springer Nature Switzerland}, pages={165--182} } -
Theresa Kruse-Kurbach ,
Dominic Lohr ,
Marc Berges ,
Michael Kohlhase ,
Halimeh Moghbeli Damaneh,
Marcel Schütz ;
Term Extraction for Domain Modeling;
DELFI 2024,
Fulda, Germany.
Article
PDFAbstract
Addressing learners' individual needs in large lectures is challenging, especially if we want to tailor teaching materials, learning interventions, and feedback to individual students or sub-cohorts with special needs and educational biographies. AI-based adaptive learning systems (ALS) can help. Given a fine-grained domain model, we work on a system that can maintain a learner model and use it to generate learner-adaptive course materials: targeted explanations, flashcards, or quizzes from collections of learning objects that reference the domain model. In this system, the domain model consists of a knowledge graph of theories, each introducing a set of concepts and their definitions, properties, and relations.
The conceptual and semantic relations – i.e., the terminological dependency relation between concepts – in the knowledge graph, together with a model of cognitive processes, shape the learner model. In our experience, given sufficient student activity in the system, the quality and coverage of the domain model are key determining factors for the quality of the learner-adaptivity of the system.
The domain model is essential to the system and requires a large investment. Concept definitions and statements of properties and relations can be taken from course material or textbooks. In other words, the development of domain models should be computer-assisted, not only for quality assurance but also for efficiency reasons. In this paper, we present and evaluate experiments on using natural language processing (NLP) techniques, in particular term extraction, to generate term lists for domain models.
We focus on the following research question: To what extent can automatic keyword extraction support domain model creation? To answer this question, we extract terms from an introductory computer science course to compare the results of different automatic term extraction tools with those of manual term extraction.
BibTEX
@InProceedings{KruLohBerKohMogSch2024:TerExtForDomMod, author={Kruse-Kurbach, Theresa and Lohr, Dominic and Berges, Marc and Kohlhase, Michael and Moghbeli Damaneh, Halimeh and Schütz, Marcel}, title={Term Extraction for Domain Modeling}, booktitle={Proceedings of the 22. Fachtagung Bildungstechnologien ({DELFI})}, year={2024}, publisher={Gesellschaft für Informatik e.V.} }
2022
-
Marcel Schütz ,
Adrian De Lon ,
Peter Koepke ;
Setting up Set-Theoretical Foundations in Naproche;
in: Kevin Buzzard, Temur Kutsia (eds.);
Work-in-progress papers presented at the 15th Conference on Intelligent Computer Mathematics;
CICM 2022,
Tbilisi, Georgia.
Article
PDFAbstract
Bringing out the potential of interactive theorem provers requires efficient mathematical foundations. The current release of the natural language proof assistant Naproche has become sufficiently stable to allow a broader and principled approach towards libraries of basic mathematical material. We present Naproche's new ontology of objects, classes, maps, etc. and two foundational libraries about basic set theory and number theory. These foundations are then used, e.g., in a formalization of the Cantor–Schröder–Bernstein theorem.
BibTEX
@InProceedings{SchDelKoe2022:SetUpSetTheFouInNap, author={Schütz, Marcel and De Lon, Adrian and Koepke, Peter}, editor={Buzzard, Kevin and Kutsia, Temur}, title={Setting up Set-Theoretical Foundations in {Naproche}}, booktitle={Work-in-progress papers presented at the 15th Conference on Intelligent Computer Mathematics, {CICM} 2022 (Informal Proceedings)}, year={2022}, pages={52--64} }
2021
-
Adrian De Lon ,
Peter Koepke ,
Anton Lorenzen ,
Adrian Marti ,
Marcel Schütz ,
Makarius Wenzel ;
The Isabelle/Naproche Natural Language Proof Assistant;
in: André Platzer, Geoff Sutcliffe (eds.);
Automated Deduction – CADE 28;
CADE 2021,
online.
Article
PDFAbstract
Naproche is an emerging natural proof assistant that accepts input in the controlled natural language ForTheL. Naproche is included in the current version of the Isabelle/PIDE which allows comfortable editing and asynchronous proof-checking of ForTheL texts. The .tex dialect of ForTheL can be typeset by LATEX into documents that approximate the language and appearance of ordinary mathematical texts.
BibTEX
@InProceedings{DelKoeLorMarSchWen2021:TheIsaNapNatLanProAss, author={De Lon, Adrian and Koepke, Peter and Lorenzen, Anton and Marti, Adrian and Schütz, Marcel and Wenzel, Makarius}, editor={Platzer, André and Sutcliffe, Geoff}, title={The {Isabelle}/{Naproche} Natural Language Proof Assistant}, booktitle={Automated Deduction -- {CADE} 28}, year={2021}, publisher={Springer International Publishing}, address=Cham, pages={614--624} } -
Adrian De Lon ,
Peter Koepke ,
Anton Lorenzen ,
Adrian Marti ,
Marcel Schütz ,
Erik Sturzenhecker;
Beautiful Formalizations in Isabelle/Naproche;
in: Fairouz Kamareddine, Claudio Sacerdoti Coen (eds.);
Intelligent Computer Mathematics;
CICM 2021,
online.
Article
PDFAbstract
We present short example formalizations of basic theorems from number theory, set theory, and lattice theory which ship with the new Naproche component in Isabelle< 2021. The natural proof assistant Naproche
BibTEX
@InProceedings{DelKoeLorMarSchStu2021:BeaForInIsaNap, author={De Lon, Adrian and Koepke, Peter and Lorenzen, Anton and Marti, Adrian and Schütz, Marcel and Sturzenhecker, Erik}, editor={Kamareddine, Fairouz and Sacerdoti Coen, Claudio}, title={Beautiful Formalizations in {Isabelle}/{Naproche}}, booktitle={Intelligent Computer Mathematics}, year={2021}, publisher={Springer International Publishing}, address={Cham}, pages={19--31} }
2020
-
Peter Koepke ,
Jan Penquitt,
Marcel Schütz ,
Erik Sturzenhecker;
Formalizing Foundational Notions in Naproche-SAD;
NFM,
CICM 2020,
online.
Article
PDFAbstract
We present three current formalization projects with the proof assistant Naproche-SAD. Naproche-SAD formalizations use the natural mathematical input language ForTheL and in favorable cases read like textbook material. In this paper we emphasize the encoding of basic notions and axioms on the basis of inbuilt or slightly modified mechanisms of Naproche-SAD. The formalizations concern an introduction into set theory up to substantial results in infinitary combinatorics, a general theory of structures which are all made pairwise disjoint to avoid ambiguities, and an introduction to abstract linear algebra where for efficiency reasons the type system is restricted to a single type “object”, which is hard-coded into Naproche-SAD.
BibTEX
@Article{KoePenSchStu2021:ForFouNatInNapSad, author={Koepke, Peter and Penquitt, Jan and Schütz, Marcel and Sturzenhecker, Erik}, title={Formalizing Foundational Notions in {Naproche}-{SAD}}, year={2020}, }