Towards Flexiformal Mathematics

  • The application of computer-based methods to mathematics, while meaningful, is constrained by the fact the most mathematical knowledge exists in forms that can only be understood by humans. In order for it to be also understood by machines, those aspects of mathematical knowledge that are relevant for machine-driven applications need to be made explicit. One important aspect of mathematics is the underlying semantics which can be made understandable to machines by formalizing it. Formalization makes explicit the implicit definitions and inference steps that occur naturally in mathematical documents. But, despite numerous attempts, only a small fragment of mathematics has been formalized because formalization is prohibitively expensive. Furthermore, existing formalized mathematics typically lacks in other aspects such as presentation information and narrative structure that are common in mathematics and critical for human-oriented practical applications. Therefore, existing applications for formal mathematics are mostly limited to verification so there is little practical incentive for formalization. Relying on the idea of flexiformality we propose flexiformalizing mathematics which addresses the bottlenecks discussed above in two ways. First, by allowing content of flexible formality, it minimizes the starting cost of flexiformalization compared to formalization. Second, by co-representing the narration, structure and meaning of mathematical knowledge it forms a basis for not only machine processing but also for building practical, human-oriented applications. We call the result of flexiformalization as described here flexiformal knowledge and we believe mathematical knowledge is fundamentally flexiformal.

Download full text

Cite this publication

  • Export Bibtex
  • Export RIS

Citable URL (?):

Search for this publication

Search Google Scholar Search Catalog of German National Library Search OCLC WorldCat Search Catalog of GBV Common Library Network Search Catalog of Jacobs University Library Search Bielefeld Academic Search Engine
Meta data
Publishing Institution:IRC-Library, Information Resource Center der Jacobs University Bremen
Granting Institution:Jacobs Univ.
Author:Mihnea Iancu
Referee:Michael Kohlhase, Herbert Jaeger, William Farmer, Florian Rabe
Advisor:Michael Kohlhase
Persistent Identifier (URN):urn:nbn:de:gbv:579-opus-1007213
Document Type:PhD Thesis
Language:English
Date of Successful Oral Defense:2017/01/05
Date of First Publication:2017/09/22
Academic Department:Computer Science & Electrical Engineering
PhD Degree:Computer Science
Focus Area:Mobility
Call No:Thesis 2017/19

$Rev: 13581 $