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

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

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

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

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