情景演算公理化简介.doc

我们说情景演算是一个关于变化推理的逻辑语言。更精确的说是一个一阶语言,有时会用一些二阶特征来充实。通过把情景和动作表示为可以量化的一节对象,我们就可以用一阶逻辑语言来描述情景演算问题了。arthy和Hayes把关系流表示为最后的参数为情景术语的谓词。例如在情景s时积木x在桌子可以用二元谓词ontable(x,s)表示。arthy谋求具体化关系流为一阶对象,导入一个特殊的二元谓词“Holds(p,s)”来表示在情景s时关系流p为真。这样象ontable(x,s)的形式可以看做是Holds(ontable(x),s)的缩写。现在假定下列与特定域独立的谓词和函数:Holds(p,s)—在情景s时流p为真;do(a,s)—在情景s时执行动作a产生的新情景;Poss(a,s)—在情景s时动作a可以执行。当然我们也可以导入其他特殊谓词和函数。例如,Do(P,s1,s2)的三元谓词,意为s2是在s1情景下执行程序P的结束情景。对流的因果关系我们可以使用三元谓词Caused(p,v,s),意为在情景s时流p变成真值v。这里关系流由不带情景参数的函数表示,函数流由最后的参数为情景的函数表示。例如clear(x)是一元关系流。通常写的clear(x,s)是Holds(clear(x),s)的缩写。color(x,s)是二元函数流可以如下写出他的公理:color(x,do(paint(x,c),s))=c。现在我们可以用一阶逻辑来公理化上里的积木域(假定所有的自由变量为全局变量):Poss(stack(x,y),s)≡holding(x,s)∧clear(y,s),Poss(unstack(x,y),s)≡on(x,y,s)∧clear(x,s)∧handempty(s),Poss(pickup(x),s)≡ontable(x,s)∧clear(x,s)∧handempty(s),Poss(putdown(x),s)≡holding(x,s),holding(u,do(stack(x,y),s))≡holding(u,s)∧u≠x,handempty(do(stack(x,y),s)),on(u,v,do(stack(x,y),s))≡(u=x∧v=y)∨on(u,v,s),clear(u,do(stack(x,y),s))≡u=x∨(clear(u,s)∧u=y),ontable(u,do(stack(x,y),s))≡ontable(u,s),holding(u,do(unstack(x,y),s))≡u=x,¬handempty(do(unstack(x,y),s)),on(u,v,do(unstack(x,y),s))≡on(u,v,s)∧¬(x=u∧y=v),clear(u,do(unstack(x,y),s))≡u=y∨(clear(u,s)∧u=x),ontable(u,do(unstack(x,y),s))≡ontable(u,s),holding(u,do(pickup(x),s))≡u=x,¬handempty(do(pickup(x),s)),on(u,v,do(pickup(x),s))≡on(u,v,s),clear(u,do(pickup(x),s))≡clear(u,s)∧u=x,ontable(u,do(pickup(x),s))≡onta