资源描述:
《Logic for Computer Science》由会员上传分享,免费在线阅读,更多相关内容在学术论文-天天文库。
1、LogicForComputerScienceFoundationsofAutomaticTheoremProvingCopyright2003,JeanH.GallierJune2003JeanGallierUniversityofPennsylvaniaDepartmentofComputerandInformationScience200South33rdStreetPhiladelphia,Pa19104USAe-mail:jean@saul.cis.upenn.eduToAnne,mywife,Mia,Philipp
2、eandSylvie,mychildren,andmymother,SimonePreface(2003Edition)Thisisaslightyrevisedversionofthe1985editionofmylogicbook.Manyty-posanderrorshavebeencorrectedandthelinedrawingshavebeenimproved.Mostmistakeswereminor,exceptforasubtleerrorinTheorem4.3.3.Indeed,thesecondpar
3、tofthetheoremaboutthecomplexityoftheprooftreeTob-tainedfromaresolutionrefutationDisfalse:ItisnotnecessarilythecasethatthenumberofleavesofTislessthanorequaltothenumberofresolutionstepsinD.Asaconsequence,Lemma4.3.4isalsofalse.Inthisrevisededition,wesimplyremovedallsta
4、tementsaboutthecom-plexityoftheconversionofresolutionrefutationsintoprooftrees.Hopefully,thispartofthebookisnowcorrect,aswellastherestofit!Somepartsofthebookhavenowaged,inparticular,thepartsaboutPROLOG.Also,eighteenyearslater,Iwouldprefertopresentsomeofthematerialin
5、adifferentorderandinadifferentmanner.Inparticular,Iwouldseparatemoreclearlythematerialontheresolutionmethod(Chapter4)fromthemoreproof-theoryorientedmaterial.However,Iconsiderthistoobigataskandthismildlyrevisedversionwillhavetodo(atleast,fornow!).Ideally,anumberoftopic
6、sshouldalsobecovered,forexample,somebasicsofconstructivelogic,linearlogic,temporallogicandmodelchecking.Again,thisistooformidableataskforasingleindividualandIhopethatreadersenjoythisnewversionofmybookanyway.Itshouldbenotedthatthisbookisof“preTEXvintage.”Thismeanstha
7、tLaTEXwasnotavailableatthetimethisbookwaswritten,whichimpliesthatIhadtowritemacros(stolenandadaptedfromD.KnuthblueTEXbook)todochapterheadings,etc.IalsohadtoadapttheinfamousmacrovviPreface(2003Edition)makeindextoproducethedreadedindex(whichwasturnedintofinalformusinga
8、PASCALprogram!).Thus,Iindulgedinthepracticeofthechangeofcatcodetoturnthesymbolˆintoanactivecharacter,amongotherstrangethings!Nevertheless,