W3CHINA.ORG讨论区--请教Description Logics推理的问题！

姓名：(无权查看)
城市：(无权查看)
院校：(无权查看)

以下是引用zhaonix在2007-11-1 19:37:00的发言：
[quote]以下是引用wolfel在2007-11-1 10:32:00的发言：

跟表示方法没有关系，你可以认为 C是一个描述逻辑公式比如 A < B
[/quote]

那 ~(A<B) 是什么意思呢？在DL中。

描述逻辑的语法中当然不能有这种表达式，不过这种形式的公式的语义也是可以定义的，见文献：

Giorgos Flouris, Zhisheng Huang, Jeff Z. Pan, Dimitris Plexousakis, HolgerWache: "Inconsistencies, Negations and Changes in Ontologies", in Proc. of AAAI'06

在这篇文章中，negation有两种形式的语义：coherence negation 和consistency negation，相应的， ~(A\sqsubseteq B)可以定义为 \exists (A\sqcap \neg B)和 A\sqsubseteq \neg B

LZ确实使用符号不规范，并且其实LZ的“KB不可满足”也是不规范的说法，因为不可满足是针对某个concept说的，KB只有incoherence和inconsistency。

不过最主要的问题是我觉得LZ提的这个问题实际上是一个一阶逻辑的问题。

姓名：(无权查看)
城市：(无权查看)
院校：(无权查看)

我认为，如果K|=C的话（无论C是一个concpet还是axiom），这说明C是为universal concept的，
每个知识库K有自己的universal concept（它们是不同的），这样C并不是并不是tautology，而只是对K的所有model都成立而已。

这种认为每个知识库有自己不同的universal concept的说法不知对不对

第二个问题就是K|=C的表示方法问题，一般说来，DL知识库K只是有axiom做成的（TBox，RBox and ABox），C也一般只有A subclassOf B，D(a),等axiom的格式

但是在K中含有概念，和C是概念这种写法也应该是允许的。
在Tableaux算法里，A subclassOf B是转化成~A\/B的格式的，
这表明TBox可以完全转化成concept,K|=A subclassOf B 也可转化为 K|=~A\/B
至于为什么一直不这么写，也许是因为习惯或者难以理解等等问题。

望大家指点！

姓名：(无权查看)
城市：(无权查看)
院校：(无权查看)

以下是引用Leon.Essence在2007-11-1 21:36:00的发言：
我认为，如果K|=C的话（无论C是一个concpet还是axiom），这说明C是为universal concept的，
每个知识库K有自己的universal concept（它们是不同的），这样C并不是并不是tautology，而只是对K的所有model都成立而已。

这种认为每个知识库有自己不同的universal concept的说法不知对不对

第二个问题就是K|=C的表示方法问题，一般说来，DL知识库K只是有axiom做成的（TBox，RBox and ABox），C也一般只有A subclassOf B，D(a),等axiom的格式

望大家指点！

1. 我没有听说过这种说法，TOP就是一个全集概念，所有的concept都属于它。而且我觉得你定义每个KB的universal concept也没有什么意义啊

2. 我觉得可以，但是本身DL的语法对否定的使用有限制，因此没有~(A\sqsubseteq B)这种语法形式，LZ要想把DL做类似一阶逻辑那样的语法变化，必需要扩展DL的语法和语义，尤其是否定的语法和语义。

姓名：(无权查看)
城市：(无权查看)
院校：(无权查看)

以下是引用wolfel在2007-11-1 21:22:00的发言：

描述逻辑的语法中当然不能有这种表达式，不过这种形式的公式的语义也是可以定义的，见文献：

Giorgos Flouris, Zhisheng Huang, Jeff Z. Pan, Dimitris Plexousakis, HolgerWache: "Inconsistencies, Negations and Changes in Ontologies", in Proc. of AAAI'06

在这篇文章中，negation有两种形式的语义：coherence negation 和consistency negation，相应的， ~(A\sqsubseteq B)可以定义为 \exists (A\sqcap \neg B)和 A\sqsubseteq \neg B

LZ确实使用符号不规范，并且其实LZ的“KB不可满足”也是不规范的说法，因为不可满足是针对某个concept说的，KB只有incoherence和inconsistency。

不过最主要的问题是我觉得LZ提的这个问题实际上是一个一阶逻辑的问题。

