The role of computational logic in mathematical communication

Ursula Martin

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 (Gdel'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 had little impact on mainstream mathematics, perhaps because of apparently naive claims sometimes made by non-mathematicians, traditional misgivings about the place of formal proof in mathematics, or an unwillingess to divert scarce resources into reworking known material inside a computational logic system.

I shall argue that it is time for the mathematical community to revisit computational logic: - 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 - to share in ownership of a technology that is becoming increasingly important in applications of mathematics, such as hardware design, e-commerce protocols or network analysis, that require the highest assurance of correctness - 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

Professor Ursula Martin PhD MA CEng holds degrees from Cambridge and Warwick Universities, and following posts at Urbana-Champaign, Manchester and London is now Professor of Logic, Algebra and Computation at the University of St Andrews in Scotland, where she heads a research group working on the theory and applications of computational logic and symbolic computation. She is currently spending a sabbatical at the Computer Science Laboratory at SRI International in Menlo Park, investigating the application of computational logic to continuous mathematics. She has served on the Council of the London Mathematical Society 1994-1999, and initiated and coordinated from 1996 to 1999 EPSRC/LMS MathFIT, a joint initiative of the LMS and the UK national science research council to promote interdisciplinary research in mathematics and computer science.

created Mon Dec 6 17:43:45 PST 1999