[DL] DL'03 paper
fgrandi at deis.unibo.it
Mon Sep 8 12:19:44 CEST 2003
This is a due note concerning my paper "A Tableau Algorithm for ALCN(o,U)"
that appeared in the DL'03 proceedings.
The claim at p. 72: <<no further application of the first five completion rules
can be triggered once Phase 2 has started>> is wrong.
I thank very much Franz Baader and Uli Sattler for having pointed it out.
As it is, the algorithm does not always produce a complete ABox.
By removing precondition 1. in the atmost-rule, the algorithm
produces a complete ABox but is not guaranteed to terminate.
Hence decidability of ALCN(o,U) actually remains an open problem.
-- Fabio Grandi
More information about the dl