Computational Logic
Ursula Martin, University of St. Andrews, UK
Friday, March 2, 2001, at U. of Western Ontario.
Abstract:
Computational logic means the use of computers to produce formal proofs in
a given logical system, a dream of logicians such as Russell and Hilbert,
which (Goedel's theorem aside) has only really become feasible with today's
computer support. It ranges from implementations of automatic procedures,
through collections of strategies for the machine to try which will not
necessarily find a proof, to programs which check line by line whether or
not the input generated by the user or another program is a valid proof.
Computational logic software systems such as Otter, Mizar and PVS have been
used, for example, to prove conjectures and generate online journals of
mechanically verified mathematics, and companies such as Intel and Cadence
are investing heavily in such technology for modelling hardware.
Yet this work has thus far had little impact on mainstream mathematics or
its applications in science and engineering. I shall discuss some of the
reasons for this and outline recent work and future plans:
for its immediate application as an effective component of mathematical
software such as Maple or for representing mathematical knowledge as part
of endeavours like OpenMath/MathML
the use of computational logic techniques to support applied math and
mathematical modeling, particularly in areas where the highest degree of
assurance is required, such as avionics
to develop a strategy for the representation, validation and
communication of mathematics in a future where the opportunities and
challenges of digitally embodied knowledge may radically change scholarship
and scientific discourse
