假设K|=A, K|=B，那么K和¬A，¬B都是unsatifiable的，
这意味着K unsatifiable with A∧¬B和¬A∧B
前者可以推出K|=A subclassof B，后者可以推出K|=B subclassof A

这肯定是不对的，可是错在什么地方呢？

请高手指教！谢谢！

使用～代表not的意思

在描述逻辑中，如果有一个知识库和一个概念，那么下面的式子是成立的
K |= C <==> ～C unsatisfiable with K,

假设K|=A, K|=B，那么K和～A，～B都是unsatifiable的，
这意味着K unsatifiable with A∧～B和～A∧B
前者可以推出K|=A subclassof B，后者可以推出K|=B subclassof A

这肯定是不对的，可是错在什么地方呢？

请高手指教！谢谢！

实际上就是这样的：

K|=A => K|=A \/~ B <=> K|= B->A
K|=B => K|= ~A\/B  <=> K|= A->B

于是有 K |= A<->B

但是我觉得不正确，因为如果这样的话，
岂不是意味着知识库imply的任意concept都是相等的！

Thanks for any comments!

对于K的所有可能世界，假如A和B在所有可能世界中都能得到满足，那么A和B的不同就仅仅在于他们使用了不同的名字，但是在论域中的指称都是相同的。

注意：A=B的语义是 A^I=B^I

最近一直在做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，
这是为什么呢？

我查了一下描述逻辑手册，提到描述逻辑的语义解释只是针对语言中出现的符号，我理解就是只是针对知识库中有的符号进行解释，没有提到语言中没有出现的符号如何解释。

你举的例子中，C没有出现在K中，所以我觉得也许pallet中认为语言中没有出现的符号，自动解释为空集了，因此C就不可满足。我觉得这是一种特殊情况，推理机可以自己选择处理这种特例的方法，所以如果认为C可满足，也是说得过去的。

至少我是这么觉得的，欢迎大家拍砖～

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?...

“现在假设K为{A subclassof B, D subclassof E} concept为C 则C应该是satisfiable with K的   但是我在Pellet中，发现C is unsatisfiable with K，这是为什么呢？”

这应该看作Pellet的bug。理论上,C是可满足的。

以下是引用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)。

    baojie老大，我说的对吗？

谢谢大家的讨论，首先我来总结以下上面这个问题，
正像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

K|=C <==> ~C is unsatisfiable with K
这表明 ~C的解释为空集，即bottom concept
所以C为universal concept

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)".

