Skip to main content

and
  1. No Access

    Chapter and Conference Paper

    Towards an Annotation Standard for STEM Documents

    When publishing papers, researchers in mathematics and related disciplines typically focus on the presentation, i.e. type-setting, of their ideas and provide little semantic information. This impedes the devel...

    Jan Frederik Schaefer, Michael Kohlhase in Intelligent Computer Mathematics (2023)

  2. Chapter and Conference Paper

    Logic-Independent Proof Search in Logical Frameworks

    Logical frameworks like LF allow to specify the syntax and (natural deduction) inference rules for syntax/proof-checking a wide variety of logical systems. A crucial feature that is missing for prototy** log...

    Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen in Automated Reasoning (2020)

  3. Chapter and Conference Paper

    Prototy** Controlled Mathematical Languages in Jupyter Notebooks

    The Grammatical Logical Framework (GLF) is a framework for prototy** the translation of natural language sentences into logic. The motivation behind GLF was to apply it to mathematical language, as the classica...

    Jan Frederik Schaefer, Kai Amann, Michael Kohlhase in Mathematical Software – ICMS 2020 (2020)