赞楼上！相关文献说来就来。
    同意：楼主提的问题，是把DL和FOL混在一块了。虽然DL可以看作FOL的子集，但为了其用途定义了一套特定语法，不宜与FOL的混用。如果自己非要引入新的语法的话，得按照其风格定义好语义才行。
    用FOL的等价形式来看，DL中的 C<D 与 ~CVD  还是有区别的。DL中的C相当于是一个FOL一元谓词，而C<D则是一个命题（sentence,即不含自由变元的公式）： forAny.x.(C(x)->D(x)) ，等价于 forAny.x.(~C(x)VD(x)) 。后面这个式子与描述逻辑中的T<(~CVD)相当，而不是~CVD本身，因为后者是一个谓词而非公式。后者这种形式——谓词的组合——只在DL中有，而在通常的FOL中没有，倒也挺有意思。
    关于Tableaux算法中在判断 K|=(C<D) 问题时会搞出一个 ~CVD 来的问题。问题出在：算法不是把后者当作一个普通的概念那样对待的！   对于普通的概念C，DL系统会用Tableaux算法作用于C，以确定C是否可以满足；而这里，DL系统的任务是要把算法作用于~CVD的否定上去，想确定的是其否定式(即C^~D)是否可以满足。
    而虽然“C可满足”成立意味着“C不可满足不成立"、反之亦然，但  “C可满足” 与 “~C不可满足” 并不等价！——前一对命题中后者是前者的双重否定式，但后一对命题中后者不不是前者的双重否定式（把“可满足”看作一元谓词、把C看作个体常量即可。哇塞，二阶逻辑了！:)）。   确切地说：C不可满足意味着~C对（堪作当前KB的model的）任何解释都是可满足的；而C可满足时，~C也可能满足也可能不满足，即相当于啥也没说:) 。
    这一点其实完全不奇怪。再用FOL来描述：
    C不可满足 <-->  ~C恒满足   ：  ~exists.x.C(x) <--> forAny.x.~C(x)
    C可满足      -->  ~C ?          ：    exists.x.C(x)   -->         ?   ~C(x)
因此，判定C的可满足性与判定~C的可满足性对于能得到的关于C本身的结论，是完全不同的。
——感谢楼主及大家的讨论，才使我想了这么多、对这个问题才头一次感到这么清楚。

[此贴子已经被作者于2007-11-2 13:17:30编辑过]

姓名：(无权查看)
城市：(无权查看)
院校：(无权查看)

To: Leon.Essence&wolfel
：你们是对的，我的说法错了。tautology和validity在一阶逻辑中并不相等，前者是后者的真子集。所以“K|= C”说明C是valid而已。

至于楼主说的K |= C implies D,我的看法和zhaonix一样。理论上，DL Reasoner也有可能使用：TOP implies (not C or D)，也就是做为GCI去推理。但实现上一般都是采用的Lazy Unfolding一套，单方向使用unfolding rule。

PS. “C可满足” 与 “~C不可满足”在经典逻辑中就是不等价的。一个是SAT的定义，一个是validity的等价式。

PPS. 楼上最后的那段话：。。。“确切地说：C不可满足意味着~C对（堪作当前KB的model的）任何解释都是可满足的；而C不可满足时，~C也可能满足也可能不满足，即相当于啥也没说:) 。”
那个“不”字貌似多余的。。。

姓名：(无权查看)
城市：(无权查看)
院校：(无权查看)

以下是引用wjwenoch在2007-11-2 11:26:00的发言：
To: Leon.Essence&wolfel
：你们是对的，我的说法错了。tautology和validity在一阶逻辑中并不相等，前者是后者的真子集。所以“K|= C”说明C是valid而已。

PS. “C可满足” 与 “~C不可满足”在经典逻辑中就是不等价的。一个是SAT的定义，一个是validity的等价式。

~~~~~~~~~~~~~是

，现在改过来了。Tks！

姓名：(无权查看)
城市：(无权查看)
院校：(无权查看)

以下是引用zhaonix在2007-11-2 10:02:00的发言：
[quote]以下是引用wolfel在2007-11-1 21:22:00的发言：

描述逻辑的语法中当然不能有这种表达式，不过这种形式的公式的语义也是可以定义的，见文献：

Giorgos Flouris, Zhisheng Huang, Jeff Z. Pan, Dimitris Plexousakis, HolgerWache: "Inconsistencies, Negations and Changes in Ontologies", in Proc. of AAAI'06

在这篇文章中，negation有两种形式的语义：coherence negation 和consistency negation，相应的， ~(A\sqsubseteq B)可以定义为 \exists (A\sqcap \neg B)和 A\sqsubseteq \neg B

