毕业设计跟的导师是研究计算机理论的,花了三个月学习符号逻辑,试图优化一个回答集程序的求解器(Answer set solver)。比起眼花缭乱的前端框架和热闹的社区讨论,符号逻辑就是一个挺小众的数学领域。一讲到逻辑程序就会涉及一大堆的概念 ,伴随一大堆数理逻辑的符号,令有兴趣的新手望而却步。此篇博文能够说是导师的博士论文的一篇读后感,一篇回答集编程的发展史,一篇回答集程序入门简介。详见《提升ASP效率的若干途径及在服务机器人上的应用》。前端
1.人工智能学派程序员
一些传统人工智能的研究者认为,(人工)智能能够经过符号推理形式化刻画,这一派系的研究如今被归类为符号主义。此外,还有联结主义和行为主义。当下很火的机器学习就是属于联结主义,原理主要为神经网络及神经网络间的链接机制与学习算法。行为主义源于控制论,主要的应用是感知-动做型控制系统。比起另外两个兄弟,符号逻辑目前的工业应用还不多,是一座数学家在构筑的伊甸园。算法
2.回答集程序的背景数据库
“ASP研究来源于逻辑程序和非单调推理两个领域的交叉融合。最初,基于经典逻辑,逻辑程序定义了陈述性表达(declarative representation)的程序语言,并经过语法限制实现高效计算。以后,因为应用的须要引入否认知识的表达,并经过失败即否认原则进行推理。编程
Gelfond and Lifschitz(1 988)提出稳定模型语义(stable model semantics),首次利用非单调推理领域的成果成功解释失败即否认。前端框架
随着研究的深刻,稳定模型语义不断被扩展,发现了不少良好的性质,它不光能解释逻辑程序中失败即否认,还与非单调推理中不少工做有密切联系,从而被承认为一个实用的非单调推理工具和能够表达常识知识的知识表示语言。以后,愈来愈多的人开始关注这个方向,并称这个新领域为回答集编程(Answer Set Programming,ASP)。“网络
2.1 逻辑程序框架
“逻辑程序起源于七十年代自动定理证实和人工智能方面的工做,其主要思想能够用Kowalski(1979)提出的等式来解释:机器学习
Algorithm=Logic+Control。即,算法分为两部分,逻辑与控制。编程语言
其中逻辑部分用来讲明问题是什么(what),控制部分用来讲明如何求解问题(how)。而逻辑程序的最终目标就是,程序员只须要刻画出算法的逻辑部分,系统能够自动求解。逻辑程序领域已经有诸如PROLOG的不少实际成果和应用。“
这种用通用方法求解问题的想法很美好,但实现起来很是艰难,推广也一样是一个大问题。这个工做能够类比C++中的模板(template),为一个复杂度高的抽象问题实现一个高效的程序,而后调用这个程序去解决简单的问题。
目前,效率这一块已经有很高效的实现,反而应用方面,却不如预料中的普遍。成为流行的编程语言须要有不少条件,这个语言原本就不是面向一个广阔“市场”来设计的,天然难以作到流行。目前有中科大的服务机器人项目在应用这个语言,随着服务机器人的发展,逻辑程序的前景至少不算穷途末路。
2.2 逻辑程序中的否认
(传统)逻辑程序通常状况下只能推理出正文字形式的结论,但根据实际应用的须要,经过增长额外的规则,它也能够推出负文字形式的结论。这些额外规则中最主要的两个是:封闭世界假设(Closed World Assumption,CWA)和失败即否认(negation as failure,NAF)。
封闭世界假设来源于演绎数据库,因为数据库中有大量事实,为了更紧凑的表达,很天然的会假设,凡是没有说明为真的命题都默认为假。
例如,当数据库中不存在某个时刻的航班时,咱们会假设此刻没有此航班。严格的说,封闭世界假设对应推理规则:
若是一个常原子A不是一个逻辑程序的结论(属于其极小模型),则推出A的否认。注意,封闭世界假设是一个非单调推理规则,即,当加入新知识后,原先推出的结论可能再也不成立。同时,因为一阶逻辑是不可断定的,因此实际中封闭世界假设只能用在那些能够在有限时间内判断
出推不出的公式,由此引出失败即否认。
失败即否认对应推理规则:若是常原子A被判断出推不出,则推出not A。一样,失败即否认也是一个非单调推理规则。
2.3 非单调推理
经典逻辑(命题,一阶)是单调的(monotonic):若是语句A是语句集丁的逻辑结论,则A必定是丁的任意超集的结论。即,增长新知识并不影响之前的结论。
而常识推理却与此不一样,大多数状况下,因为信息不彻底,知识不完备等缘由,为了推出有用的结果,咱们不得不作一些额外的假设,例如封闭世界假设。
更通常的,咱们假设环境是正常的(normal),没有意外发生,并获得一般状况下结论。而当环境变化,增长新知识后,原来的假设可能再也不成立,即,发生意外,得知真实状况再也不是一般的,此时咱们只能调整之前的结论,甚至获得否认的结论。如下是一些常识推理的例子:
1.鸟(一般状况下)会飞,特威蒂(tweety)是鸟,因此,特威蒂会飞。
2.鸟会飞,特威蒂是鸟,但特威蒂不会飞,因此,特威蒂不会飞。
3.鸟会飞,企鹅不会飞,特威蒂是鸟,特威蒂是企鹅,因此,特威蒂不知是否会飞。
4.企鹅是鸟,鸟会飞,企鹅不会飞,特威蒂是鸟,特威蒂是企鹅,因此,特威蒂不会飞。
5.贵格会教徒(一般状况下)是和平主义者,共和党人(一般状况下)不是和平主义者,尼克松是贵格会教徒,因此,尼克松是和平主义者。
6.贵格会教徒是和平主义者,共和党人不是和平主义者,尼克松是贵格会教徒,尼克松是共和党人,因此,尼克松不知是不是和平主义者。
这些推理是研究常识推理一般都会列举或考虑到的例子,其中第4项称为企鹅原则(Penguin Principle),第6项称为尼克松菱形(Nixon Diamond)。它们能够用来测试一个逻辑是否合理的刻画常识推理。而上述推理充分说明了非单调推理的做用,即,ASP的其中一个良好性质。
2.4 一个简单的ASP例子
紧接上一章:鸟(通常)会飞,但企鹅是一种不会飞的鸟。当咱们知道名为tweety的个体的一些信息(它是小鸟,或进一步,它是企鹅)时,能够经过ASP推理它是否会飞:
此程序惟一的回答集为{penguin(tweety),bird(tweety),nfly(tweety)),即得出结论tweety不会飞。
若是从上面的程序中去掉事实penguin(tweety), 即只知道tweety是鸟,则新程序惟一的回答集为{bird(tweety),fly(tweety))。
即在只告诉tweety是鸟的状况,得出结论tweety会飞。该例子代表ASP能够合理刻画常识推理。