TY - GEN
T1 - Automated Theorem Proving in Support of Computer Algebra: Symbolic Definite Integration As a Case Study
AU - Adams, A. A.
AU - Gottliebsen, H.
AU - Linton, S. A.
AU - Martin, U.
PY - 1999
Y1 - 1999
N2 - We assess the current state of research in the application of computer aided formal reasoning to computer algebra, and argue that embedded verification support allows users to enjoy its benefits without wrestling with technicalities. We illustrate this claim by considering symbolic definite integration, and present a verifiable symbolic definite integral table look up: a system which matches a query comprising a definite integral with parameters and side conditions, against an entry in a verifiable table and uses a call to a library of lemmas about the reals in the theorem prover PVS to aid in the transformation of the table entry into an answer. We present the full model of such a system as well as a description of our prototype implementation showing the efficacy of such a system: for example, the prototype is able to obtain correct answers in cases where computer algebra systems [CAS] do not. We extend upon Fateman's web-based table by including parametric limits of integration and queries with conditions.
AB - We assess the current state of research in the application of computer aided formal reasoning to computer algebra, and argue that embedded verification support allows users to enjoy its benefits without wrestling with technicalities. We illustrate this claim by considering symbolic definite integration, and present a verifiable symbolic definite integral table look up: a system which matches a query comprising a definite integral with parameters and side conditions, against an entry in a verifiable table and uses a call to a library of lemmas about the reals in the theorem prover PVS to aid in the transformation of the table entry into an answer. We present the full model of such a system as well as a description of our prototype implementation showing the efficacy of such a system: for example, the prototype is able to obtain correct answers in cases where computer algebra systems [CAS] do not. We extend upon Fateman's web-based table by including parametric limits of integration and queries with conditions.
U2 - 10.1145/309831.309949
DO - 10.1145/309831.309949
M3 - Conference contribution
SN - 1-58113-073-2
T3 - ISSAC '99
SP - 253
EP - 260
BT - Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation
PB - ACM
CY - New York, NY, USA
ER -