Determining the SHOIN(D)-Satisfiability with a Complete Disjunctive Normal Form Group
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    This paper presents an approach to check the satisfiability of acyclic SHOIN(D)-concepts—CDNF (complete disjunctive normal form) algorithm. This calculus can make a direct judgment on the satisfiability of acyclic SHOIN(D)-concept by restructuring it into a hierarchical disjunctive normal form group on concept descriptions which is satisfiability self-telling, and reusing description clauses to block unnecessary extensions. CDNF algorithm eliminates description overlaps to the largest extent for it works on concept description directly. Therefore, CDNF algorithm has much better performance than Tableau as it saves a lot of spatial and temporal costs.

    Reference
    Related
    Cited by
Get Citation

古华茂,王 勋,凌 云,高 济.完全析取范式群判定SHOIN(D)-可满足性.软件学报,2010,21(8):1863-1877

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 31,2008
  • Revised:February 16,2009
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063