问题:前束中( )存在量词的前束范式称为斯柯伦范式。
A.不含 B.含有
下面学习消解原理
前面讲的搜索技术针对的是状态空间知识表示方法,也就是说如果将问题形式化为状态空间图,那么可以用搜索技术求解问题,求解问题的过程转化成在状态空间图中寻找从初始状态到目标状态的路径问题。生活中有一些问题不能转化成状态空间图的形式,而转化成谓词逻辑比较方便,例如储蓄问题:
前提:每个储蓄钱的人都获得利息。
结论:如果没有利息,那么就没有人去储蓄钱。
类似这样的问题可以应用谓词逻辑的知识表示方法对问题进行是形式化表示,然后应用消解原理进行推理。
消解原理(resolution principle),也叫做归结原理。消解是一种可用于一定的子句公式的重要推理规则。当消解可使用时,消解过程被应用于母体子句对,以便产生一个导出子句。例如,如果存在某个公理E1∨E2和另一公理~E2∨E3,那么E1∨E3在逻辑上成立。这就是消解,而称E1∧E3为E1∨E2和~E2∨E3的消解式(resolvent)。
1.自由变元与约束变元
设α,β是一个谓词公式,将量词记作θ(即或)。如果α中包含部分公式(θx)β,则β中变元x的一切出现都称为x在α中的约束出现,相应地称x为约束变元(哑元、约束变量)。α中不在任何量词作用域内的变元x,称为变元x在α中的自由出现,相应地称x为自由变元(自由变量)。
说明:量词的作用域(辖域)是直接跟在它后面的公式。如果有括号,则是括号里的公式。如果没有括号,则是最短的完整公式。如:
x(P(x)=>y(R(x,y)))
x,y都是约束变元
x(P(x)=>(R(x,y)))
x是约束变量,y是自由变元
改名:将谓词公式中一个变元名改成另一个变元名,但是要求改名后的公式与原公式意义相同(真假值相同)。
原则:改成的新的变元名一定是量词作用域中没有出现过的变元名(包括约束变元和自由变元)。
例如:
x(P(x)=>(R(x,y)))
除了y外,可以将x改成任何变元名
xP(x)∧Q(y)
可以改成任何变元名,包括y(建议不要用y)
2.前束范式与前束合取范式
设谓词公式α具有形式:α=(θ1x1)…(θnxn)
其中:θi(i=1,…,n)是或,M是不包含量词的谓词公式,则称α是前束范式。称(θ1x1)…(θnxn)为前束,称M为母式。
设谓词公式α是一个前束范式,如果α的母式具有形式:
M11∨M12∨…∨M1n∧
M21∨M22∨…∨M2n∧
…
Mm1∨Mm2∨…∨Mmn
其中,Mij是原子公式或其非,则称α是前束合取范式。相应地有前束析取范式。
例如,将前束析取范式:
(x)(y)(z)((~P(x)∧~Q(y))∨R(z))
变成前束合取范式(应用交换律、分配律):
(x)(y)(z)((R(z)∨~P(x))∧(R(z)∨~Q(y)))
3.斯科伦(Skolem)范式
定义:前束中不含存在量词的前束范式称为斯柯伦范式。
问题:前束中( )存在量词的前束范式称为斯柯伦范式。
A.不含 B.含有
前束范式化成斯柯伦的步骤是:
①xk(1≤k≤n)左边没有全称量词,则取不在母式中出现的常量替代母式中的所有xk,并删除前束中的xk
②若xk(1≤k≤n)左边有全称量词(xs1)(xs2)…(xsr)(1≤r,1<s1<s2<…<sr<k)
则,取不在母式中出现的r阶函数fr(xs1,xs2,…,xsr)替代母式中的所有xk,并删除前束中的xk。
③反复使用上述两条规则,消除前束中的所有存在量词,即得到斯柯伦范式。
其中,引入的函数称为斯柯伦函数。需要说明的是一个谓词公式的斯科伦范式不是唯一的,尽可能将斯科伦函数取得简单一点。
正常的做法是先将公式化成前束范式,然后再化成前束合取范式最后再化成斯科伦范式。这样引入的斯科伦函数的变元较多。