文档介绍：Computer Algebra and
Theorem Pro ving
Clemens Ballarin
Darwin College
Univ ersit y of Cam bridge
A dissertation submitted for the degree of
Do ctor of Philosoph y
Abstract
Is the use puter algebra tec hnology b ene
cial for mec hanised reason
ing in and ab out mathematical domains
Usually it is assumed that it is
Man y w orks in this area
ho w ev er
either ha v e little reasoning con ten t
or
use sym b putation only to simplify expressions
In w ork that has
ac hiev ed more
the used metho ds do not scale up
They trust puter
algebra system either to o m uc h or to o little
Computer algebra systems are not as rigorous as man y pro v ers
They
are not logically sound reasoning systems
but collections of algorithms
W e
classify soundness problems that ur puter algebra systems
While
man y algorithms and their implemen tations are p erfectly trust w orth y
the
seman tics of sym b ols is often unclear and leads to errors
On the other
hand
more robust approac hes to in terface external reasoners to pro v ers are
not alw a ys practical b ecause the mathematical depth of pro ofs algorithms
puter algebra are based on can b e enormous
Our o wn approac h tak es b oth trust w orthiness of the o v erall system and
e
ciency in to accoun t
It relies on using only reliable parts of puter
algebra system
whic h can b e ac hiev ed b y c ho osing a suitable library
and
deriving sp eci
cations for these algorithms from their literature
W e design and implemen t an in terface b et w een the pro v er Isab elle and
puter algebra library Sumit and use it to pro v e non
trivial theorems
from co ding theory
This is based on the mec hanisation of the algebraic
theories of rings and p olynomials
Co ding theory is an area where pro ofs
do ha v e a substan tial amoun t putational con ten t
Also
it is realistic
to assume that the v eri
cation of an enco ding or deco ding device could b e
undertak en in
and indeed
b e simpli
ed b