加入VIP
  • 专属下载特权
  • 现金文档折扣购买
  • VIP免费专区
  • 千万文档免费下载

上传资料

关闭

关闭

关闭

封号提示

内容

首页 面向计算机科学的数理逻辑系统建模与推理

面向计算机科学的数理逻辑系统建模与推理.pdf

面向计算机科学的数理逻辑系统建模与推理

yongyong
2009-09-21 0人阅读 举报 0 0 暂无简介

简介:本文档为《面向计算机科学的数理逻辑系统建模与推理pdf》,可适用于工程科技领域

ThispageintentionallyleftblankLOGICINCOMPUTERSCIENCEModellingandReasoningaboutSystemsLOGICINCOMPUTERSCIENCEModellingandReasoningaboutSystemsMICHAELHUTHDepartmentofComputingImperialCollegeLondon,UnitedKingdomMARKRYANSchoolofComputerScienceUniversityofBirmingham,UnitedKingdomCAMBRIDGEUNIVERSITYPRESSCambridge,NewYork,Melbourne,Madrid,CapeTown,Singapore,SãoPauloCambridgeUniversityPressTheEdinburghBuilding,CambridgeCBRU,UKFirstpublishedinprintformatISBNISBN©CambridgeUniversityPressInformationonthistitle:wwwcambridgeorgThispublicationisincopyrightSubjecttostatutoryexceptionandtotheprovisionofrelevantcollectivelicensingagreements,noreproductionofanypartmaytakeplacewithoutthewrittenpermissionofCambridgeUniversityPressISBNISBNXCambridgeUniversityPresshasnoresponsibilityforthepersistenceoraccuracyofurlsforexternalorthirdpartyinternetwebsitesreferredtointhispublication,anddoesnotguaranteethatanycontentonsuchwebsitesis,orwillremain,accurateorappropriatePublishedintheUnitedStatesofAmericabyCambridgeUniversityPress,NewYorkwwwcambridgeorgpaperbackeBook(EBL)eBook(EBL)paperbackContentsForewordtothefirsteditionpageixPrefacetothesecondeditionxiAcknowledgementsxiiiPropositionallogicDeclarativesentencesNaturaldeductionRulesfornaturaldeductionDerivedrulesNaturaldeductioninsummaryProvableequivalenceAnaside:proofbycontradictionPropositionallogicasaformallanguageSemanticsofpropositionallogicThemeaningoflogicalconnectivesMathematicalinductionSoundnessofpropositionallogicCompletenessofpropositionallogicNormalformsSemanticequivalence,satisfiabilityandvalidityConjunctivenormalformsandvalidityHornclausesandsatisfiabilitySATsolversAlinearsolverAcubicsolverExercisesBibliographicnotesPredicatelogicTheneedforaricherlanguagevviContentsPredicatelogicasaformallanguageTermsFormulasFreeandboundvariablesSubstitutionProoftheoryofpredicatelogicNaturaldeductionrulesQuantifierequivalencesSemanticsofpredicatelogicModelsSemanticentailmentThesemanticsofequalityUndecidabilityofpredicatelogicExpressivenessofpredicatelogicExistentialsecondorderlogicUniversalsecondorderlogicMicromodelsofsoftwareStatemachinesAlma–revisitedAsoftwaremicromodelExercisesBibliographicnotesVerificationbymodelcheckingMotivationforverificationLineartimetemporallogicSyntaxofLTLSemanticsofLTLPracticalpatternsofspecificationsImportantequivalencesbetweenLTLformulasAdequatesetsofconnectivesforLTLModelchecking:systems,tools,propertiesExample:mutualexclusionTheNuSMVmodelcheckerRunningNuSMVMutualexclusionrevisitedTheferrymanThealternatingbitprotocolBranchingtimelogicSyntaxofCTLContentsviiSemanticsofCTLPracticalpatternsofspecificationsImportantequivalencesbetweenCTLformulasAdequatesetsofCTLconnectivesCTL*andtheexpressivepowersofLTLandCTLBooleancombinationsoftemporalformulasinCTLPastoperatorsinLTLModelcheckingalgorithmsTheCTLmodelcheckingalgorithmCTLmodelcheckingwithfairnessTheLTLmodelcheckingalgorithmThefixedpointcharacterisationofCTLMonotonefunctionsThecorrectnessofSATEGThecorrectnessofSATEUExercisesBibliographicnotesProgramverificationWhyshouldwespecifyandverifycodeAframeworkforsoftwareverificationAcoreprogramminglanguageHoaretriplesPartialandtotalcorrectnessProgramvariablesandlogicalvariablesProofcalculusforpartialcorrectnessProofrulesProoftableauxAcasestudy:minimalsumsectionProofcalculusfortotalcorrectnessProgrammingbycontractExercisesBibliographicnotesModallogicsandagentsModesoftruthBasicmodallogicSyntaxSemanticsLogicengineeringThestockofvalidformulasviiiContentsImportantpropertiesoftheaccessibilityrelationCorrespondencetheorySomemodallogicsNaturaldeductionReasoningaboutknowledgeinamultiagentsystemSomeexamplesThemodallogicKTnNaturaldeductionforKTnFormalisingtheexamplesExercisesBibliographicnotesBinarydecisiondiagramsRepresentingbooleanfunctionsPropositionalformulasandtruthtablesBinarydecisiondiagramsOrderedBDDsAlgorithmsforreducedOBDDsThealgorithmreduceThealgorithmapplyThealgorithmrestrictThealgorithmexistsAssessmentofOBDDsSymbolicmodelcheckingRepresentingsubsetsofthesetofstatesRepresentingthetransitionrelationImplementingthefunctionspre∃andpre∀SynthesisingOBDDsArelationalmucalculusSyntaxandsemanticsCodingCTLmodelsandspecificationsExercisesBibliographicnotesBibliographyIndexForewordtothefirsteditionbyEdmundMClarkeFORESystemsProfessorofComputerScienceCarnegieMellonUniversityPittsburgh,PAFormalmethodshavefinallycomeofage!Specificationlanguages,theoremprovers,andmodelcheckersarebeginningtobeusedroutinelyinindustryMathematicallogicisbasictoallofthesetechniquesUntilnowtextbooksonlogicforcomputerscientistshavenotkeptpacewiththedevelopmentoftoolsforhardwareandsoftwarespecificationandverificationForexample,inspiteofthesuccessofmodelcheckinginverifyingsequentialcircuitdesignsandcommunicationprotocols,untilnowIdidnotknowofasingletext,suitableforundergraduateandbeginninggraduatestudents,thatattemptstoexplainhowthistechniqueworksAsaresult,thismaterialisrarelytaughttocomputerscientistsandelectricalengineerswhowillneedtouseitaspartoftheirjobsinthenearfutureInstead,engineersavoidusingformalmethodsinsituationswherethemethodswouldbeofgenuinebenefitorcomplainthattheconceptsandnotationusedbythetoolsarecomplicatedandunnaturalThisisunfortunatesincetheunderlyingmathematicsisgenerallyquitesimple,certainlynomoredifficultthantheconceptsfrommathematicalanalysisthateverycalculusstudentisexpectedtolearnLogicinComputerSciencebyHuthandRyanisanexceptionalbookIwasamazedwhenIlookedthroughitforthefirsttimeInadditiontopropositionalandpredicatelogic,ithasaparticularlythoroughtreatmentoftemporallogicandmodelcheckingInfact,thebookisquiteremarkableinhowmuchofthismaterialitisabletocover:linearandbranchingtimetemporallogic,explicitstatemodelchecking,fairness,thebasicfixpointixxForewordtothefirsteditiontheoremsforcomputationtreelogic(CTL),evenbinarydecisiondiagramsandsymbolicmodelcheckingMoreover,thismaterialispresentedatalevelthatisaccessibletoundergraduateandbeginninggraduatestudentsNumerousproblemsandexamplesareprovidedtohelpstudentsmasterthematerialinthebookSincebothHuthandRyanareactiveresearchersinlogicsofprogramsandprogramverification,theywritewithconsiderableauthorityInsummary,thematerialinthisbookisuptodate,practical,andelegantlypresentedThebookisawonderfulexampleofwhatamoderntextonlogicforcomputerscienceshouldbelikeIrecommendittothereaderwithgreatestenthusiasmandpredictthatthebookwillbeanenormoussuccess(Thisforewordisreprintedinthesecondeditionwithitsauthor’spermission)PrefacetothesecondeditionOurmotivationfor(re)writingthisbookOneoftheleitmotifsofwritingthefirsteditionofourbookwastheobservationthatmostlogicsusedinthedesign,specificationandverificationofcomputersystemsfundamentallydealwithasatisfactionrelationM�φwhereMissomesortofsituationormodelofasystem,andφisaspecification,aformulaofthatlogic,expressingwhatshouldbetrueinsituationMAttheheartofthissetupisthatonecanoftenspecifyandimplementalgorithmsforcomputing�Wedevelopedthisthemeforpropositional,firstorder,temporal,modal,andprogramlogicsBasedontheencouragingfeedbackreceivedfromfivecontinentswearepleasedtoherebypresentthesecondeditionofthistextwhichmeanstopreserveandimproveontheoriginalintentofthefirsteditionWhat’snewandwhat’sgoneChapternowdiscussesthedesign,correctness,andcomplexityofaSATsolver(amarkingalgorithmsimilartoSt˚almarck’smethodSS)forfullpropositionallogicChapternowcontainsbasicresultsfrommodeltheory(CompactnessTheoremandLo¨wenheim–SkolemTheorem)asectiononthetransitiveclosureandtheexpressivenessofexistentialanduniversalsecondorderlogicandasectionontheuseoftheobjectmodellinglanguageAlloyanditsanalyserforspecifyingandexploringunderspecifiedfirstorderlogicmodelswithrespecttopropertieswritteninfirstorderlogicwithtransitiveclosureTheAlloylanguageisexecutablewhichmakessuchexplorationinteractiveandformalxixiiPrefacetothesecondeditionChapterhasbeencompletelyrestructuredItnowbeginswithadiscussionoflineartimetemporallogicfeaturestheopensourceNuSMVmodelcheckingtoolthroughoutandincludesadiscussiononplanningproblems,morematerialontheexpressivenessoftemporallogics,andnewmodellingexamplesChaptercontainsmorematerialontotalcorrectnessproofsandanewsectionontheprogrammingbycontractparadigmofverifyingprogramcorrectnessChaptersandhavealsobeenrevised,withmanysmallalterationsandcorrectionsTheinterdependenceofchaptersandprerequisitesThebookrequiresthatstudentsknowthebasicsofelementaryarithmeticandnaivesettheoreticconceptsandnotationThecorematerialofChapter(everythingexceptSectionsto)isessentialforallofthechaptersthatfollowOtherthanthat,onlyChapterdependsonChapterandabasicunderstandingofthestaticscopingrulescoveredinChapter–althoughonemayeasilycoverSectionsandwithouthavingdoneChapteratallRoughly,theinterdependencediagramofchaptersisWWWpageThisbookissupportedbyaWebpage,whichcontainsalistoferratatextfilesforalltheprogramcodeancillarytechnicalmaterialandlinksallthefiguresaninteractivetutorbasedonmultiplechoicequestionsanddetailsofhowinstructorscanobtainthesolutionstoexercisesinthisbookwhicharemarkedwitha∗TheURLforthebook’spageiswwwcsbhamacukresearchlicsSeealsowwwcambridgeorgxAcknowledgementsManypeoplehave,directlyorindirectly,assistedusinwritingthisbookDavidSchmidtkindlyprovidedserveralexercisesforChapterKrysiaBrodahaspointedoutsometypographicalerrorsandsheandtheotherauthorsofBEKVhaveallowedustousesomeexercisesfromthatbookWehavealsoborrowedexercisesorexamplesfromHodandFHMVSusanEisenbachprovidedafirstdescriptionofthePackageDependencySystemthatwemodelinAlloyinChapterDanielJacksonmakeveryhelpfulcommentsonversionsofthatsectionZenaMatildeAriola,JoshHodas,JanKomorowski,SergeyKotov,ScottASmolkaandSteveVickershavecorrespondedwithusaboutthistexttheircommentsareappreciatedMattDwyerandJohnHatcliffmadeusefulcommentsondraftsofChapterKevinLucasprovidedinsightfulcommentsonthecontentofChapter,andnotifiedusofnumeroustypographicalerrorsinseveraldraftsofthebookAchimJungreadseveralchaptersandgaveusefulfeedbackAdditionally,anumberofpeoplereadandprovidedusefulcommentsonseveralchapters,includingMotiBenAri,GrahamClark,ChristianHaack,AnthonyHook,RobertoSegala,AlanSextonandAllenStoughtonNumerousstudentsatKansasStateUniversityandtheUniversityofBirminghamhavegivenusfeedbackofvariouskinds,whichhasinfluencedourchoiceandpresentationofthetopicsWeacknowledgePaulTaylor’sLATEXpackageforproofboxesAbouthalfadozenanonymousrefereesmadecritical,butconstructive,commentswhichhelpedtoimprovethistextinvariouswaysInspiteofthesecontributions,theremaystillbeerrorsinthebook,andwealonemusttakeresponsibilityforthoseAddedforsecondeditionManypeoplehavehelpedimprovethistextbypointingouttyposandmakingotherusefulcommentsafterthepublicationdateAmongthem,xiiixivAcknowledgementswementionWolfgangAhrendt,YasuhiroAjiro,TorbenAmtoft,StephanAndrei,BernhardBeckert,JonathanBrown,JamesCaldwell,RuchiraDatta,AmyFelty,DimitarGuelev,HirotsuguKakugawa,KamranKashef,MarkusKro¨tzsch,JagunKwon,RankoLazic,DavidMakinson,AlexanderMiczo,AartMiddeldorp,RobertMorelli,PrakashPanangaden,AileenParaguya,FrankPfenning,ShekharPradhan,KoichiTakahashi,KazunoriUeda,HiroshiWatanabe,FuzhiWangandReinhardWilhelmPropositionallogicTheaimoflogicincomputerscienceistodeveloplanguagestomodelthesituationsweencounterascomputerscienceprofessionals,insuchawaythatwecanreasonaboutthemformallyReasoningaboutsituationsmeansconstructingargumentsaboutthemwewanttodothisformally,sothattheargumentsarevalidandcanbedefendedrigorously,orexecutedonamachineConsiderthefollowingargument:ExampleIfthetrainarriveslateandtherearenotaxisatthestation,thenJohnislateforhismeetingJohnisnotlateforhismeetingThetraindidarrivelateTherefore,thereweretaxisatthestationIntuitively,theargumentisvalid,sinceifweputthefirstsentenceandthethirdsentencetogether,theytellusthatiftherearenotaxis,thenJohnwillbelateThesecondsentencetellsusthathewasnotlate,soitmustbethecasethatthereweretaxisMuchofthisbookwillbeconcernedwithargumentsthathavethisstructure,namely,thatconsistofanumberofsentencesfollowedbytheword‘therefore’andthenanothersentenceTheargumentisvalidifthesentenceafterthe‘therefore’logicallyfollowsfromthesentencesbeforeitExactlywhatwemeanby‘followsfrom’isthesubjectofthischapterandthenextoneConsideranotherexample:ExampleIfitisrainingandJanedoesnothaveherumbrellawithher,thenshewillgetwetJaneisnotwetItisrainingTherefore,JanehasherumbrellawithherThisisalsoavalidargumentCloserexaminationrevealsthatitactuallyhasthesamestructureastheargumentofthepreviousexample!AllwehavePropositionallogicdoneissubstitutedsomesentencefragmentsforothers:ExampleExamplethetrainislateitisrainingtherearetaxisatthestationJanehasherumbrellawithherJohnislateforhismeetingJanegetswetTheargumentineachexamplecouldbestatedwithouttalkingabouttrainsandrain,asfollows:Ifpandnotq,thenrNotrpTherefore,qIndevelopinglogics,wearenotconcernedwithwhatthesentencesreallymean,butonlyintheirlogicalstructureOfcourse,whenweapplysuchreasoning,asdoneabove,suchmeaningwillbeofgreatinterestDeclarativesentencesInordertomakeargumentsrigorous,weneedtodevelopalanguageinwhichwecanexpresssentencesinsuchawaythatbringsouttheirlogicalstructureThelanguagewebeginwithisthelanguageofpropositionallogicItisbasedonpropositions,ordeclarativesentenceswhichonecan,inprinciple,argueasbeingtrueorfalseExamplesofdeclarativesentencesare:()Thesumofthenumbersandequals()JanereactedviolentlytoJack’saccusations()Everyevennaturalnumber>isthesumoftwoprimenumbers()AllMartianslikepepperoniontheirpizza()AlbertCamuse´taitune´crivainfranc¸ais()DieWu¨rdedesMenschenistunantastbarThesesentencesarealldeclarative,becausetheyareinprinciplecapableofbeingdeclared‘true’,or‘false’Sentence()canbetestedbyappealingtobasicfactsaboutarithmetic(andbytacitlyassuminganArabic,decimalrepresentationofnaturalnumbers)Sentence()isabitmoreproblematicInordertogiveitatruthvalue,weneedtoknowwhoJaneandJackareandperhapstohaveareliableaccountfromsomeonewhowitnessedthesituationdescribedInprinciple,eg,ifwehadbeenatthescene,wefeelthatwewouldhavebeenabletodetectJane’sviolentreaction,providedthatitindeedoccurredinthatwaySentence(),knownasGoldbach’sconjecture,seemsstraightforwardonthefaceofitClearly,afactaboutallevennumbers>iseithertrueorfalseButtothisdaynobodyknowswhethersentence()expressesatruthornotItisevennotclearwhetherthiscouldbeshownbysomefinitemeans,evenifitweretrueHowever,inDeclarativesentencesthistextwewillbecontentwithsentencesassoonastheycan,inprinciple,attainsometruthvalueregardlessofwhetherthistruthvaluereflectstheactualstateofaffairssuggestedbythesentenceinquestionSentence()seemsabitsilly,althoughwecouldsaythatifMartiansexistandeatpizza,thenallofthemwilleitherlikepepperonionitornot(WehavetointroducepredicatelogicinChaptertoseethatthissentenceisalsodeclarativeifnoMartiansexistitisthentrue)Again,forthepurposesofthistextsentence()willdoEtalors,qu’estcequ’onpensedesphrases()et()Sentences()and()arefineifyouhappentoreadFrenchandGermanabitThus,declarativestatementscanbemadeinanynatural,orartificial,languageThekindofsentenceswewon’tconsiderherearenondeclarativeones,like�Couldyoupleasepassmethesalt�Ready,steady,go!�MayfortunecomeyourwayPrimarily,weareinterestedinprecisedeclarativesentences,orstatementsaboutthebehaviourofcomputersystems,orprogramsNotonlydowewanttospecifysuchstatementsbutwealsowanttocheckwhetheragivenprogram,orsystem,fulfilsaspecificationathandThus,weneedtodevelopacalculusofreasoningwhichallowsustodrawconclusionsfromgivenassumptions,likeinitialisedvariables,whicharereliableinthesensethattheypreservetruth:ifallourassumptionsaretrue,thenourconclusionoughttobetrueaswellAmuchmoredifficultquestio

用户评价(0)

关闭

新课改视野下建构高中语文教学实验成果报告(32KB)

抱歉,积分不足下载失败,请稍后再试!

提示

试读已结束,如需要继续阅读或者下载,敬请购买!

文档小程序码

使用微信“扫一扫”扫码寻找文档

1

打开微信

2

扫描小程序码

3

发布寻找信息

4

等待寻找结果

我知道了
评分:

/49

面向计算机科学的数理逻辑系统建模与推理

仅供在线阅读

VIP

在线
客服

免费
邮箱

爱问共享资料服务号

扫描关注领取更多福利