Translating a fragment of weak type theory into type theory with open terms

G.I. Jojgov

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    Abstract

    One of the main application areas of interactive proof assistants is the formalization of mathematical texts. This formalization not only allows mathematical texts to be handled electronically, but also to be checked for correctness. Due to the level of detail required in the formalization, formalized texts eliminate ambiguities that may be present in an informally presented mathematical texts.
    Original languageEnglish
    Title of host publicationMathematical Knowledge Management (Fourth International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised selected papers)
    EditorsM. Kohlhase
    Place of PublicationBerlin
    PublisherSpringer
    Pages389-403
    ISBN (Print)3-540-31430-X
    DOIs
    Publication statusPublished - 2006

    Publication series

    NameLecture Notes in Computer Science
    Volume3863
    ISSN (Print)0302-9743

    Cite this