-- 发布时间：9/19/2008 11:17:00 AM
-- 关于Tableau算法的说明（从描述逻辑手册翻译整理）
要点：任何一个标准否定形式的ALCN概念的可满足性，都可以通过应用一系列的变换法则，简化（归约）到一个有限的完全的Abox集合S^的可满足性上。S^的连续性可以通过检查其中是否包含矛盾（冲突）来判定。 任何ALCN概念的可满足性是可判定的。
下面是阅读时做的翻译笔记，附件中有需要的字体文件。供参考。
|
以文本方式查看主题 - 中文XML论坛 - 专业的XML技术讨论区 (http://bbs.xml.org.cn/index.asp) -- 『 Semantic Web(语义Web)/描述逻辑/本体 』 (http://bbs.xml.org.cn/list.asp?boardid=2) ---- 关于Tableau算法的说明（从描述逻辑手册翻译整理） (http://bbs.xml.org.cn/dispbbs.asp?boardid=2&rootid=&id=67420) |
|
-- 作者：duxiong -- 发布时间：9/19/2008 11:17:00 AM -- 关于Tableau算法的说明（从描述逻辑手册翻译整理） 要点：任何一个标准否定形式的ALCN概念的可满足性，都可以通过应用一系列的变换法则，简化（归约）到一个有限的完全的Abox集合S^的可满足性上。S^的连续性可以通过检查其中是否包含矛盾（冲突）来判定。 任何ALCN概念的可满足性是可判定的。 下面是阅读时做的翻译笔记，附件中有需要的字体文件。供参考。
|
|
-- 作者：xiaoqi1220 -- 发布时间：10/22/2008 10:04:00 PM -- 感谢！ |
|
-- 作者：hworld -- 发布时间：11/3/2008 4:44:00 PM -- 感谢！ |
|
-- 作者：xieyibupt -- 发布时间：3/21/2010 5:48:00 AM -- 感谢！ |
|
-- 作者：Avansky -- 发布时间：4/11/2010 9:02:00 AM -- 好好学习，天天向上！ |
|
-- 作者：xpg0312 -- 发布时间：4/12/2010 9:29:00 PM -- 一直对描述逻辑没有深入到的理解。多谢lz的东西。 |
|
-- 作者：sophiazsj -- 发布时间：11/23/2010 3:53:00 PM -- 谢谢！帮了很大的忙！ |
|
-- 作者：Kejia -- 发布时间：12/2/2010 12:27:00 AM -- 描述逻辑文献中的Tableau算法介绍比较晦涩。其实Tableau算法是适合自动证明的一阶逻辑算法中的一种，古已有之，很多一阶逻辑文献中讲得言简意赅。描述逻辑文献通常只是在罗列completion规则，对算法本身很少探究。Melvin Fitting的First-Order Logic and Automated Theorem Proving里就有对Tableau算法的详细论述，有一阶逻辑基础的读者可以很快领悟。 |
|
-- 作者：海豚_128 -- 发布时间：12/25/2012 2:03:00 PM -- 谢谢 |
|
W 3 C h i n a ( since 2003 ) 旗 下 站 点 苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》 |
7,253.906ms |