A LANGUAGE FOR MATHEMATICAL KNOWLEDGE MANAGEMENT

• Authors: Kieffer Steven , Avigad Jeremy , Friedman Harvey
• 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.

Keywords

EN

FORMALIZATION; LANGUAGE OF MATHEMATICS; MATHEMATICAL KNOWLEDGE MANAGEMENT

Discipline

• LIBRARY_&_INFORMATION_SCIENCE: LIBRARY & INFORMATION SCIENCE

• Publisher: Sciendo
• Journal: Studies in Logic, Grammar and Rhetoric
• Year: 2009
• Issue: 18(31)
• Pages: 51-66
• Document type: ARTICLE

Contributors

author

Kieffer Steven

author

Avigad Jeremy

author

Friedman Harvey

• Steven Kieffer, Simon Fraser University; Jeremy Avigad, Carnegie Mellon University; Harvey Friedman, Ohio State University, USA

Identifiers

CEJSH db identifier

11PLAAAA10164