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

新书推介：《语义网技术体系》
作者：瞿裕忠，胡伟，程龚

XML论坛

>>W3CHINA.ORG讨论区<<

计算机科学论坛

SOAChina论坛

Blog

开放翻译计划

新浪微博

首页

软件下载

资料下载

核心成员

帮助

>> 本版讨论Semantic Web(语义Web,语义网或语义万维网, Web 3.0)及相关理论，如：Ontology(本体,本体论), OWL(Web Ontology Langauge,Web本体语言), Description Logic(DL, 描述逻辑),RDFa,Ontology Engineering等。

[返回] W3CHINA.ORG讨论区 - 语义网·描述逻辑·本体·RDF·OWL → W3CHINA.ORG讨论区 - Web新技术讨论 → 『 Semantic Web(语义Web)/描述逻辑/本体』 → 请教Description Logics推理的问题！

◇查看新帖 ◇ 用户列表 ◇

(订阅本版)

您是本帖的第 25131 个阅读者　　

*	贴子主题：请教Description Logics推理的问题！	举报打印推荐 IE收藏夹
	本主题类别:

zhaonix

  威望：2
  头衔：博士
  等级：研一(日夜苦读RDF Semantics)
  文章：242
  积分：3185
  门派：W3CHINA.ORG
  注册：2005/4/18

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

	第11楼

有趣！琢磨了半天，觉得有了点眉目，见下面。大家批判：

以下是引用Leon.Essence在2007-10-29 11:38:00的发言：
显示不正确，我重写一遍，不好意思！
使用～代表not的意思
在描述逻辑中，如果有一个知识库和一个概念，那么下面的式子是成立的
K |= C <==> ～C unsatisfiable with K,

~~~~~~~错就错在这里。事实上, DL中在这里不满足类似于命题逻辑的排中律那样的东西，C is satisfiable w.r.t K 并不意味着～C is unsatisfiable w.r.t K ！请看DL Handbook 2.2.4.1中对Satisfiability的定义：A concept C is satisfiable with respect to T if there exists a model I of T such that CI is nonempty. 注意这里说的是“存在一个”而不是“任意一个” model of T。
另外，DL TBox中Satisfiability推理任务似乎也不这么写的：K|=C 。你见过K|=C<D, 见过K|=C(x)，但你见过K|=C吗？
倒是在命题逻辑系统中，有 K|=C 形式，表示的是任何弄真K的指派都使得命题C为真，因此K|=C和K|=D同时成立意味着在任何弄真K的指派下，C和D都永远为真，这当然意味着此情形下C和D要么同真要么同假，即K|=(C<->D)。

[此贴子已经被作者于2007-11-1 8:42:06编辑过]

2007/10/31 11:13:00

zhaonix

  威望：2
  头衔：博士
  等级：研一(日夜苦读RDF Semantics)
  文章：242
  积分：3185
  门派：W3CHINA.ORG
  注册：2005/4/18

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

	第12楼

以下是引用wjwenoch在2007-10-31 9:38:00的发言：
It is right. That you find it weird is due to the fact that both A and B are actually equivalent to *TOP* in DL.
We say K |= A, then A is a semantic consequence following from K, that is, A is SAT in every interpretation/model of K. So is B. thus A, B are tautologies.  In DL, they are actually *TOP* or GCIs. Am I correct?...

