![]() OpenDreamKit – “Open Digital Research Environment Toolkit for the Advancement of Mathematics” – is an H2020 EU Research Infrastructure project that aims at supporting, over the period 2015–2019, the ecosystem of open-source mathematical software systems. I present a few such services: (a) Curating alignments (roughly: two symbols S, T are called aligned if they represent the same platonic mathematical concept), (b) a generic method for translating formal expressions between systems and libraries using known alignments, theory morphisms and (if necessary) programmatic tactics, (c) an algorithm for automatically finding morphisms between theories (modulo alignments, if between theories from different libraries) and (d) Theory Intersections as a method to refactor given theories using theory morphisms. This enables accessing the core concepts and libraries of various systems from within the MMT system, and hence implement knowledge management services generically, acting on multiple libraries at once. I demonstrate this exemplary on the theorem prover PVS, the computer algebra systems Sage and GAP, and the LMFDB database. We can use this framework to formalize the logical foundation – or, if nonexistent, at least the foundational ontology – of a formal system, which we can use in turn to translate the associated libraries to OMDoc/MMT. An important aspect of such a framework is the ability to include potentially complex and computationally expensive features (such as subtyping mechanisms or record types) on demand only. This allows for specifying almost arbitrarily complicated logics, type theories and related systems. I demonstrate how we can develop modular logical frameworks within the MMT system – a foundation-agnostic framework for formal knowledge management based on the OMDoc/MMT language. ![]() Specifically, it is divided into three main parts: 1. This thesis describes the approach towards solving this problem pursued at our research group. This is due to different input languages, IDEs, library management facilities etc., but also due to fundamental theoretical aspects primarily the reliance on different logical foundations, such as set theories, type theories, and additional primitive features (e.g. This dissertation is concerned with the problem of integrating formal libraries: There is a plurality of theorem prover systems and related software with different strengths and weaknesses, that are fundamentally incompatible.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |