1. 引言
人类思维中严格的推理主要是两种,一种是使用真值表,一种是使用演绎规则。真值表方法,有两个特点,其一,是机械性;其二是,每一个要素,都需要用固定的对象表达出来,假设用n表示推理中一个命题中含有对象的数目,当n大到一定程度的时候,2n会是一个极其庞大的数目,这就限制了它在机器推理当中的应用。
思维中还可以使用演绎推理规则来进行推理,如常用的分离规则1,下面两个是利用分离规则的具体例子:
1、如果得了肺炎,那么就会发烧;某人得了肺炎,他一定会发烧。
2、如果得了肺炎,那么,就会出去旅游;某人得了肺炎,所以他会出去旅游。
1是正确的推理,2是错误的推理,这依赖于人类的经验。让机器从知识库中,学会人类的整体经验,显然存在很大的难度,即使一个库中包含着人类绝大多数经验,检索耗时也限制了其应用。因此这种方法也不适用于机器推理。
归结和合一算法的出现,为解决机器的自动推理提供了很好的方法并得到广泛应用,这一点早已为相关的研究者熟悉。但从事逻辑学研究的人员,往往限于依据罗素和怀特海在《数学原理》中构建的推理体系,不了解机器自动推理的进展。这在人工智能兴起的今天,显然是不满足时代要求的。更多的非专业人士其实也有一窥机器推理的需求,实际工作中,越来越需要构架起《数学原理》中的为人熟知的推理体系与人工智能中自动推理之间的桥梁,让更多的非人工智能领域的研究人员深入认识与了解该方法,这也是本文的主要目的。
1963年,J. Alan Robinson找到了在机器上实现逻辑推理的简单方法:著名的归结与合一(resolution and unification)算法 [1] 。归结原理实质上是一条简洁的推理规则。使用这一条规则,对一阶逻辑中的任一个恒真公式,都将是可证的。到了1972年,以L. Wos为代表建立了一个以归结方法为主的自动推理系统。这个系统对于解有限数学、线路设计、程序正确性验证及形式逻辑等领域中的疑难问题,提供了帮助。1997年,Leitsch,Alexander又在The Resolution Calculus中给出了总结。至此,该方法得以广泛应用。
2. 命题逻辑中的归结算法:
令p,q,r,s…表达命题逻辑中的任意一个原子命题,通过命题逻辑的五个连接词
,
,
,
,
形成合式公式。令A,B,C为任一合式公式,利用以下规则:
(1) 等值式:
(2) 蕴析律:
(3) 德·摩根律:
(4) 双重否定:
(5) 分配律:
可将任意一个合式公式改写为合取范式(CNF)或者析取范式(DNF),其中的合取范式就是以下进行归结运算的基础。设已有CNF:
2,归结的步骤如下:
1、将合取范式中的每个简单析取用集合表达,整个合取范式为集合的集合:
。
2、在不同的集合中寻找同一个命题字母及其否定,即
与
这样的互补对。如上面第一个集合里的p和第二个集合里的
就是互补对。
3、由两个集合减去互补对得到的并集,组成新的集合就是进行归结,集合
,和集合
归结为
。
4、归结持续到不能归结或出现空集为止 [2] ,继续将
和
归结得到
。
由此可见,归结算法处理命题逻辑推理,简单明了,尤其适合于计算机编程执行,这一方法使得人类第一次在机器上实现了复杂的逻辑推理。付出的代价也是巨大的,一个简单的推理,需要经过繁琐的步骤,因为得到范式本身就需要许多步骤;稍复杂的推理其步骤是非常庞杂的。
3. 一阶谓词逻辑中的归结算法
归结算法同样适用于谓词演算。但有两个难点,第一是谓词逻辑中多出来量词、谓词和个体词,增加了问题的复杂性;第二是Skolem函数引入,进一步提高了处理推理的难度。
我们先看一阶谓词演算公式要得到范式新增加的规则:
(6) 符号移至量词的辖域之内:
(7) 如果两个量词的约束变量名相同,则对其中一个变量改名,使得每个量词约束唯一变量。如可将
改为
。
(8) 量词前置形成前束范式,依据以下规则:若x在公式A中不出现,则
末尾四个公式对析取也成立,这里不再列出。应用以上的(1)~(8)规则,可以求出任一一阶谓词逻辑公式的合取范式。例如,“小王所有的朋友都不喜欢快餐”用公式表达为:
注意,为了理解方便和与prolog语言统一,采用英语单词表达谓词。其范式为:
由于全称量词约束整个公式的所有变量,在一定的个体域内,依据一阶谓词逻辑的全称销去规则,可进一步得到:
这使我们得到了规则:
(9) 位于公式左端的全称量词全部可以销去。
如果公式中包含存在量词,在进行归结算法时需要进行Skolem化,以达到销去存在量词的目的。分为两种情况:第一,当个体域中有k个个体时
定义为:
当
为真时,
中至少有一个
使得
为真,此时用一个公式中未出现的新个体常量c,得到F(c)可方便的替代了
,达到销去存在量词的目的。第二,考虑如下谓词公式:
对于所有x都存在一个y,使得x和y具有F关系,如“每个人都读一些书籍”:
这时,存在量词不可为个体常量c替代,不论c指的是那些书,一旦用c替代,就意味着每个人都读同样的书籍。解决的办法是定义Skolem函数f,来代替被存在量词约束的变量y,函数f将每个x映射到他读的书籍:
x是变量,能将每个x映射到它所对应的书籍。这样就用函数f将存在量词销去得到:
Skolem化的应用,形成了归结算法的新规则:
(10) 若谓词公式中有存在量词,对他进行Skolem化。
把(1)~(10)条规则,综合应用于句子“每个人都读一些书”:
这是规范的,机器能识别的谓词逻辑公式。到此,仍然没有实现机器对谓词逻辑推理的处理,还要引进新的算法-合一。
4. 合一
合一是一个替换个体词的集合。具体的推理,涉及不止一个语句,往往是多个句子形成一个推理。这些句子中可能有大量的个体常项和许多个体变量,如果不进行一定的替换,或者随机替换,就会使得计算数量庞大到不能付之于实际应用。
首先是匹配文字。在范式中的两个不同的简单析取或简单合取中的两个文字相匹配,而且其中一个是另外一个的否定(又称互补),则该文字可以归结。具体的匹配条件是:
1、n元谓词的名称和元:谓词名称完全一样,“book”和“books”是两个不同的谓词。谓词的元也必须一样,book(x, y)和book(x, y, z)一个是二元谓词,一个是三元谓词。
2、两个常量的匹配:两个常量的每个字符一一匹配时二者匹配。如mary只能与mary匹配,而与Mary不匹配。
3、常量c与变量x的匹配:如果x没有赋值,则二者匹配;如果x已经赋值,则当且仅当x的赋值与c匹配时c与x才匹配。
4、未赋值的两个变量x,y总是匹配的,赋值后要看结果,可能匹配,也可能不匹配。
举例如下:mother(x, y)与mothers(z, u)不匹配,谓词不同;up(x, y)与up(x, y, z)不匹配,前者是二元谓词,后者是三元谓词;brother(x, y)与brother(john, w)匹配,实际上是使用赋值x/john,y/w;brother(x/robert, y)与brother(john, z)不匹配,x已经赋值给robert,它与john是两个不同的个体常项。
其次,匹配和给变量赋值的过程,就是在进行合一运算。如上例子中brother(x, y)与brother(john, w)匹配,得到的集合{x/john, y/w}就称作合一。
通过一个具体例子,能很好说明机器在一阶谓词逻辑中的自动推理。
小王所有的朋友都不喜欢快餐。
每个不喜欢快餐的人都不吃方便面。
小星是小王的朋友。
小星喜欢方便面吗?
符号化为谓词公式:
将以上三个句子先求范式再化为机器识别的标准公式:
用集合形式表达得到的公式:
1、
2、
3、
4、
根据匹配规则,寻找互补的文字对,得到:
5、
(1,4归结,x/xing)
6、
(2,4归结)
7、
(3,5归结)
8、
(6,7归结)
这显然是正确的结论,“小星不吃方便面”。至此,通过繁琐的步骤,Robinson实现了准确的自动推理,使命题逻辑公式和一阶谓词逻辑公式的推理自动的在机器上运行,Robinson的贡献在人工智能发展中其地位如何高估都不为过。
5. 代码实现
最终目的是用机器代替人工,实现全自动化证明。而这是容易做到的:
#ifndef SUBSENTENCE_H
#define SUBSENTENCE_H
#include
#include
#include
#include
#include
#include
namespace FormulaNamepace {
// 公式符号定义
const char EQ = '#'; // 存在量词符号
const char UQ = '@'; // 全称量词符号
const char IMPLICATION = '>'; // 蕴含符号
const char NEGATION = '~'; // 否定符号
const char CONJUNCTION = '&'; // 合取符号
const char DISJUNCTION = '|'; // 析取符号
const char CONSTANT_ALPHA[] = { 'a', 'b', 'c', 'd', 'e',
'i', 'j', 'k'};
typedef std::string Formula;
typedef std::string Subsentence;
typedef std::set
SubsentenceSet;
bool IsConstantAlpha(char ch);
// 移除最外层的括号对
Formula& RemoveOuterBracket(Formula& f);
// 前向扫描,查找匹配的一对组件,并且返回后者所在位置
template
FwdIter FindPairChar(FwdIter first, FwdIter last,
Compo former, Compo latter)
{
std::size_t pairCnt = 0;
while(1) {
if(first == last) return last;
if(*first == former)
++pairCnt;
else if(*first == latter)
if(--pairCnt == 0)
break;
++first;
}
return first;
}
// 查找谓词符号
template
inline FwdIter FindPredicate(FwdIter first, FwdIter last)
{
return std::find_if(first, last,
std::ptr_fun
(islower));
}
// 查找公式符号
template
inline FwdIter FindFormula(FwdIter first, FwdIter last)
{
return std::find_if(first, last,
std::ptr_fun
(isupper));
}
// 查找量词符号
template
inline FwdIter FindQuantifier(FwdIter first, FwdIter last)
{
return std::find_if(first, last,
[] (const typename FwdIter::value_type& lhs)
{ return lhs == EQ || lhs == UQ; }
);
}
template
char FindNewLowerAlpha(const Set& s)
{
const size_t alphaCnt = 26;
std::default_random_engine e;
for(size_t i = 0; i < alphaCnt; ++i) {
char ch = 'a' + e() % alphaCnt;
if(s.find(ch) == s.end())
return ch;
}
throw std::logic_error(no more new alpha can use);
}
inline bool IsConnector(char ch)
{
return ch == CONJUNCTION || ch == DISJUNCTION;
}
Formula& ReplaceAlphaWithString(Formula& target,
char alpha, const Formula& str);
// 获取谓词串
Subsentence GetPredicate(
typename Subsentence::const_iterator first,
typename Subsentence::const_iterator last);
// 获取公式串
Subsentence GetFormula(
typename Subsentence::const_iterator first,
typename Subsentence::const_iterator last);
// 消去蕴含连接词
Formula& RemoveImplication(Formula& f);
// 将否定符号移到紧靠谓词的位置
Formula& MoveNegation(Formula& f);
// 对变元标准化
Formula& StandardizeValues(Formula& f);
// 化为前束范式
Formula& TransformToPNF(Formula& f);
// 化为Skolem标准型
Formula& TransformToSkolem(Formula& f);
// 消去存在量词
Formula& RemoveEQ(Formula& f);
// 消去全称量词
Formula& RemoveUQ(Formula& f);
// 消去合取符号,获得子句集
void ExtractSubsentence(SubsentenceSet& subset,
const Formula& f);
}
#endif // SUBSENTENCE_H
对这一方法也有不同的质疑,根源于这一算法的繁琐,有人批评这种自动逻辑推理,认为人类在生活中从不这样机械和繁琐地思考。明显这种批评很无力,人类也从不高速旋转运动,但机器的高速旋转却极大提高了生产力。机器不一定跟人类思维方法一样,它用自己的方式达到了和人们一样的推理结果,这正是归结算法在人工智能发展中的真正意义所在。
NOTES
1分离规则是在给定前提A→B,A都为真时,得到结论B为真的规则。
2原来的公式为
[3] ,此处省去具体求范式的步骤。