以文本方式查看主题

-  W3CHINA.ORG讨论区 - 语义网·描述逻辑·本体·RDF·OWL  (http://bbs.xml.org.cn/index.asp)
--  『 Semantic Web(语义Web)/描述逻辑/本体 』  (http://bbs.xml.org.cn/list.asp?boardid=2)
----  请教一个问题,为什么很多文章说描述逻辑是一阶逻辑的可判定子集?  (http://bbs.xml.org.cn/dispbbs.asp?boardid=2&rootid=&id=72258)


--  作者:jjwwjjww
--  发布时间:2/24/2009 4:17:00 PM

--  请教一个问题,为什么很多文章说描述逻辑是一阶逻辑的可判定子集?
很多文章说描述逻辑是一阶逻辑的可判定子集,可是没有说理由啊。什么叫一个逻辑是另一个逻辑的子集?好像不像集合A是集合B的定义那样的!
--  作者:iamwym
--  发布时间:2/24/2009 4:26:00 PM

--  
楼主只是觉得中文名词,逻辑,是无法作为集合存在吧。其实描述逻辑和一阶逻辑都是一系列的公理的集合,这样理解就可以了。

--  作者:jjwwjjww
--  发布时间:2/26/2009 2:57:00 PM

--  
还有一个问题:如何理解描述逻辑是一阶逻辑的可判定子集?有些描述逻辑系统是不可判定的,有些是可以判定。描述逻辑应该是一类逻辑,不是一个逻辑。而一阶逻辑是一个逻辑。这理解对吗?
--  作者:Huang
--  发布时间:3/4/2009 9:17:00 PM

--  
人们通常把一阶谓词逻辑看成是一个逻辑, 但这并不影响人们还可以对一阶逻辑的公式作进一步的限定, 如只允许使用2个不同的变元, 这个逻辑被称为2变元一阶逻辑(two variable logic, 缩写为FO2)。 由于变元可以有作用域,所以这2个不同的变元在一定的情况下可以重复使用, 所以FO2表达能力还是比较强的。

Mortimer 于1975年证明了FO2具有有限模型性(Finite model property)。搞逻辑的人都知道所有具有有限模型性的完备的(complete)逻辑都是可判定的, 所以FO2的可满足性问题是可判断的。

Schilder 于1991年指出最常用的描述逻辑ALC在语义上直接对应着多模态逻辑K系统。熟悉模态逻辑的人都知道多数模态逻辑都可以对应到2变元一阶逻辑(再加上一些语义公理)的子逻辑。所以我们可以说,多数描述逻辑在语义上对应着一阶逻辑的一个可判定的子逻辑(fragment)。


--  作者:jjwwjjww
--  发布时间:3/5/2009 12:21:00 PM

--  
语义上对应具体是什么含义?是指许多描述逻辑系统可以satisfiability-preserving 翻译(对应)到一阶逻辑的fragment(片断)。这里,我把fragment译成片断,因为子逻辑的定义是不明确的。
--  作者:wolfel
--  发布时间:3/5/2009 3:37:00 PM

--  
所谓语义上对应,我觉得是说它们的语义模型上具有同态关系。描述逻辑的语义是一个structure,一阶逻辑的语义也是,所以一个描述逻辑系统翻译成一阶逻辑公式之后,他们的语义模型是同构的(我没有证明过,不过看起来很显然)。

但是如果给出一个一阶公式,却找不到对应的描述逻辑公式,使之具有同构的模型。所以可以说描述逻辑的语义是一阶逻辑语义的子集。


--  作者:jjwwjjww
--  发布时间:3/5/2009 7:57:00 PM

--  
一个描述逻辑系统翻译到一阶逻辑的一个片断(fragment)上分为两层:语法和语义。
语法:任意给定一个描述逻辑的断言翻译到一阶逻辑的公式;
语义:任意给定一个描述逻辑的模型翻译到一阶逻辑的一个模型。由于描述逻辑的模型和一阶逻辑的模型都是一个structure,所以语义上的翻译是明显的。但是这个翻译不是满的。
--  作者:wolfel
--  发布时间:3/7/2009 3:05:00 PM

--  
你说的没错,这些都是很显然的。描述逻辑公式在语法上也只能翻译成有两个变元的一届逻辑公式。这样称呼为子集没有什么问题。再说也没有必要再这个称谓上纠缠太多。
--  作者:marylogic
--  发布时间:7/24/2011 9:59:00 PM

--  
并不是所有的描述逻辑的公式都可以翻译成一阶逻辑的公式啊?所以才只能说描述逻辑是语义上对应到一阶逻辑的一个片段。这样理解对吗?
--  作者:yezhunan3h
--  发布时间:7/25/2011 5:00:00 AM

--  
黄老师说的已经很完全了。。  

marylogic的理解不对,一阶逻辑本身是semi-decidable的,而且不具备finite model property,除非做一些限制。

我认为可以这样理解,用FOL可以表述所有DLs,但反之不行。。

DLs都可以转化为FOL,比如目前最复杂的SROIQ的FOL-translation,可以看yevgeny的这篇论文(http://www.cs.ox.ac.uk/isg/people/yevgeny.kazakov/publications/confs/Kaz08SROIQ_KR.pdf)。

哪个DLs不可以,请麻烦指出来一下。。


有一点我不太清楚的是,比如SROIQ中,对于一些role的操作是有限制的,simple role什么的,定义这些限制是否能用FOL定义??


--  作者:yezhunan3h
--  发布时间:7/25/2011 5:06:00 AM

--  
marylogic另外一个帖子中还问到FOL和DLs的优缺点。。

其实很显然,不可判定的意思是没有一个算法能在有限时间内给出是或不是。。FOL是semi-decidable,意思是如果问题是正确的,那么没问题,tableau一下就行。但如果问题是错的,这个算法可能永远跑下去了。。  

DLs基本都是可判定的,尽管像OWl-1是NEXPTIME的,OWL-2是N2EXPTIME的,但这说的都是worst的情况,实际中我们可以做很多算法优化,做一些启发式算法,做并行,随你怎么整,整快了就行,所以很多复杂的OWL2推理也是可以接受的。


--  作者:marylogic
--  发布时间:7/25/2011 12:58:00 PM

--  关系的传递闭包不可以用FOL表示
比如关系的传递闭包不可以用FOL表示,但是可以用DL表示。
--  作者:marylogic
--  发布时间:7/25/2011 1:01:00 PM

--  
描述逻辑有认知, 模态,时态的扩充,显然做在扩充之后的公式无法翻译到一阶公式了。
W 3 C h i n a ( since 2003 ) 旗 下 站 点
苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》
62.500ms