'completeness' of OWL DL

Does what is called the 'computational completeness' of OWL DL [1] give
us the following property?

Given a query Q expressible in the language of an OWL DL ontology O,
an OWL DL reasoner will terminate in a finite amount of time, indicating
whether Q is true in all models of O.



What I'm trying to get at is a distinction between two different notions of
completeness, which Hintikka in [2] calls 'semantical completeness' and
'deductive completeness' [pp. 91, 92].

"[Semantical completeness] is a property of a so-called axiomatization
of (some part of) logic. It means that all the valid sentences of the
underlying language can be obtained as theorems from the so-called axioms
of that system of logic by means of its inference rules" [p. 91]

"Deductive completeness is a property of a nonlogical axiom system T
together with an axiomatization of logic (method of formal logical proof).
It means that from T one can prove by means of the underlying logic
C or not C for each sentence C of the language in question." [pp. 91,92]


Thanks,

Jim

------------------------------------------------------------------------------
[1] http://www.w3.org/TR/owl-features/
"computational completeness (all conclusions are guaranteed to be computable)"
(Section 1.3)

[2] The Principles of Mathematics Revisited. Cambridge, 1996.
------------------------------------------------------------------------------

Received on Sunday, 25 July 2004 14:13:21 UTC