得到baojie的确认，看来问题很清楚了：楼主自己创造了一种表示法！:)   而且与读者(至少如我)根据命题逻辑中这种表示方法的含义所形成的直觉（任何是K的模型的解释必然也是C的模型）不一致:(

如果这个表示法是楼主这个意思的话，那还存在刚开始说的问题吗？——C和D都是universal concept了，当然互相subClassOf了 可能楼主一开始也不是很确定这个表示法的用意。
     事实上，这个新奇的表示法所表示的意思是可以很自然地用现有的DL表示方法来表示的： K|=T<C  (其中T表示universal concept， “<”表示 subClassOf) ——一个最典型不过的DL推理任务。

我觉得有问题，有效式（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

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

那 ~(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提的这个问题实际上是一个一阶逻辑的问题。

这种认为每个知识库有自己不同的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
至于为什么一直不这么写，也许是因为习惯或者难以理解等等问题。

望大家指点！

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

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

至于楼主说的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也可能满足也可能不满足，即相当于啥也没说:) 。”
那个“不”字貌似多余的。。。

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

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

(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。

对的！但是注意一点就是 x可满足和x不可满足是互为补问题，C可满足和~C不可满足分别是两个问题的实例而已， 与逻辑否定~没有关系。

这个问题本身就是错误的.

想问一下楼主,  K |= C 是什么???  

看你的帖子,C应该是一个concept. 但是实际上 在DL 里面 K |= C 是没有意义的?

只有  K |= C(a) 或者  K |= C subsumed D 才有意义.

以下是引用Leon.Essence在2007-10-29 11:38:00的发言： 显示不正确，我重写一遍，不好意思！ 使用～代表not的意思 在描述逻辑中，如果有一个知识库和一个概念，那么下面的式子是成立的 K |= C <==> ～C unsatisfiable with K, 假设K|=A, K|=B，那么K和～A，～B都是unsatifiable的， 这意味着K unsatifiable with A∧～B和～A∧B 前者可以推出K|=A subclassof B，后者可以推出K|=B subclassof A 这肯定是不对的，可是错在什么地方呢？ 请高手指教！谢谢！

以下是引用kolapig在2007-11-3 2:10:00的发言： 不是吧,各位! 这个问题本身就是错误的. 想问一下楼主,  K |= C 是什么???   看你的帖子,C应该是一个concept. 但是实际上 在DL 里面 K |= C 是没有意义的? 只有  K |= C(a) 或者  K |= C subsumed D 才有意义. [quote]以下是引用Leon.Essence在2007-10-29 11:38:00的发言： 显示不正确，我重写一遍，不好意思！   使用～代表not的意思   在描述逻辑中，如果有一个知识库和一个概念，那么下面的式子是成立的   K |= C <==> ～C unsatisfiable with K,   假设K|=A, K|=B，那么K和～A，～B都是unsatifiable的，   这意味着K unsatifiable with A∧～B和～A∧B   前者可以推出K|=A subclassof B，后者可以推出K|=B subclassof A   这肯定是不对的，可是错在什么地方呢？   请高手指教！谢谢！ [/quote]

A is satisfiable with K
<=> (这步是对的,)
not A is unsatisfiable with K
=> (这步是对的, )
not A and B is unsatisfiable with K
<=> (这步也是对的)
A and not B is satisfiable with K
<=> (这步就*不对*了,看下面的解释)
K |= B subsumed A

解释: "A and not B is satisfiable with K" 表明 *存在一个  x* such that   
K |= A and not B(x) . 但是 "K |= B subsumed A" 是 说 *对于 所有的 x*, K |= A and not B(x) 成立.

以下是引用Leon.Essence在2007-10-29 11:38:00的发言： 显示不正确，我重写一遍，不好意思！ 使用～代表not的意思 在描述逻辑中，如果有一个知识库和一个概念，那么下面的式子是成立的 K |= C <==> ～C unsatisfiable with K, 假设K|=A, K|=B，那么K和～A，～B都是unsatifiable的， 这意味着K unsatifiable with A∧～B和～A∧B 前者可以推出K|=A subclassof B，后者可以推出K|=B subclassof A 这肯定是不对的，可是错在什么地方呢？ 请高手指教！谢谢！

这步不对吧？ 见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 C^I is nonempty. 注意这里说的是“存在一个”而不是“任意一个” model of T。

最明显的是例子是{p\/q}中，p和~p都是可满足的...

A is satisfiable with K
<=>
存在 x使得 K|= A(x)
<=>
存在 x 使得 K |= A or not B (x)
<=>
A or not B is satisfiable with K
<=> (这步就*不对*了)
K |= B subsumed A

解释: "A and not B is satisfiable with K" 表明 *存在一个  x* such that   
K |= A and not B(x) . 但是 "K |= B subsumed A" 是 说 *对于 所有的 x*, K |= A and not B(x) 成立.

这下该对了... 在此抱歉。。。。。

以下是引用wolfel在2007-11-3 18:51:00的发言： A相应于K可满足的时候，~A相应于K也有可能可满足 最明显的是例子是{p\/q}中，p和~p都是可满足的... [此贴子已经被作者于2007-11-3 21:40:20编辑过]

一开始的错误就是把 ''A is satisfiable with K'' 理解为 K|= A.
首先, K|= A这个表示方法是不存在的, 应该是楼主把''A is satisfiable with K'' 混淆了 K|= A(a).
其次, K|= A(a) 不是 ''A(a) is satisfiable with K''(即存在一个K的model 使得 A(a)成立), 而是 ''K可以推出 A(a)'', (即''对于K 得所有model, A(a)都满足'').

欢迎评论...

以下是引用kolapig在2007-11-3 2:32:00的发言： 最根本的问题是搂主对  satisfiable和 |= 的关系 的理解错误 A is satisfiable with K <=> (这步是对的,) not A is unsatisfiable with K => (这步是对的, ) not A and B is unsatisfiable with K <=> (这步也是对的) A and not B is satisfiable with K <=> (这步就*不对*了,看下面的解释) K |= B subsumed A 解释: "A and not B is satisfiable with K" 表明 *存在一个  x* such that    K |= A and not B(x) . 但是 "K |= B subsumed A" 是 说 *对于 所有的 x*, K |= A and not B(x) 成立. [quote]以下是引用Leon.Essence在2007-10-29 11:38:00的发言： 显示不正确，我重写一遍，不好意思！   使用～代表not的意思   在描述逻辑中，如果有一个知识库和一个概念，那么下面的式子是成立的   K |= C <==> ～C unsatisfiable with K,   假设K|=A, K|=B，那么K和～A，～B都是unsatifiable的，   这意味着K unsatifiable with A∧～B和～A∧B   前者可以推出K|=A subclassof B，后者可以推出K|=B subclassof A   这肯定是不对的，可是错在什么地方呢？   请高手指教！谢谢！ [/quote]

    A is satisfiable with K
    <=>
    存在 x使得 K|= A(x)

因为1)"|="符号表示的是对于左侧KB的“任意”model如何如何，现在与“存在x”放在一起似乎不太和谐:)；
2)satisfiable的原始定义中说的是存在KB的一个model……，而不是存在x。改写如下应该就没问题了：