LZ确实使用符号不规范，并且其实LZ的“KB不可满足”也是不规范的说法，因为不可满足是针对某个concept说的，KB只有incoherence和inconsistency。

  不过最主要的问题是我觉得LZ提的这个问题实际上是一个一阶逻辑的问题。

[/quote]
赞楼上！相关文献说来就来。
     同意：楼主提的问题，是把DL和FOL混在一块了。虽然DL可以看作FOL的子集，但为了其用途定义了一套特定语法，不宜与FOL的混用。如果自己非要引入新的语法的话，得按照其风格定义好语义才行。
     用FOL的等价形式来看，DL中的 C<D 与 ~CVD  还是有区别的。DL中的C相当于是一个FOL一元谓词，而C<D则是一个命题（sentence,即不含自由变元的公式）： forAny.x.(C(x)->D(x)) ，等价于 forAny.x.(~C(x)VD(x)) 。后面这个式子与描述逻辑中的T<(~CVD)相当，而不是~CVD本身，因为后者是一个谓词而非公式。后者这种形式——谓词的组合——只在DL中有，而在通常的FOL中没有，倒也挺有意思。
     关于Tableaux算法中在判断 K|=(C<D) 问题时会搞出一个 ~CVD 来的问题。问题出在：算法不是把后者当作一个普通的概念那样对待的！   对于普通的概念C，DL系统会用Tableaux算法作用于C，以确定C是否可以满足；而这里，DL系统的任务是要把算法作用于~CVD的否定上去，想确定的是其否定式(即C^~D)是否可以满足。
     而虽然“C可满足”成立意味着“C不可满足不成立"、反之亦然，但  “C可满足” 与 “~C不可满足” 并不等价！——前一对命题中后者是前者的双重否定式，但后一对命题中后者不不是前者的双重否定式（把“可满足”看作一元谓词、把C看作个体常量即可。哇塞，二阶逻辑了！:)）。   确切地说：C不可满足意味着~C对（堪作当前KB的model的）任何解释都是可满足的；而C可满足时，~C也可能满足也可能不满足，即相当于啥也没说:) 。
     这一点其实完全不奇怪。再用FOL来描述：
     C不可满足 <-->  ~C恒满足   ：  ~exists.x.C(x) <--> forAny.x.~C(x)
     C可满足      -->  ~C ?          ：    exists.x.C(x)   -->         ?   ~C(x)
因此，判定C的可满足性与判定~C的可满足性对于能得到的关于C本身的结论，是完全不同的。
——感谢楼主及大家的讨论，才使我想了这么多、对这个问题才头一次感到这么清楚。

讨论越来越热烈了，是个好现象！^^

不过对于你的说法，我觉得你把问题复杂化了。

(1)实际上语法(syntax)包含了词法和句法，不管在一阶逻辑中还是在描述逻辑中都有，词法包括字母表，变元，常元，函数词的定义，句法是公式的定义。在描述逻辑中，词法就是concept description的归纳定义，比如
C,D -> Top|Bottom| C | C /\ D | C\/ D | \forall R.C | \exists R.C .....

而句法就是TBOX的terminology和ABOX中的assertion的定义，比如两种形式的公理 C= D 和 C< D，这些就相当于一阶逻辑中的formula。

(2)关于可满足：可满足是一个语义上的概念，C相对于知识库K可满足表示K有一个模型I使得C^I不是空集，而 K|= C<D (称为 C<D是K的语义后承) 的意思是对K的任意模型I，使得 C^I 是D^I的子集。由此可以证明， C /\ \neg D相对于K不可满足在语义上等价于 K|= C< D。

(3)关于C可满足和~C不可满足，再多说一句：两个问题互为补问题(complement)。从计算复杂性来说，在命题逻辑中，C可满足是NP的，C有效是coNP的。目前尚不清楚NP是否等于coNP。

姓名：(无权查看)
城市：(无权查看)
院校：(无权查看)

kAON2 也有一个显然的reasoning BUG: K={ \top subclassof \bot} is satisfiable by KAON2.

姓名：(无权查看)
城市：(无权查看)
院校：(无权查看)

你是想说 K={ \top subclassof \bot} is “consistent” by KAON2 ?

姓名：(无权查看)
城市：(无权查看)
院校：(无权查看)


	W 3 C h i n a ( since 2003 ) 旗下站点苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》	110.352ms