Automated theorem proving in support of computer algebra
Andrew A. Adams, Hanne Gottliebsen, Stephen Linton, Ursula Martin · 1999
\Ve assws the current state of research in the application of coluputcr aidd fbllal rCilsOIliIlg to couqmtrr illgt?~Jl'?l: ihlld argUC ~.llilt f?Ulbdtl(!dVWifiCat.iOllSUppOrt, idlOWS USCI'S t.0 eri,joy its hewfits bvit,liout wwstling wit.11 1:c?c:llilicalit,ics.We illust,rilte t.llis Claim by considering syuholir defiuitw intcgridion, autl prcscnt a Ycrifiable syubolic defiuit,c iIlWglX1 table look up: it systeru which ru,at,cllc!s a (picry comprising il.t1efiuit.cintegral with paraulct,crs ant1 sitlo c:onrlit.ious.iqqiiist.au cnt.r\; iu a W!rifiabk tahlc autl uses a c:a.ll to a librarv of leninias almut t.hc ITids in the tlicwrenl prover P\,'S t.0 Rid iii t.h: I;rilIlsfOrnlatiOIl of the tal.)lC cI1t.qiIlt0 it11 Xlsw-er.11-0 present tlw full model of such il syst~cul as well ilS a tloscriptiou Of our prototype i~ll~,leme~lt,a.tio~~showiug the efficacy of such a syst.eul:for examplc~ the protol.qv2 is al~lc I.0 obtaiu correct.answers in CRSW w-hcrc coinputcr illgehr~~ S~RkIllS [CAYS] Cl0 IlOt.11,-f?('XtCIM.1 Ill)011 Ehtf3n?lIl'S WlY!~)-bilSf!tltable by iuclutling piumllet.ric'IiuliLs of iut,cgra t ion ad queries with side coiidit.ious.