ion consider units in which one can define sorts, typed symbols (optionally providing their definitions) and axioms stating the properties of the defined sorts and symbols. We use the term theory presentation to refer to this abstract unit. The theory of this abstraction has been well-studied under the name universal algebra [5]. Our goal is to identify what knowledge can be automatically generated from theory presentations. We want to provide a library of algorithms to generate this knowledge. This way, we provide tool support for library development and formalization tasks by removing some of the boilerplate associated with defining constructs that can be automatically generated. Not only does generating these new pieces save time and effort for the developer, but, more importantly, leverages the information contained in the theory graph by establishing new connections between the theories. A theory graph is a collection of theories and theory morphisms. We want to be able to generate the new pieces of knowledge and the morphisms connecting them to the graph. We describe our contributions as • Evaluating the status of current popular libraries of mathematics, in terms of modularity and reusability. • Compiling a list of constructions that can be automatically generated from the syntax of a theory presentation.
Copyright © by the paper’s authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
In: C. Kaliszyk, E. Brady, J. Davenport, W.M. Farmer, A. Kohlhase, M. Kohlhase, D. Müller, K. Pąk, and C. Sacerdoti Coen (eds.):
Joint Proceedings of the FMM and LML Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent
Computer Mathematics 2019 co-located with the 12th Conference on Intelligent Computer Mathematics (CICM 2019), Prague,
Czech Republic, July 8–12, 2019, published at http://ceur-ws.org
We are interested in syntactically manipulating theory presentations, in their most abstract form. To achieve a
high level of abstraction, we use Mmt [
After generating the different pieces of knowledge, we want to be able to translate them into different formal systems. Considering systems with very different foundations, like Isabelle/HOL and Agda. The first is based on HOL, while the second is based on dependent type theory. They have different representations of theories, yet the information contained in them is the same. For example, a Monoid theory consists of a sort, a point, a binary operation and three axioms. These pieces do not change based on the logic, but the way they are formalized does. We are interested in automating the generation of theories in different formal systems. For this, we aim to develop a feature model exploring the similarities and differences between the different systems. This feature model will be used to design generators from our abstract model to the different systems. This way, the information is generated once, and translated automatically to different representations.
Evaluation
We use the MathScheme library [
In conclusion, we aim at supporting the development of libraries by generating some related construction that can be made available by syntactic manipulation of theory presentations. As an outcome of our work, a user should be able to write something like B o o l e a n A l g e b r a := T h e o r y {
U : type ; * : ( U , U ) -> U ; + : ( U , U ) -> U ; - - > : ( U , U ) -> U ; 0 : U ; 1 : U ; c o m p l : U -> U ; a x i o m u n i p o t e n t _ - - > _1 : f o r a l l x : U . ( x - - > x ) = (1); .... } g e n e r a t e ( termLang , s i m p l i f y ) and then ask the system to evaluate simplify ((x * y) + 1) without any extra effort to define the term language or simplification rules. 1By expressivity we mean practical expressivity, in terms that information is expressed in a practical and convenient way