計算理論與符號邏輯

內(nèi)容概要

　　《計算理論與符號邏輯》對計算理論和數(shù)理邏輯中一組最為基本的問題和重要概念進行詳細介紹．以boolos等的經(jīng)典教材computability
and
logic為出發(fā)點，從教學(xué)效果出發(fā)，對內(nèi)容做了簡化和充實．本書注重體現(xiàn)數(shù)理邏輯在計算機科學(xué)研究中的應(yīng)用，強調(diào)直觀感受與理論分析相結(jié)合．對定義、定理的引入進行了精心設(shè)計，采用了易于理解的證明體例，重要章節(jié)之后都有小結(jié)．力圖引導(dǎo)讀者超越技術(shù)細節(jié)，更多地關(guān)注定義、定理背后所隱藏的一般思維模式和思想方法，使理論學(xué)習(xí)不再枯燥乏味．
　　《計算理論與符號邏輯》可作為數(shù)學(xué)、計算機科學(xué)相關(guān)專業(yè)的教材，對軟件工程、形式化方法、人工智能、數(shù)理邏輯等領(lǐng)域的研究者和工程技術(shù)人員提升理性思維的層次和分析能力大有裨益．

書籍目錄

第1章 緒論
　1.1 符號邏輯與計算機科學(xué)
　1.2 全書結(jié)構(gòu)
第2章 集合、關(guān)系和函數(shù)
　2.1 集合的基本概念
　2.2 集合的笛卡兒積
　2.3 關(guān)系
　2.4 函數(shù)
　習(xí)題
第3章 集合的可數(shù)性
　3.1 可數(shù)性的基本概念
　3.2 有結(jié)構(gòu)集合的可數(shù)性
　3.3 不可數(shù)性
　習(xí)題
第4章 圖靈可計算性
　4.1 能行可計算
　4.2 圖靈可計算性
　4.3 圖靈機的例子
　4.4 圖靈機的多種表示方法
　4.5 對定義4.2的進一步討論
　4.6 不可計算性
　4.7 圖靈論題與通用圖靈機
　習(xí)題
第5章 算盤可計算性
　5.1 算盤機的定義
　5.2 算盤機例子程序
　5.3 算盤可計算性
　5.4 將算盤機編譯為圖靈機
　習(xí)題
第6章 遞歸函數(shù)可計算性
第7章 遞歸函數(shù)與遞歸關(guān)系
第8章 不同計算模型之間的等價性
第9章 一階謂詞邏輯的基本概念
第10章 蘊涵關(guān)系的不可判定性
第11章 模型
第12章 緊致性定理的證明
第13章 形式化推理系統(tǒng)
第14章 計算行為的邏輯刻畫
第15章 godel不完全性定理
參考文獻
索引

章節(jié)摘錄

版權(quán)頁：插圖：人們自然會想到，前面所說的形式化方法是否會受到Godel不完全性定理的負面影響？是否存在這樣的程序，盡管其正確性斷言是真的，但在我們所使用的形式系統(tǒng)中根本就不存在其證明？從工程實踐的角度看，這種擔(dān)心是不必要的。如果人們在編程時足夠負責(zé)，一定會認真考慮為什么自己的程序是正確的，并給出充分的理由，這就是在試圖以某種方式構(gòu)造該程序的正確性證明。盡管這個證明可能有錯，并且只是短暫地出現(xiàn)在人們的腦海中，但它畢竟是存在的。人們絕對不會交付一個連自己都看不懂的程序。仍然以前面的哥德巴赫猜想的反例程序為例，我們構(gòu)造這個程序的目的只是想說明該程序的終止性問題與哥德巴赫猜想同構(gòu)，并不是真的要證明哥德巴赫猜想，因為我們的需求只是為了說明與哥德巴赫猜想的同構(gòu)，我們也知道為什么自己所寫的程序能滿足這一需求，所以，該程序與哥德巴赫猜想的同構(gòu)性證明是存在的，是可以被證明搜索程序找到的。在實際的軟件開發(fā)中，人們對軟件的需求以及軟件正確性的理由都是清楚的，只是沒有完整地表達出來而已，而形式化方法的本意只是借助于計算機輔助技術(shù)將不夠明晰的需求和正確性證明用符號邏輯中的斷言和推理顯式地表達出來并檢查其合法性，因此，形式化方法是可行的。也許人們還有這樣的疑問，是否會有這樣的情況：盡管我們知道軟件的正確性理由，但現(xiàn)有的形式系統(tǒng)表達能力不夠強，無法表述這些理由，這種擔(dān)心也是不必要的。因為形式系統(tǒng)總是可以擴展的。以Godel不完全性定理為例，雖然一個形式系統(tǒng)不能表述自己的一致性證明，但該證明可以在該系統(tǒng)之外的另外一個形式系統(tǒng)中表述，當然，這個另外的系統(tǒng)如果是一致的，也同樣不能表述自己的一致性證明。如果人們能發(fā)現(xiàn)某個命題是不可證明的，往往意味著他們對命題所在領(lǐng)域的認識有了升華，此時，為了繼續(xù)對該命題的討論，往往需要對形式系統(tǒng)進行修改擴展，引入新的公理或者新的推理規(guī)則構(gòu)成新的形式系統(tǒng)。Godel不完全性定理只是說：人類在認識上的升華是沒有止境的，認識升華導(dǎo)致新的形式系統(tǒng)，新的形式系統(tǒng)又會帶來新的問題，有待于認識上新的升華，落實到形式化方法，即使程序的正確性證明不能在現(xiàn)有的形式系統(tǒng)中表述，如果人們真的清楚自己的程序為什么是正確的，他們也應(yīng)該知道如何對現(xiàn)有的系統(tǒng)進行擴展來表述其正確性證明?；谏鲜稣J識，形式化方法是完全可行的。

編輯推薦

《計算理論與符號邏輯》是普通高等教育“十一五”國家級規(guī)劃教材之一。

圖書封面

圖書標簽Tags

無

評論、評分、閱讀與下載

---

    計算理論與符號邏輯 PDF格式下載

---