Computer Algebra and Theorem Proving

ComputerAlgebraandTheoremProvingClemensBallarinDarwinCollegeUniversityofCambridgeAdissertationsubmittedforthedegreeofDoctorofPhilosophy2AbstractIstheuseofcomputeralgebratechnologybenecialformechanisedreason-inginandaboutmathematicaldomains?Usuallyitisassumedthatitis.Manyworksinthisarea,however,eitherhavelittlereasoningcontent,orusesymboliccomputationonlytosimplifyexpressions.Inworkthathasachievedmore,theusedmethodsdonotscaleup.Theytrustthecomputeralgebrasystemeithertoomuchortoolittle.Computeralgebrasystemsarenotasrigorousasmanyprovers.Theyarenotlogicallysoundreasoningsystems,butcollectionsofalgorithms.Weclassifysoundnessproblemsthatoccurincomputeralgebrasystems.Whilemanyalgorithmsandtheirimplementationsareperfectlytrustworthy,thesemanticsofsymbolsisoftenunclearandleadstoerrors.Ontheotherhand,morerobustapproachestointerfaceexternalreasonerstoproversarenotalwayspracticalbecausethemathematicaldepthofproofsalgorithmsincomputeralgebraarebasedoncanbeenormous.Ourownapproachtakesbothtrustworthinessoftheoverallsystemandeciencyintoaccount.Itreliesonusingonlyreliablepartsofacomputeralgebrasystem,whichcanbeachievedbychoosingasuitablelibrary,andderivingspecicationsforthesealgorithmsfromtheirliterature.WedesignandimplementaninterfacebetweentheproverIsabelleandthecomputeralgebralibrarySumitanduseittoprovenon-trivialtheoremsfromcodingtheory.Thisisbasedonthemechanisationofthealgebraictheoriesofringsandpolynomials.Codingtheoryisanareawhereproofsdohaveasubstantialamountofcomputationalcontent.Also,itisrealistictoassumethatthevericationofanencodingordecodingdevicecouldbeundertakenin,andindeed,besimpliedby,suchasystem.Thereasonwhysemanticsofsymbolsisoftenunclearincurrentcom-puteralgebrasystemsisnotmathematicaldiculty,butthedesignofthosesystems.ForGaussianeliminationweshowhowthesoundnessproblemcanbexedbyasmallextension,andwithoutlosingeciency.Thisisaprerequisitefortheecientuseofthealgorithminaprover.34PrefaceThistechnicalreportisintendedtomakemyPh.D.dissertationmoreeas-ilyaccessible.ThedissertationwassubmittedinJuneandthevivavoceexaminationtookplaceinSeptember1999.Thisrevisionincludessomeimprovementsthatweresuggestedbymyexaminers.Mymechanisationofthetheoryofringsandpolynomialsmaybeusefultothosewhoworkonthemechanisationofmathematicsfromthisarea.ItwillbecomepubliclyavailableaspartofthedistributionofthetheoremproverIsabelle.Pleaserefertotheprover’shomepages:://~isabelle/An\electronicversionofthisdocumentcanbeobtainedfrommyhomepage:1999byClemensBallarin.Allrightsreserved.56AcknowledgementsIwouldliketothankmysupervisorLarryPaulsonforsteeringmesafelythroughthe\adventurePh.D.Larryhadalwaystimetoanswermyques-tions,motivatedmewhenIthoughtthingsweregettingtoodicultandhadtherightdoseofcriticismwhenIconsideredthingssimplerthantheyactuallywere.Iwasimpressedbyhiseciency,andIadmirehisabilitytofocusonthatwhatisimportant.Goodresearchcanonlybedoneinastimulatingenvironment.TheComputerLaboratory,despiteitssomewhatshabbybuildingsandfurni-ture,provedtobeanexcellentplacetobe.IremembermanyinterestingdiscussionsoverteaandwouldliketothankeveryoneintheComputerLab-oratory|andbeyond|whohelpedmewiththisproject.ImustnotforgetJacquesCalmetwhoseceaselesseortstosetupinternationallinkswithinthescienticcommunitywerealsotomybenet.IdonotthinkIwouldhavedonemyPh.D.atsuchanexcellentplaceotherwise.TheStudienstiftungdesdeutschenVolkesandtheCambridgeEuropeanTrusthaveprovidedfundingformyresearch.TheComputerLaboratory,theUniversitatdesSaarlandesandDarwinCollegehelpedwithtravelcosts.Last,butbynomeansleast,Iwouldliketothankmyparentsfortheirsupport.ThatIwaslivingsofarawayhasnotalwaysbeeneasyforthem.78ToMarthaandMaria10ContentsListofFigures15ListofTables171Introduction191.1SymbolicComputation......................191.2ComputerAlgebra........................211.3TheoremProving.........................241.4ComputationalStrengthofProvers...............251.5SuitableDomainsofApplication................261.5.1Analysis..........................261.5.2Algebra..........................271.5.3GeneratingFunctionTechniques............271.5.4CodingTheory......................281.6OutlineoftheDissertation....................282MakingtheIntegrationTrustworthy312.1SoundnessinComputerAlgebra................322.1.1MisleadinglyUniformInterface.............322.1.2TheSpecialisationProblem...............342.1.3Algorithmsthatareadhoc...............352.2TrustandCerticates......................362.2.1ProofReconstruction...................362.2.2MetaTheoreticalExtensionoftheProver.......372.2.3TrusttheExternalReasoner..............392.3ReviewofEarlierWork.....................392.3.1Analytica.........................402.3.2InterfacebetweenIsabelleandMaple..........402.3.3BridgebetweenHOLandMaple............411112CONTENTS2.3.4Sapper...........................422.4OutlineofaNewApproach...................433DesignoftheInterface473.1Op