[DL] DL'03 paper

[Fabio Grandi]

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.

Regards,
-- Fabio Grandi