Technical reports

Computer algebra and theorem proving

Clemens Ballarin

October 1999, 122 pages

This technical report is based on a dissertation submitted by the author for the degree of Doctor of Philosophy to the University of Cambridge, Darwin College.

Abstract

Is the use of computer algebra technology beneficial for mechanised reasoning in and about mathematical domains? Usually it is assumed that it is. Many works in this area, however, either have little reasoning content, or use symbolic computation only to simplify expressions. In work that has achieved more, the methods used do not scale up. They trust the computer algebra system either too much or too little.

Computer algebra systems are not as rigorous as many provers. They are not logically sound reasoning systems, but collections of algorithms. We classify soundness problems that occur in computer algebra systems. While many algorithms and their implementations are perfectly trustworthy the semantics of symbols is often unclear and leads to errors. On the other hand, more robust approaches to interface external reasoners to provers are not always practical because the mathematical depth of proof algorithms in computer algebra can be enormous.

Our own approach takes both trustworthiness of the overall system and efficiency into account. It relies on using only reliable parts of a computer algebra system which can be achieved by using a suitable library, and deriving specifications for these algorithms from their literature.

We design and implement an interface between the prover Isabelle and the computer algebra library Sumit and use it to prove non-trivial theorems from coding theory. This is based on mechanisation of the algebraic theories of rings and polynomials. Coding theory is an area where proofs do have a substantial amount of computational content. Also it is realistic to assume that the verification of an encoding or decoding device cound be undertaken in, and indeed, be simplified by, such a system.

The reason why semantics of symbols is often unclear in current computer algebra systems is not mathematical difficulty, but the design of those systems. For Gaussian elimination we show how the soundness problem can be fixed by a small extention, and without using efficiency. This is a prerequisite for the efficient use of the algorithm in a prover.

Full text

PDF (8.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-473,
  author =	 {Ballarin, Clemens},
  title = 	 {{Computer algebra and theorem proving}},
  year = 	 1999,
  month = 	 oct,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-473.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-473},
  number = 	 {UCAM-CL-TR-473}
}