A is satisfiable with K
<=>
存在一个K的model I使得 A^I不为空
<=>
存在一个K的model I使得 (A or not B)^I不为空
<=>
A or not B is satisfiable with K
<=> (这步就*不对*了)
K |= B is subsumed by A  //不是subsume
因为上面最后这个式子 <=>
K|= TOP is subsumed by (A or not B)  //而不是(A or not B)本身

以下是引用zhaonix在2007-11-4 9:17:00的发言： [quote]以下是引用kolapig在2007-11-4 6:02:00的发言： 这个帖子从本质上来讲,   一开始的错误就是把 ''A is satisfiable with K'' 理解为 K|= A.   首先, K|= A这个表示方法是不存在的, 应该是楼主把''A is satisfiable with K'' 混淆了 K|= A(a).   其次, K|= A(a) 不是 ''A(a) is satisfiable with K''(即存在一个K的model 使得 A(a)成立), 而是 ''K可以推出 A(a)'', (即''对于K 得所有model, A(a)都满足'').   欢迎评论... [/quote] [quote]以下是引用kolapig在2007-11-4 6:02:00的发言： 这个帖子从本质上来讲,   一开始的错误就是把 ''A is satisfiable with K'' 理解为 K|= A.   首先, K|= A这个表示方法是不存在的, 应该是楼主把''A is satisfiable with K'' 混淆了 K|= A(a).   其次, K|= A(a) 不是 ''A(a) is satisfiable with K''(即存在一个K的model 使得 A(a)成立), 而是 ''K可以推出 A(a)'', (即''对于K 得所有model, A(a)都满足'').   欢迎评论... [/quote] 嗯，真相大白，达成共识。热烈的讨论基本上圆满结束：） 一点小疑问：既然你这一贴也这么说了。那么再上面一楼里的如下说法是不是严格来说也不贴切：      A is satisfiable with K      <=>      存在 x使得 K|= A(x) 因为1)"|="符号表示的是对于左侧KB的“任意”model如何如何，现在与“存在x”放在一起似乎不太和谐:)； 2)satisfiable的原始定义中说的是存在KB的一个model……，而不是存在x。改写如下应该就没问题了： A is satisfiable with K <=> 存在一个K的model I使得 A^I不为空 <=> 存在一个K的model I使得 (A or not B)^I不为空 <=> A or not B is satisfiable with K <=> (这步就*不对*了) K |= B is subsumed by A  //不是subsume 因为上面最后这个式子 <=> K|= TOP is subsumed by (A or not B)  //而不是(A or not B)本身