Carnegie Mellon University
Browse
file.pdf (197.48 kB)

A Language for Mathematical Knowledge Management

Download (197.48 kB)
journal contribution
posted on 2008-01-01, 00:00 authored by Steven Kieffer, Jeremy AvigadJeremy Avigad, Harvey Friedman
We argue that the language of Zermelo Fraenkel set theory with definitions and partial functions provides the most promising bedrock semantics for communicating and sharing mathematical knowledge. We then describe a syntactic sugaring of that language that provides a way of writing remarkably readable assertions without straying far from the set-theoretic semantics. We illustrate with some examples of formalized textbook definitions from elementary set theory and point-set topology. We also present statistics concerning the complexity of these definitions, under various complexity measures.

History

Publisher Statement

All Rights Reserved

Date

2008-01-01

Usage metrics

    Categories

    Keywords

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC