完全析取范式检测ALCN-概念的可满足性

古华茂; 高济; 王勋

您当前的位置：

首页 >

文章列表页 >

完全析取范式检测ALCN-概念的可满足性

信息工程 | 更新时间：2023-11-28

- 完全析取范式检测ALCN-概念的可满足性
- Checking the Satisfiability of ALCN-concepts with a Complete DNF
- 工程科学与技术 2009年41卷第6期页码：165-170
- 作者机构：
  
  1. 浙江工商大学信息学院
  2. 浙江大学人工智能研究所
- 作者简介：
- 基金信息：
  
  国家自然科学基金(60775029);国家高技术研究发展计划(863)(2007AA01Z187);国家重点基础研究发展规划(973)(2003cb31700);浙江省科技计划（2007C33072）;浙江省自然科学基金(Y1090734)资助项目
- DOI：
  中图分类号：
- 纸质出版日期：2009，
  
  网络出版日期：2008-10-3，
扫描看全文
古华茂,高济,王勋.完全析取范式检测ALCN-概念的可满足性[J].工程科学与技术,2009,41(6):165-170.

Gu Hua-Mao, Gao Ji, Wang Xun. Checking the Satisfiability of ALCN-concepts with a Complete DNF[J]. Advanced Engineering Sciences, 2009,41(6):165-170.
古华茂,高济,王勋.完全析取范式检测ALCN-概念的可满足性[J].工程科学与技术,2009,41(6):165-170. DOI：

Gu Hua-Mao, Gao Ji, Wang Xun. Checking the Satisfiability of ALCN-concepts with a Complete DNF[J]. Advanced Engineering Sciences, 2009,41(6):165-170. DOI：

摘要

中文摘要: 基于“逐步展开”模式的Tableau算法在各类非循环定义的描述逻辑概念的可满足性判断中会产生大量的重复性的中间概念描述，因而浪费大量的空间。为此，提出了一个全新的对非循环定义的ALCN-概念可满足性进行判断的完全析取范式（CDNF）算法。CDNF算法直接在输入概念描述上，以角色为纽带构建不同层次的析取范式，从而将输入概念描述重组成一种层次结构的可满足性直接可知的完全析取范式，从而实现了真正意义上的“计算”可满足性。CDNF算法采用“一步到位”的展开方式并且直接在输入概念描述上进行处理，因而可最大程度地消除概念描述的重复。因此，CDNF算法比Tableau算法能节省线性甚至指数倍于输入概念描述长度的空间代价。

Abstract

Abstract:The Tableaux based on “unfolding gradually” may produce a lot of repetitive intermediate concept descriptions in deciding the satisfiabilities of acyclic concepts in a variety of description logics

which wastes large space. To tackle this problem

a novel Complete Disjunctive Normal Form (CDNF) algorithm was presented to check the satisfiabilities of acyclic ALCN-concepts. CDNF algorithm built disjunctive normal forms connected by roles in different levels directly on input concept description

and reorganized the input concept description into some hierarchical complete disjunctive normal forms whose satisfiabilities are already known

thus “worked out” satisfiabilities in a real sense. CDNF algorithm employed “one-step” unfolding pattern and acts directly on input concept description

thus eliminated description overlaps to the largest extent. As a result

CDNF algorithm had better performance than tableaux by saving spatial cost linearly or even exponentially.

关键词

可满足性推理析取范式ALCN

Keywords

reasoning on satisfiabilitydisjunctive normal formALCN

references

Stoilos G;Stamou G;Tzouvaras V,The fuzzy description logic f-SHIN,2005.

Chang L;Shi Z Z;Qiu L R;et 81.

Chang L;Lin F;Sift Z Z,A dynamic description logic for representation and reasoning about actions,New York:springer-verlag,2007.

Liebig T;Muller F,PamUelizing tableaux-based description logic reasoning,Berlin/Heidelberg:Springer,2007.

Lutz C;Mflici M,A Tableau algorithm for description logics with concrete domains and general TBoxes,Journal of Automated Reasoning,2007(1-3).

Horrocks I;Sattler U A Tableau decision procedure for SHOIQ [J]

Horrecks I;Satthr U,Ontology reasoning in the SHOQ(D) description logic,San Francisco:Morgan Kanfmann,2001.

Hustadt U;Motik B;Sattler U,Reasoning in description logics by a reduction to disjunctive datalog,Journal of Automated Reasoning,2007.

Stoilcs G;Stamou G;Pan J Z,Reasoning with very expressive fuzzy description logics,Journal of Artificial Intelligence Research,2007.

Baader F;Calvanese D;McGuinneas D L,The description logic handbook:Theory,implementation,and applications,Cambridge:Cambridge University Press,2003.

浏览量

188

下载量

CNKI被引量

文章被引用时，请邮件提醒。

提交

工具集

关联资源

暂无数据