[FOM] paper announcement
avigad at cmu.edu
Fri Jan 12 11:26:39 EST 2007
Dear friends and colleagues,
I would like to announce a few papers that may be of interest to the FOM
audience. The are all available on my web page,
"Understanding proofs". This argues for a particular way of thinking
about mathematical understanding, and surveys contemporary work in
formal verification that bears on the topic.
"A decision procedure for linear 'big O' equations" (with Kevin
Donnelly). We show that the validity of boolean combinations of linear
"big O" equations (in various formulations) is decidable.
"A variant of the double-negation translation". This short note
describes an interesting variant of the double-negation translation, and
an application to functional interpretation. (These results were
discovered independently by Streicher and Kohlenbach.)
"Combining decision procedures for the reals" (with Harvey Friedman).
This includes decidability and undecidability results for theories
obtained by combining the linear and multiplicative fragments of the
reals (as an ordered field). We also propose a strategy for verifying
common inferences involving real inequalities in the context of formal
"Gödel and the metamathematical tradition". This consists of reflections
on Gödel and his uneasy relationship with the Hilbert tradition. This
was presented as a talk to the ASL Spring Meeting in Montreal last year.
"Computers in mathematical inquiry". This is a survey of philosophical
issues related to the use of computers in mathematics. This article,
together with "Understanding proofs", will appear in a collection of
essays on the philosophy of mathematical practice, edited by Paolo Mancosu.
I have announced the last three of these papers in this forum before,
but they have been revised since then.
Associate Professor of Philosophy
Carnegie Mellon University
More information about the FOM