Constraints and Theorem Proving Lecture Notes for

ConstraintsandTheoremProvingLectureNotesfortheInternationalSummerSchoolonConstraintsinComputationalLogics?HaraldGanzinger1andRobertNieuwenhuis21Max-Planck-InstitutfurInformatik,ImStadtwald,66123Saarbrucken,[e-mail]2TechnicalUniversityofCatalonia,JordiGirona1,08034Barcelona,[e-mail]1AbouttheselecturesSymbolicconstraintsprovideaconvenientwayofdescribingtheconnectionbetweendeductionatthelevelofgroundformulaeandthegeneralinferencesastheyarecomputedbyaproveronformulaewithvariables.Forinstance,eachresolutioninferencerepresentsinnitelymanygroundin-ferences,obtainedbysubstitutinggroundtermsforthevariablesintheclauses.Forrefutationalcompletenessonlycertainrestrictedcasesofgroundinferencesarerequired.Inthecaseoforderedresolution,essentialgroundinferencesonlyresolvemaximalliterals.Onthenon-groundlevel,theseorderingrestrictionscanberepresentedasakindofrestrictedquantication:onlygroundtermsthatsatisfytheorderingrestrictionsshouldbesubstitutedforthevariables.Thisleadsustoresolutioncalculiwithorder-constrainedclauses,whereineachin-ferencetheconclusionisrestrictedbytheorderingconstraintsofthecurrentdeductionstep,combinedwiththeconstraintsthatarealreadypresentinthepremises.Clauseswithunsatisableconstraintsrepresentnogroundclausesandcanhenceberemovedduringthedeductionprocess,thuspruningthesearchspace.Inthesenoteswewillmainlyfocusonsaturation-basedtheoremprovingmethodsincludingresolution,superpositionandchaining.Inthiscontext,apartfromorderingrestrictions,constraintsarealsousedtodescribeunicationprob-lems.Thispaperconsistofthreemainparts.Firstwewillintroducethemainconceptsforthecaseofpureequationallogic,whererewritingandKnuth/Bendixcompletionarefundamentaldeduc-tionmethods.ThetopicswhichwecoverwillincludeBirkho’stheorem,rst-ordervs.inductiveconsequences,termrewritesystems,conuence,termination,orderingsandcriticalpaircomputation(i.e.,superposition).Inthesecondpart,wewillextendtheseideastosaturation-basedmethodsforgeneralrst-orderclauses,includingsuperpositionandchaining-basedinference?BothauthorssupportedbytheESPRITworkinggroupCCL-II,ref.WG#22457.2systems,completenessproofsbymeansofthemodelgenerationmethodandanabstractnotionofredundancyforinferences.Thethirdpartwillcoverseveralextensions,withspecialattentiontothoseaspectsforwhichconstraintsplayanimportantrole,likebasicstrategies,de-ductionmoduloequationaltheories,constraint-basedredundancymethods,anddeduction-basedcomplexityanalysisanddecisionprocedures.Formoredetailsandfurtherreferencesthereaderisreferredto[BG98,NR99].2EqualityclausesWebrieyrecallsomebasicconceptsonrst-orderlogicwithequality.Inparticular,wegivethesyntaxandsemanticsforthefragmentofclausal(andhenceonlyuniversallyquantied)formulae.Wereferthereadertostandardtextbookssuchas[Fit90]forclausalnormalformtransformationsofarbitrarilyquantiedrst-orderformulae.2.1Syntax:terms,atoms,equations,andclausesLetFbeasetoffunctionsymbols,Xaninnitesetofvariables(disjointwithF),andafunctionarity:F!INassociatinganarity(anaturalnumber)toeachfunctionsymbol.Functionsymbolsfwitharity(f)=narecalledn-arysymbols.Inparticular,fiscalledunary,ifn=1,binary,ifn=2,andaconstantsymbol,ifn=0.T(F;X)denotesthesetoftermswithvariablesorsimplyterms:atermisavariableoranexpressionf(t1;:::;tn)wherefisann-aryfunctionsymbolandthetiaretermsfor1in.Notethattermscanbeseenasorderedtreeswheretheleavesarelabeledbyconstantsymbolsorvariables,andwhereeveryothernodeislabeledbyafunctionsymbolofarityatleast1.Thenodesintermscanbeaddressedbypositionswhicharesequencesofnaturalnumbers.Therootinatermisaddressedbyposition(denotingtheemptysequence)andifpistheaddressofanodevinthavingthen0successorsv1;:::;vn,thenthesehaveaddressesp:1;:::;p:n,respectively.Wesaythatafunctionsymboloravariableoccurs(atpositionp)inatermtifthenodeaddressedbypcarriesthatsymbolasalabel.Byvars(t)wedenotethesetofallvariablesoccurringint.LetPbeasetofpredicatesymbolswitharity(disjointfromFandX).Thenp(t1;:::;tn)isanatomifpisann-arypredicatesymbolandthetiaretermsfor1in.Inthesequelitwilloftensimplifymatterstechnicallytoalsoviewatomsastermsofaspecicsortwhich,inparticular,cannotoccuraspropersubtermsofotherterms.Bytjpwedenotethesubtermoftatpositionp:wehavetj=t,andf(t1;:::;tn)ji:p=tijpif1in(andisundenedifin).Wealsowritet[s]ptodenotethetermobtainedbyreplacingintthesubtermatpositionpbytheterms.Forexample,iftisf(a;g(b;h(c));d),thentj2:2:1=c,andt[d]2:2=f(a;g(b;d);d).3AmultisetoverasetSisafunctionM:S!IN.TheunionmultisetsisdenedbyM1[M2(x)=M1(x)+M2(x).Wesometimesalsouseaset-likenotation:M=fa;a;bgdenotesthemultisetMwhereM(a)=2,M(b)=1,andM(x)=0forx6=aandx6=b.Arst-orderclauseisapairofnitemultisetsofatoms(;),written!,whereiscalledtheantecedent,andthesuccedentoftheclause.Theemptyclause2isaclausewherebothandareempty,andaHornclauseisaclausewhosesuccedentcontainsatmostoneatom.Inclausesweoftenusecommatodenotetheunionofmultisetsortheinclusionofanatominamultiset;forexample,wewriteA;;0!insteadoffAg[[0!.Aliteraliseitheranatom(apositiveliteral)oranegationthere