毕业设计跟的导师是研究计算机理论的，花了三个月学习符号逻辑，试图优化一个回答集程序的求解器（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一定是丁的任意超集的结论。即，增加新知识并不影响以前的结论。而常识推理却与此不同，大多数情况下，由于信息不完全，知识不完备等原因，为了推出有用的结果，我们不得不做一些额外的假设，例如封闭世界假设8。更一般的，我们假设环境是正常的(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可以合理刻画常识推理。