No unfortunately. :(  They are not the "TOP" concept.
    即使在DL中引入“K|=C”这样的表示方法以表示“K的任何一个model都是C的model”，也有个问题在于：一个解释如果是C的model的话，同时完全有可能是~C的model的。
    如 KB{TBox{A}, ABox{}} |=A 不假，但并不意味着A就是那个universal concept。因为任何一个赋予A一个非空的、哪怕只含有一个元素x的集合的解释，都是该KB的model，显然它也是A的model，同时也是~A的model——只要这个domain中除了x外还存在至少一个别的元素。
    baojie老大，我说的对吗？

[此贴子已经被作者于2007-11-1 8:54:03编辑过]

2007/10/31 11:40:00

Leon.Essence

  威望：9
  等级：大四寒假(收到Microsoft的Offer啦)(贵宾)
  文章：129
  积分：1409
  门派：W3CHINA.ORG
  注册：2005/9/4

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

	第13楼

以下是引用Leon.Essence在2007-10-29 16:43:00的发言：
谢谢wolfel，我回去再想想这个问题，总觉的有点不对！
最近一直在做DL方面的工作，碰到了很多问题，
下面有一个问题：
在DL中，C satisfiable with K 表示存在至少一个model同时满足K和C
C unsatisfiable with K 表示不存在model能同时满足K和C
现在假设K为{A subclassof B, D subclassof E} concept为C
则C应该是satisfiable with K的
  但是我在Pellet中，发现C is unsatisfiable with K，
这是为什么呢？

谢谢大家的讨论，首先我来总结以下上面这个问题，
正像baojie 和 wolfel 说的那样，这是Pellet设计的问题，
可以通过参数来改变，这是Evren的回复：
> Dear all,
>
> As we know, in DL,
> C satisfiable with K mean there exists at least one model of K such
> that the interpretation of C is nonempty.
> C unsatisfiable with K mean there doesn't exist any model of K which
> can interpret C.
>
> if K is set to {A subclass of B}, and  concept is set to C
> C should be satisfiable with K
>
> but in pellet, i found C is unsatisfiable with K,  why?
This is an API design decision for Pellet. The function
KnowledgeBase.isSatisfiable function will always return false for any
concept that is not defined in the KB although semantically there is no
constraint. This has proved to be more useful in practice because asking
for undefined concepts generally indicate an error on the calling function.
If you want to distinguish between logically inconsistent concepts and
undefined concepts there is a configuration option you can change. If
the option named SILENT_UNDEFINED_ENTITY_HANDLING is set to false then
isSatisfiable function will throw an UndefinedEntityException that you
can catch and handle accordingly.
Cheers,
Evren
----------------------------------------------
做个勤奋者,思考者,更要做个偏执狂!

2007/10/31 17:02:00

Leon.Essence

  威望：9
  等级：大四寒假(收到Microsoft的Offer啦)(贵宾)
  文章：129
  积分：1409
  门派：W3CHINA.ORG
  注册：2005/9/4

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

	第14楼

以下是引用zhaonix在2007-10-31 11:40:00的发言：
[quote]以下是引用wjwenoch在2007-10-31 9:38:00的发言：
  It is right. That you find it weird is due to the fact that both A and B are actually equivalent to *TOP* in DL.
  We say K |= A, then A is a semantic consequence following from K, that is, A is SAT in every interpretation/model of K. So is B. thus A, B are tautologies.  In DL, they are actually *TOP* or GCIs. Am I correct?...
[/quote]
No unfortunately. :(  They are not the "TOP" concept.
     即使在DL中引入“K|=C”这样的表示方法以表示“K的任何一个model都是C的model”，也有个问题在于：一个解释如果是C的model的话，同时完全有可能是~C的model的。
     如 KB{TBox{A}, ABox{}} |=A 不假，但并不意味着A就是那个universe concept。因为任何一个赋予A一个非空的、哪怕只含有一个元素x的集合的解释，都是该KB的model，显然它也是A的model，同时也是~A的model——只要这个domain中除了x外还存在至少一个别的元素。
     baojie老大，我说的对吗？

[此贴子已经被作者于2007-10-31 18:49:16编辑过]

K|=C <==> ~C is unsatisfiable with K
这表明 ~C的解释为空集，即bottom concept
所以C为universal concept
----------------------------------------------
做个勤奋者,思考者,更要做个偏执狂!

2007/10/31 19:14:00

wjwenoch

  等级：大三(要不要学学XML呢?)
  文章：101
  积分：744
  门派：W3CHINA.ORG
  注册：2006/2/13

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

	第15楼

以下是引用zhaonix在2007-10-31 11:13:00的发言：
有趣！琢磨了半天，觉得有了点眉目，见下面。大家批判：
[quote]以下是引用Leon.Essence在2007-10-29 11:38:00的发言：
显示不正确，我重写一遍，不好意思！
  使用～代表not的意思
  在描述逻辑中，如果有一个知识库和一个概念，那么下面的式子是成立的
  K |= C <==> ～C unsatisfiable with K,
[/quote]
~~~~~~~错就错在这里。事实上, DL中在这里不满足类似于命题逻辑的排中律那样的东西，C is satisfiable w.r.t K 并不意味着～C is unsatisfiable w.r.t K ！请看DL Handbook 2.2.4.1中对Satisfiability的定义：A concept C is satisfiable with respect to T if there exists a model I of T such that CI is nonempty. 注意这里说的是“存在一个”而不是“任意一个” model of T。
     另外，DL TBox中Satisfiability推理任务似乎也不这么写的：K|=C 。你见过K|=C<D, 见过K|=C(x)，但你见过K|=C吗？
倒是在命题逻辑系统中，有 K|=C 形式，表示的是任何弄真K的指派都使得命题C为真，因此K|=C和K|=D同时成立意味着在任何弄真K的指派下，C和D都永远为真，意味着此情形下C和D要么同真要么同假，即K|=(C<->D)。

The author used "K |= C" not to claim "C is SAT with K", but instead showed that C is a tautology/valid.
It is actually saying "C is valid w.r.t K" from the previous context. In all, it is not a SAT representation when he used "K |= C".
I think "K |= C " is allowed. You can treat it as "K |= (C implies TOP)".
----------------------------------------------
一个人炫耀什么，就表示他缺乏什么。

2007/11/1 3:49:00

baojie

  威望：9
  头衔：小学生
  等级：研一(参加了一年一度的XML大会)(贵宾)
  文章：667
  积分：4442
  门派：XML.ORG.CN
  注册：2003/11/24

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

	第16楼

我觉得问题还是出在楼主的 K|=C 表示方法。通用的描述逻辑语法里，是没有这样的形式的。如果写在文章里，读者会很困惑的。

2007/11/1 4:47:00

zhaonix

  威望：2
  头衔：博士
  等级：研一(日夜苦读RDF Semantics)
  文章：242
  积分：3185
  门派：W3CHINA.ORG
  注册：2005/4/18

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

	第17楼

以下是引用Leon.Essence在2007-10-31 19:14:00的发言：
  K|=C <==> ~C is unsatisfiable with K
这表明 ~C的解释为空集，即bottom concept
所以C为universal concept

得到baojie的确认，看来问题很清楚了：楼主自己创造了一种表示法！:)   而且与读者(至少如我)根据命题逻辑中这种表示方法的含义所形成的直觉（任何是K的模型的解释必然也是C的模型）不一致:(
如果这个表示法是楼主这个意思的话，那还存在刚开始说的问题吗？——C和D都是universal concept了，当然互相subClassOf了可能楼主一开始也不是很确定这个表示法的用意。
     事实上，这个新奇的表示法所表示的意思是可以很自然地用现有的DL表示方法来表示的： K|=T<C  (其中T表示universal concept， “<”表示 subClassOf) ——一个最典型不过的DL推理任务。

2007/11/1 8:51:00

wolfel

  威望：2
  等级：计算机学士学位
  文章：280
  积分：2178
  门派：W3CHINA.ORG
  注册：2005/3/17

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

	第18楼

以下是引用wjwenoch在2007-11-1 3:49:00的发言：
[quote]以下是引用zhaonix在2007-10-31 11:13:00的发言：
有趣！琢磨了半天，觉得有了点眉目，见下面。大家批判：
  [quote]以下是引用Leon.Essence在2007-10-29 11:38:00的发言：
  显示不正确，我重写一遍，不好意思！
   使用～代表not的意思
   在描述逻辑中，如果有一个知识库和一个概念，那么下面的式子是成立的
   K |= C <==> ～C unsatisfiable with K,
  [/quote]
  ~~~~~~~错就错在这里。事实上, DL中在这里不满足类似于命题逻辑的排中律那样的东西，C is satisfiable w.r.t K 并不意味着～C is unsatisfiable w.r.t K ！请看DL Handbook 2.2.4.1中对Satisfiability的定义：A concept C is satisfiable with respect to T if there exists a model I of T such that CI is nonempty. 注意这里说的是“存在一个”而不是“任意一个” model of T。
      另外，DL TBox中Satisfiability推理任务似乎也不这么写的：K|=C 。你见过K|=C<D, 见过K|=C(x)，但你见过K|=C吗？
  倒是在命题逻辑系统中，有 K|=C 形式，表示的是任何弄真K的指派都使得命题C为真，因此K|=C和K|=D同时成立意味着在任何弄真K的指派下，C和D都永远为真，意味着此情形下C和D要么同真要么同假，即K|=(C<->D)。

[/quote]
The author used "K |= C" not to claim "C is SAT with K", but instead showed that C is a tautology/valid.
It is actually saying "C is valid w.r.t K" from the previous context. In all, it is not a SAT representation when he used "K |= C".
I think "K |= C " is allowed. You can treat it as "K |= (C implies TOP)".

我觉得有问题，有效式（valid）并不是tautology，有效式是在前提集的所有model下成真的，但是tautology是对任意解释都为真，K|=C, 只能有C是有效的，单并不能等价于TOP。
LZ的问题我已经跟他讨论过，其实问题出在这里：
K|=A <=> K \/ {\neg A}中A不可满足 => K \/ {\neg A}中 A /\ \neg B不可满足 <=> K \/ {\neg A}|= A \sqsubseteq B
K|= B <=> K \/ {\neg B}中B不可满足 => K \/ {\neg B}中\neg A /\ B不可满足 <=> K \/ {\neg B} |= B\sqsubseteq A
由于推出 A\sqsubseteq B和推出 B\sqsubseteq A的前提集不同，因此根本得不到 A=B
----------------------------------------------
Correct reasoning is our business.

2007/11/1 10:30:00

wolfel

  威望：2
  等级：计算机学士学位
  文章：280
  积分：2178
  门派：W3CHINA.ORG
  注册：2005/3/17

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

	第19楼

以下是引用zhaonix在2007-11-1 8:51:00的发言：
[quote]以下是引用Leon.Essence在2007-10-31 19:14:00的发言：
   K|=C <==> ~C is unsatisfiable with K
  这表明 ~C的解释为空集，即bottom concept
  所以C为universal concept
[/quote]
得到baojie的确认，看来问题很清楚了：楼主自己创造了一种表示法！:)   而且与读者(至少如我)根据命题逻辑中这种表示方法的含义所形成的直觉（任何是K的模型的解释必然也是C的模型）不一致:(
如果这个表示法是楼主这个意思的话，那还存在刚开始说的问题吗？——C和D都是universal concept了，当然互相subClassOf了可能楼主一开始也不是很确定这个表示法的用意。
      事实上，这个新奇的表示法所表示的意思是可以很自然地用现有的DL表示方法来表示的： K|=T<C  (其中T表示universal concept， “<”表示 subClassOf) ——一个最典型不过的DL推理任务。

跟表示方法没有关系，你可以认为 C是一个描述逻辑公式比如 A < B
----------------------------------------------
Correct reasoning is our business.

2007/11/1 10:32:00

zhaonix

  威望：2
  头衔：博士
  等级：研一(日夜苦读RDF Semantics)
  文章：242
  积分：3185
  门派：W3CHINA.ORG
  注册：2005/4/18

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

	第20楼

以下是引用wolfel在2007-11-1 10:32:00的发言：
跟表示方法没有关系，你可以认为 C是一个描述逻辑公式比如 A < B

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

2007/11/1 19:37:00

GoogleAdSense

  等级：大一新生
  文章：1
  积分：50
  门派：无门无派
  院校：未填写
  注册：2007-01-01

	广告

2024/6/16 1:50:50

本主题贴数41，分页： [1] [2] [3] [4] [5]

管理选项：修改tag | 锁定 | 解锁 | 提升 | 删除 | 移动 | 固顶 | 总固顶 | 奖励 | 惩罚 | 发布公告


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