源地址:http://blog.sina.com.cn/s/blog_4b700c4c0100j7h9.html
研究计算的一般性质的数学理论,也称算法理论或能行性理论。它通过建立计算的数学模型(例如抽象计算机),精确区分哪些是可计算的,哪些是不可计算的。计算的过程就是执行
算法
的过程。可计算性理论的重要课题之一,是将算法这一直观概念精确化。算法概念精确化的途径很多,其中之一是通过定义抽象计算机,把算法看作抽象计算机的程序。通常把那些存在算法计算其值的函数叫作可计算函数。因此,可计算函数的精确定义为:能够在抽象计算机上编出程序计算其值的函数。这样就可以讨论哪些函数是可计算的,哪些函数是不可计算的。
产生和历史
可计算性理论起源于对数学基础问题的研究。20世纪30年代,为了讨论是否对于每个问题都有解决它的算法,数理逻辑学家提出了几种不同的算法定义。K.哥德尔和S.C.克林尼提出了递归函数的概念,A.丘奇提出
λ转换演算
,
A.M.图灵
和E.波斯特各自独立地提出了抽象计算机的概念(后人把图灵提出的抽象计算机称为
图灵机
),并且证明了这些数学模型的计算能力是一样的,即它们是等价的。著名的丘奇-图灵论题也是丘奇和图灵在这一时期各自独立提出的。后来,人们又提出许多等价的数学模型,如A.马尔可夫于40年代提出的正规算法(后人称之为马尔可夫算法),60年代前期提出的随机存取机器模型(简称 RAM)等。50年代末和60年代初,胡世华和J.麦克阿瑟等人各自独立地提出了定义在字符串上的递归函数。
学科内容
若
m
和
n
是两个正整数,并且
m
≥
n
时,求
m
和
n
的最大公因子的欧几里得算法可表示为
E
1
[求余数]以
n
除
m
得余数
r
。
E
2
[余数为0吗?]若
r
=0,计算结束,
n
即为答案;否则转到步骤
E
3
。
E
3
[互换]把
m
的值变为
n
,
n
的值变为
r
,重复上述步骤。
依照这三条规则指示的步骤,可计算出任何两个正整数的最大公因子。可以把计算过程看成执行这些步骤的序列。我们发现,计算过程是有穷的,而且计算的每一步都是能够机械实现的(机械性)。为了精确刻划算法的特征,人们建立了各种各样的数学模型。
图灵机
一种在理论计算机科学中广泛采用的抽象计算机,它是图灵在1936年提出的,用于精确描述算法的特征。可用一个图灵机来计算其值的函数是可计算函数,找不到图灵机来计算其值的函数是不可计算函数。可以证明,存在一个图灵机U,它可以模拟任何其他的图灵机。这样的图灵机 U称为通用图灵机。通用图灵机正是后来出现的存储指令的通用数字计算机的理论原型。
λ转换演算
一种定义函数的形式演算系统,是A.丘奇于1935年为精确定义可计算性而提出的。他引进λ记号以明确区分函数和函数值,并把函数值的计算归结为按一定规则进行一系列转换,最后得到函数值。按照λ转换演算能够得到函数值的那些函数称为λ可定义函数(见
λ转换演算
)。
丘奇-图灵论题
可计算性理论的基本论题,也称图灵论题,它规定了直观可计算函数的精确含义。丘奇论题说:λ可定义函数类与直观可计算函数类相同。图灵论题说:图灵机可计算函数类与直观可计算函数类相同。图灵证明了图灵机可计算函数类与λ可定义函数类相同。这表明图灵论题和丘奇论题讲的是一回事,因此把它们统称为丘奇-图灵论题。直观可计算函数不是一个精确的数学概念,因此丘奇-图灵论题是不能加以证明的。30年代以来,人们提出了许多不同的计算模型来精确刻划可计算性,并且证明了这些模型都与图灵机等价。这表明图灵机和其他等价的模型确实合理地定义了可计算性,因此丘奇-图灵论题得到了计算机科学界和数学界的公认。
原始递归函数
自变量值和函数值都是自然数的函数,称为数论函数。原始递归函数是数论函数的一部分。首先规定少量显然直观可计算的函数为原始递归函数,它们是:函数值恒等于0的零函数
C
0
,函数值等于自变量值加1的后继函数
S
,函数值等于第
i
个自变量值的
n
元投影函数
P
嬪。然后规定,原始递归函数的合成仍是原始递归函数,可以由已知原始递归函数简单递归地计算出函数值的函数仍是原始递归函数。例如,和函数
f
(
x
,
y
)=
x
+
y
可由原始递归函数
P
(1)
1
和
S
递归地计算出函数值
f
(
x
,0)=
P
(1)
1
(
x
)
f
(
x
,
S
(
y
))=
S
(
f
(
x
,
y
))
比如,
f
(4,2)可这样计算,首先算出
f
(4,0)=
P
(1)
1
(4)=4,然后计算
f
(4,1)=
S
(
f
(4,0))=
S
(4)=5
f
(4,2)=
S
(
f
(4,1))=
S
(5)=6
因此,和函数是原始递归函数。显然,一切原始递归函数都是直观可计算的。许多常用的处处有定义的函数都是原始递归函数,但并非一切直观可计算的、处处有定义的函数都是原始递归函数。
部分递归函数
为了包括所有的直观可计算函数,需要把原始递归函数类扩充为部分递归函数类。设
g
(
x
1
,…,
x
n
,
z
)是原始递归函数,如果存在自然数
z
使
g
(
x
1
,…,
x
n
,
z
)=0,就取
f
(
x
1
,…,
x
n
)的值为满足
g
(
x
1
,…,
x
n
,
z
)=0的最小的自然数
z
;如果不存在使
g
(
x
1
,…,
x
n
,
z
)=0的自然数
z
,就称
f
(
x
1
,…,
x
n
)无定义。把如上定义的函数
f
加到原始递归函数类中,就得到部分递归函数类。因为不能保证如上定义的
f
在一切点都有定义,故称其为部分函数。处处有定义的部分递归函数称为递归函数。部分递归函数类与图灵机可计算函数类相同。对于每个
n
元部分递归函数
f
,可以编一个计算机程序
P
,以自然数
x
1
,…,
x
n
作为输入,若
f
(
x
1
,…,
x
n
)有定义,则
P
函数值执行终止并输出的
f
(
x
1
,…,
x
n
),否则
P
不终止。
递归集
递归集最初是对于元素都是自然数的集合定义的,它们是有算法确定每个自然数是否为其元素的集合。可以将递归集的概念推广到其他集合。所讨论的对象的全体称为域,如果有算法确定域中任意元素是否属于
A
,则称
A
为递归集。对于每个递归集,可以编一个计算机程序,以域中任意元素作为输入,计算执行该程序都可给出适当的输出,表明该元素是否属于这个递归集。有许多集合不是递归集。
递归可枚举集
如果对于集合
A
可以编一个程序
P
,输入域中任意元素
x
,若
x
∈
A
,则
P
的执行将终止并输出“是”,否则
P
的执行不终止,就称
A
为递归可枚举集。
A
为递归可枚举集的充分必要条件是可以编一个程序枚举
A
的元素,即打印
A
的元素,使得对于
A
中任意元素,只要时间足够长总会在打印纸上出现。递归集都是递归可枚举集,但有些递归可枚举集不是递归集。有许多集合不是递归可枚举集。
可判定性和半可判定性
判定问题是无穷多个同类个别问题的总称。例如,2是不是素数?6是不是素数?这些都是个别问题,把这类个别问题概括起来,就得到一个判定问题:任意给定的正整数是不是素数?这里的正整数集合称为该判定问题的域,给定域中的一个元素,判定问题就对应一个个别问题。对于一个判定问题,如果能够编出一个程序,以域中任意元素作为输入,执行该程序就能给出相应的个别问题的答案,就称该判定问题为可判定的。例如,“任意正整数是不是素数”这个问题就是可判定的。对于集合
A
,域中任意元素是否属于它的问题称为集合
A
对应的判定问题。集合是递归集的充分必要条件为对应的判定问题是可判定的。因此,全体素数的集合是递归集。
对于一个判定问题,如果能够编出一个程序
P
,以域中任意元素作为输入,当相应的个别问题的解答是肯定的时候,
P
的执行将终止并输出“是”,否则
P
的执行不终止,就称该判定问题为半可判定的。可判定的问题总是半可判定的。集合是递归可枚举集的充分必要条件为对应的判定问题是半可判定的。
图灵在1936年证明,图灵机的停机问题是不可判定的,即不存在一个图灵机能够判定任意图灵机对于任意输入是否停机。图灵机的停机问题是半可判定的。图灵机的停机问题是很重要的,由它可以推出计算机科学、数学、逻辑学中的许多问题是不可判定的。
应用
可计算性理论是计算机科学的理论基础之一。早在30年代,图灵对存在通用图灵机的逻辑证明表明,制造出能编程序来作出任何计算的通用计算机是可能的,这影响了40年代出现的存储程序计算机(即诺伊曼型计算机)的设计思想。可计算性理论确定了哪些问题可能用计算机解决,哪些问题不可能用计算机解决。例如,图灵机的停机问题是不可判定的表明,不可能用一个单独的程序来判定任意程序的执行是否终止,避免了人们为编制这样的程序而无谓地浪费精力。
可计算性理论中的基本思想、概念和方法,被广泛应用于计算机科学的各个领域。建立数学模型的方法在计算机科学中被广泛采用。递归的思想被用于程序设计,产生了递归过程和递归数据结构,也影响了计算机的体系结构。λ演算被用于研究程序设计语言的语义,例如,表处理语言就以λ转换演算为理论基础。
参考书目
H.Rogers,
Theory of Recursive Functions and Effective Computability
, McGraw-Hill, New York,1967.
F. Hennie,
Introduction to Computability
,Addison-Wesley, Masschusetts,1977.
可判定性
:一个语言
L
,是一个
集合
,且其
补集
为
。当
L
是
图灵机
可识别时,语言
L
则称为半可判定。当语言
L
不是图灵机可识别,则为不可判定语言。当且仅当
L
和
都是图灵机可识别的时候,L才能称为可判定语言。
不可判定性 |
IndecidalHlity |
不可判定性 【1”‘cida城勿;一epa3pe“HMocT‘1 【补注】一个 算法 (日即riUllll)的不 存在 性,或者在一个 形式系统 (forn以1 systeTn)中 证明 或否证一个命题的不可能性.下面分别予以讨论.解决某一给定问题的算法的不存在性常常称为该问题的 不可解性 (un- solvabiljty).有时“不可判定性”和“不可解性”看作 是同义词.(见不可解性(unsolvability).) 在一切 数学 领域中都可得到判 定性 结果,它们可能以算法的 直观 概念 为依据.由 构造 一个算法证明一个问题是可判定的,该算法在接收该问题一个例子的 数据 后产生对于这个例子的回答.一个经典例子是求 两个 自然数 的 最大公因子 的Euelid算法. 算法的概念必须形式化 才能 证明某个问题是不可判定的.一个问题的不可判定性是指算法原则上不可能存在,—不仅仅是至今还不知道这样的算法. 在这些形式化中最普通的是1物由犯机(T以角glna- chjne).然而,应该强调, 所有 提出的形式化 发现 都是 等价 的,此外, 不可判定问题 的存在性是不 依赖 所用的形式化.下面将简要阐述这一点. 这样,必须 说明 算法这个直观概念的任何形式化如何导致算法不可判定问题.考虑任何一个这样的形式化.对任何算法A和A的任何输人字x,存在两种可能性:或者A对于x停止(llah),即当A 作用 于x时得出一个停止的计算;或者A对于x不停 止.在后一种情况下,就说A对于x 循环 (loop). 停机问题 (回t叱problelll)是对于任何对(A,x), 判定A对于义是停止还是循环. 停机问题的一个特例是可自应用性问题(seif一app- licability problem), 定义 如下.每个算法A是由它的 Godel字(Gi记el word)g(A)所完全决定的.例如, 抓A)可定义为A中所有指令按顺序的 集合 .一个算法A称为可自应用的(se】f一applicable),只有当 A对于夕(A)停止.自应用问题是判定任一算法是否可自应用的.自应用问题是停机问题的子问题;因此,如果前者是不可判定的,则后者也是不可判定的. 假设 存在一个自应用问题的算法A。.这样,对所有形为g(A)的输人,A。都停机,且根据A是否可自应用产生回答yes或no.现在修改A。,加上一个由 yes回答开始的一个非停机的计算.这样,修改过的算法AI,对于形为g(A)的输人循环(或停机),其中A是(不是)可自应用的.由 对角线 化 (diagonal止mg),对A、考虑输人g(A,),得到一个矛 盾.这 蕴涵 了自应用问题是不可判定的.因此,停机问题也是不可判定的. 算法不可判定性的证明或者是直接的(direct). 或者是间接的(indire以).一个直接证明,如上所述,通常用某种 形式 的对角线法.一个问题尸的不可判定性的间接证明是将尸归约到一个其不可判定性已知的问题pl.将解尸的算法 转化 为解尸、的算法. 不可判定性问题中这样有用的参照点尸l是Hilbert 第十问题(Hilbert tenth Problem)和POst 对应 问题 (POst corresPondellce Problern). 可判定性对于由一个问题到它的子问题的 变换 是保持的.类似地,不可判定性对于问题的 扩张 是 保持 的.知道可判定性和不可判定性之间的边界线是 至关重要的.非常难以精确地确定 边界 ,但可粗略地确定其边界.例如,考虑一由有限多个 定义方程 定义的群和 半群 的字问题,也考虑单向字问题(朋记irec- tional word problem),即 定义关系 只允许 关系 的右边代换左边,反之则不行.如果也考虑可 交换性 ,则产生八个问题:群对半群,一般的对 交换 的, 方程 对单向关系.群的字问题是不可判定的,因此,三个更广泛的问题也是不可判定的.交换半群的单向字问题是可判定的,因此三个上述子问题也是可判定的.这样,在这里,可判定性和不可判定性的边界是已知的. 对于讨沦一个形式系统中的不可判定 命题 ,见不可解性(unsolva城ty);G6dd 不完全性定理 (以泪el incolllpleteness theo~).K .C池del证明了不可判定 命题的存在性不是任何个别形式系统的 缺陷 ,而是所有形式系统的内在性质.这样的内在的不可判定命题是表示一给定形式系统的 相容性 的形式命题.后来人们发现(例如,G.Chaitin!AI」,【A2」的工作)不可判定命题不是少有的,而是非常多的,它们通常非常简单,有些属于最初等的 算术 .不可判定命题不再错认为是“实际数学”中不会遇到的奇异性. 如Chaltin所述:非线性 动力学 和 量子力学 已证明 随机 存在于 自然 中,我相信:我已经证明了 随机性 在纯数学中也存在,事实上,甚至存在于 数论 的最初等的分支中. 不能忽视不可判定命题,它们不是例外的和病态的,而是大量的,可接近的,并且可感知的.对任何形式系统,存在有真正的算术命题,它的 真假值 不可能在该 系统 内证明,尽管看起来这个命题肯定或者为真或者为假.例如:关于一个给定Diopllalltus方程可解性的命题.可以构造一个带 参数 k的具有多个变元的 Diophantus方程 序列 .包含在对应于参数k 的有限多个值的方程解中的 信息 ,通常不可用于解决其他情况.数学形式 推理 无力将不同情况联系起来.这样,这个特别平常的参数化DiophantuS方程超越了任何形式系统所能达到的地步.解决不同情况的方法 本质 上不会好于直接将所要得到的结果放在 公理 中! |
可判定性和复杂性
首先,我们所有的计算机的理论模型可以抽象成图灵机(Turing Machine)的形式,即图灵机的计算能力就能够代表实际计算机的计算能力了,然后我们就可以使用图灵机来研究可判定性和复杂性的问题。
可判定性(Decidable)的问题可以说是计算理论中最具哲学意义的定理之一。计算机看上去是如此的强大,以至于使得人们相信所有的问题最终都将屈服于它们。但是,不幸的是,这个世界上存在着很多计算机不能解决的问题,即计算机不可判定(Undecidable)。在逻辑里面,如果某个推理是不可判定的,即表明对它的判断过程是不能停机的,该推理过程将一直运行下去,永远都不会停止。
如果某个问题是可判定的,那么对该问题的计算的分析就进入了复杂性分析的领域,一个比可判定性更为复杂的领域。复杂性分析的原因在于问题的求解需要计算资源(时间和存储量),某些问题即使是可解的(可判定的),但是也许由于其需要过多的计算资源而变得不可解(在实际的情况中无法应用,比如说需要一亿年的时间)。根据计算资源的不同,我们把复杂度分为时间复杂性和空间复杂性两种。
在时间复杂性中,根据计算时间增长速率的不同,将其分为两大类,P问题和NP问题。P问题是单带图灵机在多项式时间内可判定的语言类。NP问题的准确定义是具有多项式时间验证的语言类,从判定的角度说,它是非确定性图灵机在多项式时间内判定的语言类,求解NP问题的最好方法是确定性的使用指数级的时间(EXPTIME)。他们之间的关系如:P属于NP属于EXPTIME。这里要提及的几个相关的问题,第一,存在着一个CoNP的语言类,它表示NP中的补语言,即不可在多项式时间内验证的语言类;第二,如果一个算法是多项式时间内可解的,那么可以说该算法是“快速”可解的,也就是说,在实际应用中,我们需要时间复杂度不超过多项式时间可解的算法;第三,在NP问题内,存在着一类非常重要的问题,叫做NP完全的(NP-complete),这类问题是相互联系在一起(使用多项式时间的算法可以相互转化)的,即如果某一个问题解决了,该类问题就解决了。NP完全问题是最难解的一类问题。
对照着时间复杂性,空间复杂性可分为PSPACE和NPSPACE问题。PSPACE是在确定型图灵机上,在多项式空间可判定的语言。NPSPACE问题是在非确定性图灵机上,在多项式空间可判定的语言。由于空间的可重用性(与时间的最大的不同点),并根据萨维奇定理,可知PSPACE问题和NPSPACE问题是相等的。
下面来看看空间复杂性和时间复杂性之间的关系,根据图灵机模型,可以知道每个计算至多能访问一个新的单元,也就是说在多项式时间内可解得问题最多只能消耗多项式的空间,即P问题属于PSPACE问题,NP问题属于NPSPACE的问题。总结起来,得到下面的关系,P属于NP属于PSPACE等于NPSPACE属于EXPTIME
虽然在上文中,提到了算法最好是在多项式时间内可解的,但是在实际的情况中,存在着大量的NP的有价值的问题。对于这些问题,一般的处理方法有两种思路,如果它不是NP-complete问题,或许可以找到解决该问题的关键点,从而将NP问题转化成P问题;第二种方法是,采取近似的方法,牺牲部分的准确度来换取效率的提高。
想想描述逻辑中的推理问题,虽然现在OWL-DL中,推理问题被证明是指数级的,但是还是能在实际情况中应用。究其原因,我猜想主要是大部分的应用情况下,计算规模不会很大,并不会花费多少时间。现实的问题是复杂的,并不仅仅由复杂性的分析就可以断定的。关于逻辑推理的复杂性,是我关心的问题,等下次好好研究后再写心得。
哥德尔不可判定性定理。人类任何一种语言都无法完全表述客观世界的所有真理,所以势必存在着一些命题在任何依附于某语言的逻辑体系下是无法判别正误的。哥德尔的研究彻底的击碎了希尔伯特关于任何数学体系公理化的希望,是20世纪最重要的数学定理。
把初等数论形式化之后,在这个形式的演绎系统中也总可以找出一个合理的命题来,在该系统中既无法证明它为真,也无法证明它为假。
列举所有计算机学的不可判定问题,越多越好,每个问题最少简略说明一下
问题补充:如:图灵机停机问题,文法的二义性问题的不可判定性,病毒在理论上就是不可判定的
P/NP/NP-Complete/NP-Hard。
1,计算复杂性
这是描述一种算法需要多少“时间”的度量。(也有空间复杂性,但因为它们能相互转换,所以通常我们就说时间复杂性。对于大小为 n 的输入,我们用含 n 的简化式子来表达。(所谓简化式子,就是忽略系数、常数,仅保留最“大”的那部分)
比如找出 n 个数中最大的一个,很简单,就是把第一个数和第二个比,其中大的那个再和第三个比,依次类推,总共要比 n-1 次,我们记作 O(n) (对于 n 可以是很大很大的情况下,-1可以忽略不计了)。
再比如从小到大排好的 n 个数,从中找出等于 x 的那个。一种方法是按着顺序从头到尾一个个找,最好情况是第一个就是 x,最坏情况是比较了 n 次直最后一个,因此最坏情况下的计算复杂度也是 O(n)。还有一种方法:先取中间那个数和 x 比较,如偏大则在前一半数中找,如偏小则在后一半数中找,每次都是取中间的那个数进行比较,则最坏情况是 lg(n)/lg2。忽略系数lg2,算法复杂度是O(lgn)。
2,计算复杂性的排序:
根据含 n 的表达式随 n 增大的增长速度,可以将它们排序:1 < lg(n) < n < nlg(n) < n^2 < … < n^k (k是常数)< … < 2^n。最后这个 2 的 n 次方就是级数增长了,读过棋盘上放麦粒故事的人都知道这个增长速度有多快。而之前的那些都是 n 的多项式时间的复杂度。为什么我们在这里忽略所有的系数、常数,例如 2*n^3+9*n^2 可以被简化为 n^3?用集合什么的都能解释,我忘了精确的说法了。如果你还记得微积分的话就想像一下对 (2*n^3+9*n^2)/(n^3) 求导,结果是0,没区别,对不?
2,P 问题:对一个问题,凡是能找到计算复杂度可以表示为多项式的确定算法,这个问题就属于 P (polynomial) 问题。
3,NP 问题:
NP 中的 N 是指非确定的(non-deterministic)算法,这是这样一种算法:(1)猜一个答案。(2)验证这个答案是否正确。(3)只要存在某次验证,答案是正确的,则该算法得解。
NP (non-deterministic polynomial)问题就是指,用这样的非确定的算法,验证步骤(2)有多项式时间的计算复杂度的算法。
4,问题的归约:
这……我该用什么术语来解释呢?集合?太难说清了……如果你还记得函数的映射的话就比较容易想象了。
大致就是这样:找从问题1的所有输入到问题2的所有输入的对应,如果相应的,也能有问题2的所有输出到问题1的所有输出的对应,则若我们找到了问题2的解法,就能通过输入、输出的对应关系,得到问题1的解法。由此我们说问题1可归约到问题2。
5,NP-Hard:
有这样一种问题,所有 NP 问题都可以归约到这种问题,我们称之为 NP-hard 问题。
6,NP完全问题 (NP-Complete):
如果一个问题既是 NP 问题又是 NP-Hard 问题,则它是 NP-Complete 问题。可满足性问题就是一个 NP 完全问题,此外著名的给图染色、哈密尔顿环、背包、货郎问题都是 NP 完全问题。
从直觉上说,P<=NP<=NP-Complete<=NP-Hard,问题的难度递增。但目前只能证明 P 属于 NP,究竟 P=NP 还是 P 真包含于 NP 还未知。
P问题:可以通过确定性图灵机在多项式时间内求解。
NP问题:可以通过非确定性图灵机在多项式时间内求解。
或者说,可以在多项式时间内验证一个解。
NP问题的例子,Hamilton回路(在图中找一条环路,它经过且只经过一次每一个点)。
非NP问题,无法在多项式时间内验证解。例子:问一个图是否不存在Hamilton回路。(除非穷举所有可能,否则无法验证)
NPC问题的定义:它满足如下两个条件:
1.是NP问题。
2.所有的NP问题都能规约为它。
俗语就是,到现在还找不到多项式时间解法的NP问题,只能用指数级甚至阶乘级的复杂度的搜索。
因为所有的NP问题都能规约为NPC问题,如果一个NPC问题存在多项式时间的解法,那么会得出P=NP=NPC,所以,目前人们不相信NPC问题存在多项式时间的解法。
NPC问题的例子:逻辑电路问题。给定一个逻辑电路(比如输入接上若干与非门),是否存在一个输入使其输出为True?
NP-Hard问题:所有的NP问题都能规约到它,但它不一定是NP问题。
可满足式
satisfiable(可满足式)
在逻辑领域中,塔尔斯基最重要的贡献是在形式语言的语义研究方面,他是数理逻辑模型论分支的开创者之一。30年代初期,塔尔斯基提出并应用了语义学方法。这种方法的本质在于研究表达式与它们所指称的对象之间的关系。他应用该方法的目的在于建立一给定语言的真语句的定义。对于模型和某些有关的语义概念,早在塔尔斯基之前就已是数学家和逻辑学家所熟悉的。但是他首次给出了这些概念的精确的集合论描述,并使之成为许多元数学研究的有力工具。他在这个领域中的最重要的结果是关于真语句集不可定义性定理,即在很一般的假定下,在一模型M中真的语句集是在M中不可定义的。在判定问题的研究中,塔尔斯基的工作也有重要的结果。他证明了实数域的一阶理论是可判定的,在不可判定性方面,他的进一步工作是建立许多很弱的但数学上有意义的理论的不可判定性。为此,他引入本质不可判定的概念,认为一个理论如果它的所有协调扩张是不可判定的,该理论就是本质不可判定的。他还应用本质不可判定概念证明了有关不可判定性理论的定理,并在此基础上,获得许多有关不可判定性的结果。塔尔斯基的工作还包括在集合论、带无穷长公式的逻辑、弱二阶逻辑、直觉主义逻辑和模态逻辑等方面的建树。在逻辑教育方面,他培养了一批知名的逻辑学家。
在哲学方面,塔尔斯基没有发表专门的著作,可注意的是他对集合论中的假定的态度。他象大多数数学家一样简单地承认它们是真的,并系统地使用无穷性的集合论概念。这对他的逻辑和元数学研究有深刻的影响。自由地使用集合论构成他的语义学方法的发展基础。他的这种方法论态度与D.希尔伯特对于元数学的有穷主义和L.E.J.布劳维尔的直觉主义态度明显不同。
可满足性问题(satisfiability problem,简称SAT),是指合取范式的可满足性问题,简单可以叙述为:对于一个合适公式,通常我们假定已经转化为CNF的形式,即一个合取范式,那么是否有一个算法能在多项式的时间内找到该公式的一个赋值,使的其真值为真吗?
逻辑公式的可满足性判定是计算机和人工智能领域内的一个重要的问题,解决SAT问题对解决数学、计算机科学、电子工程技术中的一些实际问题都有非常重要的意义。对于可满足性SAT问题,已经被证明是一个NPC问题,并且是第一个被证明是NPC问题,详见文献[1]。
命题原子 表示命题的符号,用小写字母表示。
对于一个子句集S,如果存在一个赋值,使得S中的每个子句在该赋值下的真值为真,那么称S是可满足的,并且称赋值为S的一个模。例如:
可满足子句集的充要条件
约束满足问题
CSP-Constraint Satisfaction Problem 约束满足问题(CSP-Constraint Satisfaction Problem)是人工智能研究领域的一个重要分支,现实生活中的很多问题,都可以用约束满足问题来建模,如视觉(Vision),调度中的资源分配(Resource allocation),时序推理(Temporal reasoning)等.约束满足问题通常都是NP-hard问题,在其众多求解算法中,基于回溯的搜索算法(BT-backtracking algorithm)是一个完备的核心算法.该算法在选择实例化变量时,采用深度优先策略,若相容性检查失败则启动回溯机制,并通过引入展望(look-ahead)和回顾(look-back)两种模式,显著地提高了搜索效率[1].基于冲突的向后跳转[2]和动态的回溯算法[3]等是回顾模式类的搜索算法;基于相容性技术的算法是展望模式类的搜索算法.而弧相容(AC-arc consistency)则是众多相容性算法中一个高效的相容性技术[4],如算法AC3[5],AC4[6],AC2001[7]等.由于弧相容维护(MAC-maintaining arc consistency)具有高效的求解效率和低额空间代价的特点,所以MAC是目前求解约束满足问题的一个主流搜索技术.
逻辑公式的可满足性判定–方法 工具及应用
丛
书: 博士丛书
作
者: 张健
编
号: 5577
书
号: 9787030083647
出
版
社: 科学出版社
出版日期: 2000-10-22
定
价: 18.0 元
逻辑公式的可满足性问题是计算机科学和人工智能中的著名问题.本书前三章主要介绍经典的命题逻辑和一阶谓词逻辑公式以及模态逻辑公式的可满足性判定算法,也介绍了有关的软件工具.第四章则介绍它们在离散数学研究、软件和硬件的形式验证与测试等方面的应用. 本书可供从事计算机科学和人工智能研究的有关人员阅读,也可供高等院校计算机专业的本科生和研究生参考.