Abstract
The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that supports this claim: the mechanised proofs depend on non-trivial algorithms from computer algebra and increase the reasoning power of the theorem prover. The unsoundness of computer algebra systems is a major problem in interfacing them to theorem provers. Our approach to obtaining a sound overall system is not blanket distrust but based on the distinction between algorithms we call sound and ad hoc respectively. This distinction is blurred in most computer algebra systems. Our experimental interface therefore uses a computer algebra library. It is based on theorem templates, which provide formal specifications for the algorithms.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Clemens Ballarin, Karsten Homann, and Jacques Calmet. Theorems and algorithms: An interface between Isabelle and Maple. In A. H. M. Levelt, editor, ISSAC ’95: International symposium on symbolic and algebraic computation — July 1995, Montréal, Canada, pages 150–157. ACM Press, 1995.
Manuel Bronstein. Sumit — a strongly-typed embeddable computer algebra library. In Calmet and Limongelli [1996], pages 22–33.
J. Calmet and J. A. Campbell. A perspective on symbolic mathematical computing and artificial intelligence. Annals of Mathematics and Artificial Intelligence, 19(3–4):261–277, 1997.
Jacques Calmet and Carla Limongelli, editors. Design and Implementation of Symbolic Computation Systems: International Symposium, DISCO ’96, Karlsruhe, Germany, September 18–20, 1996: proceedings, number 1128 in Lecture Notes in Computer Science. Springer-Verlag, 1996.
Edmund Clarke and Xudong Zhao. Analytica: A theorem prover for Mathematica. The Mathematica Journal, 3(1):56–71, 1993.
Robert M. Corless and David J. Jeffrey. The unwinding number. ACM SIGSAM Bulletin, 30(2):28–35, 1996.
R. M. Corless and D. J. Jeffrey. The Turing factorization of a rectangular matrix. ACM SIGSAM Bulletin, 31(3):20–28, 1997.
Keith O. Geddes, Stephen R. Czapor, and George Labahan. Algorithms for Computer Algebra. Kluwer Academic Publishers, 1992.
John Robert Harrison. Theorem proving with the real numbers. Technical Report 408, University of Cambridge, Computer Laboratory, November 1996.
D. G. Hoffman, D. A. Leonard, C. C. Lindner, K. T. Phelps, C. A. Rodger, and J. R. Wall. Coding Theory: The Essentials. Number 150 in Monographs and textbooks in pure and applied mathematics. Marcel Dekker, Inc., New York, 1991.
Karsten Homann. Symbolisches Lösen mathematischer Probleme durch Kooperation algorithmischer und logischer Systeme. Number 152 in Dissertationen zur Künstlichen Intelligenz. infix, St. Augustin, 1997.
Manfred Kerber, Michael Kohlhase, and Volker Sorge. Integrating computer algebra with proof planning. In Calmet and Limongelli [1996], pages 204–215.
Lawrence C. Paulson. Isabelle: a generic theorem prover. Number 828 in Lecture Notes in Computer Science. Springer-Verlag, 1994.
David R. Stoutemyer. Crimes and misdemeanors in the computer algebra trade. Notices of the American Mathematical Society, 38(7):778–785, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ballarin, C., Paulson, L.C. (1998). Reasoning about coding theory: The benefits we get from computer algebra. In: Calmet, J., Plaza, J. (eds) Artificial Intelligence and Symbolic Computation. AISC 1998. Lecture Notes in Computer Science, vol 1476. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055902
Download citation
DOI: https://doi.org/10.1007/BFb0055902
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64960-1
Online ISBN: 978-3-540-49816-2
eBook Packages: Springer Book Archive