| Popis: |
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. |
