PL EN


2009 | 18(31) | 51-66
Article title

A LANGUAGE FOR MATHEMATICAL KNOWLEDGE MANAGEMENT

Selected contents from this journal
Title variants
Languages of publication
EN
Abstracts
EN
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.
Year
Issue
Pages
51-66
Physical description
Document type
ARTICLE
Contributors
author
  • Steven Kieffer, Simon Fraser University; Jeremy Avigad, Carnegie Mellon University; Harvey Friedman, Ohio State University, USA
References
Document Type
Publication order reference
Identifiers
CEJSH db identifier
11PLAAAA10164
YADDA identifier
bwmeta1.element.96cae2ff-5727-32a8-8e5c-d7f3aa35c8a1
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.