WITH UNTYPED LAMBDA-UNIFICATION

December7,200419:40WSPC/INSTRUCTIONFILEesforInternationalJournalonArtificialIntelligenceToolscWorldScientificPublishingCompanyOTTER-LAMBDA,ATHEOREM-PROVERWITHUNTYPEDLAMBDA-UNIFICATIONMICHAELBEESONComputerScienceDepartment,SanJos´eStateUniversity1WashingtonSquareSanJos´e,California95192,[e-mail]lusandanalgorithmforuntypedlambda-unificationhasbeenimplemented,startingfromthesourcecodeforOtter.TheresultisanewtheoremprovercalledOtter-λ.Thisisthefirsttimethataresolution-based,clause-languageprover(thataccumulatesdeducedclausesandusesstrategiestocontrolthedeductionandretentionofclauses)hasbeencombinedwithalambda-unificationalgorithmtoassistinthedeductions.Theresultingprovercombinestheadvantagesoftheproof-searchalgorithmofOtterandthepowerofhigher-orderunification.WedescribetheuntypedlambdaunificationalgorithmusedbyOtter-λandgiveseveralexampletheorems.Keywords:Unification;lambdacalculus;automateddeduction.IntroductionOurpurposeinthispaperistodemonstratethesuccessfulcombinationoflambdaunificationwiththewell-knownresolution-basedtheoremproverOtter19.Whatwecall“untypedlambdaunification”issimilartosecond-orderorhigher-orderunification,butthosealgorithmsaredesignedforuseintypedtheories,andwehavechosentouseanewnameforthisalgorithm,sinceitisanewalgorithmandisappliedinadifferentcontext.Theadvantagesofclause-basedproverslikeOtterlieintheretentionofdeducedconclusionsandthedevelopmentofeffectivesearchstrategiestogenerateand/orretaindesired,ratherthanundesired,newconclusions.Theadvantagesoftype-basedsystemsarethegreatereaseofdescribingmathematicalconceptsata“higherlevel”andtheavailabilityofhigher-orderunification.ByaddinglambdaunificationtoOtter,wehavecreatedasystemofferingacombinationofbothadvantages.TheimplementationoflambdacalculusandanalgorithmforlambdaunificationinOtteraredescribedinthelastsectionsofthispaper.Asoundnessproofforthealgorithmisgivenin6.Thatpaperanswersthequestion,InwhatlogicdoesOtter-λfindproofs?.ThispaperreportsonseveralexamplesintendedtodemonstratesomeofthecapabilitiesofOtter-λ,aswecallourenhancedversionofOtter(orwhen1December7,200419:40WSPC/INSTRUCTIONFILEesfor2MichaelBeesontypographydictates,Otter-lambda).Themainpointistoexplorethecombinationoflambdaunificationwithaclause-basedtheoremproverusingsearchstrategiestogeneratenewconclusions,asopposedtoeitheratype-basedprover(unaidedbyretentionofmanyclauses,demodulationandparamodulation,andavarietyofinferencestrategies)orafirst-order,clause-basedprover(unaidedbyhigher-orderunificationandtypes).First,weshowthatourenhancementsgiveOtter-λtheabilitytomanipulatequantifiersattheclausallevel,sothatdefinitionsinvolvingquantifierscanbecon-venientlyusedinproofs.Second,wetakeupthealgebraicpartofLagrange’stheo-rem,todemonstratehowlambdaunificationenablestheautomaticconstructionofmapsneededinalgebraicproofs.Third,wegiveanexampletoshowhowOtter-λcanfindaproofinalgebrathatusesmathematicalinduction,namely,therearenonilpotentsinanintegraldomain.Fourth,wereproducethewell-knownautomaticdeductionofCantor’stheorem,whichappearstodependheavilyonatypedlogicalsystem,toshowthatitcanbedoneinOtter-λ;andthatasimilarapproachinOtter-λcanyieldRussell’sparadoxandfixed-pointconstructions,whichcannotbeformalizedintypetheory.Ourfifthandlastexampleisaproofbymathematicalinduction,directlyfromtheaxiomsofPeanoarithmetic,ofthecommutativityofaddition.Boththebasiscaseandtheinductionstepofthemaininductionmustinturnbeprovedbymathematicalinduction.Otter-λisabletofindallthreeinstancesofinductiononitsown,andcompletetheproof.InputfilesandtheproofsproducedbyOtter-λforalltheseexamplescanbefoundontheOtter-λwebsite.7aLambdaunificationWefocusontheattempttoextendunificationtoinstantiatevariablesforfunctionsbymeansofλ-terms.Allpastresearchandimplementationinthissubjecthasinvolvedtypedformalisms.Inthatcontext,itisknownashigher-orderunification.Whatisnovelinthispaperistheimplementationof(aversionof)higher-orderunificationinanuntypedformalism.Wecallourunification“untypedlambda-unification”.In23,24,Pietrzykowskigaveanalgorithmforhigher-orderunification,whichweherecalltypedλ-unification.Huet17didnotinventthisalgorithm,buthiscitedpapercontainsanotherimportantcontributionandhasbecometheclassicreference.Anencyclopedictreatmentoftypetheoryandsecond-orderunificationcanbefoundin1,14;weshallsaynomoreaboutthethirtyyearsofresearchcoveredthere.Wenotethefollowingpointsaboutourimplementation:aToclearupsomemisconceptionsaboutOtter-λ:Itisatheorem-prover,builtonOtter,butitisnota“library”thatcanbepluggedintootherprovers,notevenOtter,sinceitwasnecessarytomodifyOtteratseveralpointstoconnectthenewcapabilities.Ontheotherhand,itperformsonfirst-orderproblemsexactlylikeOtter–thenewcodeisneverinvokedunlessappropriateflagsaresetintheinputfile.ThusOtterfilesruninOtter-λ,andatthesamespeed,thoughtheymayuseafewpercentmorememorysinceonedatastructurewasslightlyexpanded.December7,200419:40WSPC/INSTRUCTIONFILEesforOtter-lambda,atheorem-proverwithuntypedlambda-unification3•Wedonotimplementthefull(typed)higher-orderλ-unificationalgorithm.•Ouralgorithmcansolveproblemsw