The flexiformalist program promises to combine the distinct advantages of both machine-oriented formal and human-oriented informal mathematics, by representing both in an interleaved manner in the same document. In theory, this enables active documents augmented by in-situ services acting on the (flexi-)formal semantics of sentences and paragraphs, but so far, the required comprehensive software support to do so in practice was lacking. Towards that end, we developed a comprehensive solution for authoring, curating, and viewing (corpora of) active flexiformal documents, consisting of: 1. an ontology of flexiformal commons (based on OMDoc), 2. an annotation schema (FTML – Flexiformal H TML) for HTML documents, 3. a dedicated system ( – Flexiformal Annotation Management System) for managing and serving flexiformally annotated documents and document fragments, and 4. a standalone FTML viewer in the form of a JavaScript/WebAssembly script, rendering FTML-annotated HTML documents (inter)active. and the FTML viewer are running publicly on https://mathhub.info , giving access to large corpora of flexiformal documents, and power our learning platform ALeA, which is actively used in university education ( https://alea.education ).

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

The Flexiformalist Manifesto Made Manifest

  • Dennis Müller

摘要

The flexiformalist program promises to combine the distinct advantages of both machine-oriented formal and human-oriented informal mathematics, by representing both in an interleaved manner in the same document. In theory, this enables active documents augmented by in-situ services acting on the (flexi-)formal semantics of sentences and paragraphs, but so far, the required comprehensive software support to do so in practice was lacking. Towards that end, we developed a comprehensive solution for authoring, curating, and viewing (corpora of) active flexiformal documents, consisting of: 1. an ontology of flexiformal commons (based on OMDoc), 2. an annotation schema (FTML – Flexiformal H TML) for HTML documents, 3. a dedicated system ( – Flexiformal Annotation Management System) for managing and serving flexiformally annotated documents and document fragments, and 4. a standalone FTML viewer in the form of a JavaScript/WebAssembly script, rendering FTML-annotated HTML documents (inter)active. and the FTML viewer are running publicly on https://mathhub.info , giving access to large corpora of flexiformal documents, and power our learning platform ALeA, which is actively used in university education ( https://alea.education ).