Paper Title:
Deciding the ALCNIR+-Satisfiability with a Fully Tiered Clause
  Abstract

In contrast with Tableau algorithm, this paper presented a totally new approach to check the satisfiabilities of acyclic ALCNIR+-concepts―FTC algorithm. This calculus can make a direct judgment on the satisfiability of an acyclic ALCNIR+-concept by translating its description into a fully tiered clause whose satisfiability is directly available. FTC algorithm eliminates description overlaps to largest extent as it works on concept description directly. Therefore, FTC algorithm has notably better performance than Tableaux by saving a lot of spatial costs.

  Info
Periodical
Key Engineering Materials (Volumes 439-440)
Edited by
Yanwen Wu
Pages
1337-1342
DOI
10.4028/www.scientific.net/KEM.439-440.1337
Citation
H. M. Gu, J. Q. Shi, X. J. Zhu, "Deciding the ALCNIR+-Satisfiability with a Fully Tiered Clause", Key Engineering Materials, Vols. 439-440, pp. 1337-1342, 2010
Online since
June 2010
Export
Price
$32.00
Share

In order to see related information, you need to Login.

In order to see related information, you need to Login.

Authors: Jun Ping Zhou, Chun Guang Zhou, Ming Hao Yin, Hui Yang
Abstract:Extension rule is a new method for computing the number of models for a given propositional formula. In some sense, it is actually an inverse...
268
Authors: Jun Ping Zhou, Chun Guang Zhou, Yan Dong Zhai, Yong Juan Yang
Abstract:Extension rule is a new method for computing the number of models for SAT formulae. In this paper, we investigate the use of the extension...
250
Authors: Qin Guo, Ai Lian Wang, Ying Liu
Abstract:Preprocessing model counting instances can reduce their size considerably and decrease the solving time. In this paper we present a...
2033
Authors: Yan Xin Lu, Zi Qun Zhang
Chapter 2: Mechanical Engineering and Application
Abstract:Intelligent information processing is one of important research parts of knowledge reasoning as well as methods in artificial intelligence....
58