Symbolic Computation Group

David R. Cheriton School of Computer Science
University of Waterloo, Waterloo, Ontario, Canada

Computational Logic
Ursula Martin, University of St. Andrews, UK
Friday, March 2, 2001, at U. of Western Ontario.


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 on-line 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


Last modified on Sunday, 04 November 2012, at 15:42 hours.