Logic for Computer Science

Logic for Computer Science

ID:39716747

大小:2.12 MB

页数:534页

时间:2019-07-10

Logic for Computer Science_第页
预览图正在加载中,预计需要20秒,请耐心等待
资源描述:

《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,

当前文档最多预览五页,下载文档查看全文

此文档下载收益归作者所有

当前文档最多预览五页,下载文档查看全文
温馨提示:
1. 部分包含数学公式或PPT动画的文件,查看预览时可能会显示错乱或异常,文件下载后无此问题,请放心下载。
2. 本文档由用户上传,版权归属用户,天天文库负责整理代发布。如果您对本文档版权有争议请及时联系客服。
3. 下载前请仔细阅读文档内容,确认文档内容符合您的需求后进行下载,若出现内容与标题不符可向本站投诉处理。
4. 下载文档时可能由于网络波动等原因无法下载或下载错误,付费完成后未能成功下载的用户请联系客服处理。