John Harrison.
Proceedings of the Finnish Artificial Intelligence Society
(FAIS) symposium Logic, Mathematics and the Computer: History, Foundations
and Applications, University of Helsinki, Metsätalo, 3-4 June 1996,
pp. 153-169.
NB! Most of the contents of this paper are discussed in greater depth
in my PhD
thesis
Abstract:
It is widely believed that in principle it's possible to reduce most of
present-day mathematics to reasoning in a formal logical system. The technical
difficulty of actually doing so is quite formidable. However, the arrival of
the computer is changing this situation, since computers are good at helping
with such tedious symbolic manipulation. The computer formalization of
mathematics is now a popular research topic. Here we report on our own
development of mathematical analysis starting just from the axioms of simple
type theory and reducing all reasoning (with the aid of the computer) to a
formal deductive calculus of great simplicity.
Bibtex entry:
@INPROCEEDINGS{harrison-fais,
author = "John Harrison",
title = "Pure Mathematics in a Mechanized Logic",
booktitle = "Proceedings of the Finnish Artificial Intelligence
Society Symposium: Logic, Mathematics and the
Computer",
editor = "Christoffer Gefwert and Pekka Orponen and
Juoko Sepp{\"a}nen",
publisher = "Finnish Artificial Intelligence Society",
series = "Suomen Teko{\"a}lyseuran julkaisuja",
volume = 14,
year = 1996,
pages = "153--169"}