可計算性邏輯中CL2系統(tǒng)的可判定性及空間復(fù)雜性分析.pdf

1、可計算性(computability)，即算法有解性，是數(shù)學(xué)和計算機科學(xué)領(lǐng)域中最重要的概念之一?？捎嬎阈赃壿嫞–omputability Logic，簡寫為CoL）是研究可計算性的形式理論，它將問題看作是計算機（或者以計算機為表現(xiàn)形式的人）與外部環(huán)境之間的博弈，問題的可計算性是指存在一臺計算機能贏得這個博弈。傳統(tǒng)邏輯主要回答什么是永真的、有效的，而可計算性邏輯試圖系統(tǒng)的回答什么是可計算的及應(yīng)如何計算。CoL中的公式代表交互計算問題，邏輯

2、運算代表在可計算問題上的交互操作，一個公式是有效的是指存在解決相應(yīng)問題的方法（或者等價的，存在贏得博弈的策略）。
　　 本文首先介紹了可計算性邏輯的博弈語義及其形式化的定義，給出了CoL中的(～)、∧、∨、(∩)、(∪)和→等邏輯運算表達的意義及其形式化定義。博弈分為靜態(tài)博弈和動態(tài)博弈，靜態(tài)博弈是與博弈雙方反應(yīng)速度無關(guān)的博弈，其最終結(jié)果只取決于博弈的策略。CoL所研究的博弈問題都是靜態(tài)博弈。HPM(hard-playmachin

3、e)是交互計算機模型的最基本模型，它是在一種圖靈機模型基礎(chǔ)上修改得到的計算機模型。另一種計算模型是EPM(easy-play machine)，它與HPM在設(shè)計上唯一的區(qū)別在于只有當(dāng)計算機明確的允許環(huán)境行動時環(huán)境才可以做一個行動。對于靜態(tài)博弈問題來說，這兩種模型是等價的。在實際解決問題的過程中，我們更傾向于采用EPM模型。
　　 CL2邏輯采用博弈的語義，是對經(jīng)典命題邏輯的保守擴展，比經(jīng)典命題邏輯更富有表達力和更廣闊的應(yīng)用前景，

4、并且有較高的證明效率。與經(jīng)典命題邏輯相比，CL2邏輯包含兩類原子:簡單原子和一般原子。簡單原子代表簡單計算問題，它與經(jīng)典命題邏輯中的謂詞相對應(yīng);一般原子代表一般的交互計算問題，在意義上有別于謂詞。經(jīng)典邏輯的真的概念就相當(dāng)于CL2中的可計算性的概念。CL2邏輯系統(tǒng)已經(jīng)被證明了是完備的、可靠的邏輯系統(tǒng)。
　　 本文的創(chuàng)新點在于:
　　 (1).分析CL2系統(tǒng)的可判定性。提出判斷CL2公式可證明性的算法，并且證明該算法是多項式