出版時(shí)間:2006-9 出版社:機(jī)械工業(yè)出版社 作者:尼羅德
Tag標(biāo)簽:無(wú)
內(nèi)容概要
這是一本結(jié)合邏輯在計(jì)算機(jī)科學(xué)中的應(yīng)用來(lái)介紹數(shù)理邏輯的教科書,書中強(qiáng)調(diào)了演譯作為計(jì)算機(jī)的一種形的概念。雖然本書覆蓋了所有傳統(tǒng)的邏輯主題(語(yǔ)法,語(yǔ)義,完備性和緊致性),但是書中大部分討論的是其他主題,諸如消定理證明,邏輯式程序設(shè)計(jì)非經(jīng)典邏輯(模態(tài)邏輯和直覺主義邏輯),而這些主題在現(xiàn)代計(jì)算機(jī)科學(xué)中變得越來(lái)越理要。另外,本書還系統(tǒng)介紹了集合論基礎(chǔ)知識(shí),并對(duì)該主題提供了歷史綜述。
作者簡(jiǎn)介
作者:(美)尼羅德 等Anil Nerode 康奈大學(xué)數(shù)學(xué)系的創(chuàng)始人和教授,于1956年在芝加哥大學(xué)獲得博士學(xué)位。他的研究領(lǐng)域包括數(shù)理邏輯、自動(dòng)機(jī)、可計(jì)算理論、混合系統(tǒng)等。除本書外,他還與其他人合著了《Effective Completeness Theorems for Modal Logic》、《Tableaux for Constructive Concurrent Dynamic Logic》、《Logic,Categories,Lambda Calculus》等書。
書籍目錄
Preface IntroductionPropositional LogicOrders and TreesPropositions,Connectives and Truth TablesTruth Assignments and ValuationsTableau Proofs in Propositional CalculusSoundness and Completeness of Tableau ProofsDeductions From Prmises and CompactnessAn Axiomatic ApproachResolutionRefining ResolutionLinear Resolution,Horn Clausses and PrologPredicate LogicPredicates and QuantifiersThe Languange:Terms and FormulasFormation Trees,Structures and ListsSemantics:Meaning and TruthInterpretations of PROLOG ProgramsProofs:Complete Systemtic TableauxSoundness and Completeness of Tableau ProofsAn Axiomatic ApproachPrenex Normal Form and SkolemizationHerbrand's TheoremUnificationThe Unification AlgorithmResolutionRefining Resolution:Linear ResolutionPROLOGSLD-Resolution……
編輯推薦
這是一本結(jié)合邏輯在計(jì)算機(jī)科學(xué)中的應(yīng)用來(lái)介紹數(shù)理邏輯的教科書,書中強(qiáng)調(diào)了演譯作為計(jì)算機(jī)的一種形的概念。雖然本書覆蓋了所有傳統(tǒng)的邏輯主題(語(yǔ)法,語(yǔ)義,完備性和緊致性),但是書中大部分討論的是其他主題,諸如消定理證明,邏輯式程序設(shè)計(jì)非經(jīng)典邏輯(模態(tài)邏輯和直覺主義邏輯),而這些主題在現(xiàn)代計(jì)算機(jī)科學(xué)中變得越來(lái)越理要。另外,本書還系統(tǒng)介紹了集合論基礎(chǔ)知識(shí),并對(duì)該主題提供了歷史綜述。
圖書封面
圖書標(biāo)簽Tags
無(wú)
評(píng)論、評(píng)分、閱讀與下載