with an concept forming operator naf of non-provability. This
operator can be applied to any concept term, but it
can only occur on the left-hand side of terminological axioms. The
resulting language is called 
.
We have considered an extension of the language
with an concept forming operator naf of non-provability. This
operator can be applied to any concept term, but it
can only occur on the left-hand side of terminological axioms. The
resulting language is called .
Intuitively, an object a belongs to a concept naf(C) if we cannot prove that it belongs to C. In essence the implementation uses the negation as failure operator of PROLOG.
