Re: Semantics, in particular DAML+OIL semantics

As the co-author of the "axiomatic semantics" for RDF, RDF-S, DAML-ONT,
and DAML+OIL, I want to comment on some points that Ian made earlier in
this discussion about such semantic specifications.

> While it is clear that, in some cases, it is useful to be able to talk
> about classes as instances, we should be clear that this means going
> outside first order logic into higher order logic (HOL), because we
> can now have predicates as the arguments of other predicates. If we
> accept classes as instances, then even OWL Lite (which is supposed to
> be "viewed by tool builders to be easy enough and useful enough to
> support") will be a HOL.

That is not true.  KIF (Knowledge Interchange Format) 3.0, for example,
is a first-order logic (FOL) and includes predicates in the domain of
discourse.  In KIF 3.0, quantification over predicates is allowed by
using a "holds" predicate that takes a predicate and its arguments as
its arguments.  One can argue whether or not the inclusion of "holds"
takes one out of first-order, but it is at worst a simple extension of
"classical" FOL that is easily understood.

> It is also worth pointing out that such axiomatisations are invariably
> large and complex, and that it is difficult/impossible to be sure that
> they are correct. E.g., take a look at the axiomatisation of
> DAML+OIL/RDF in [3], which contains around 140 axioms. FOL reasoners
> can be used to detect "obvious" inconsistencies (as happened with
> earlier versions of [3]), but simply ironing these out is a LONG way
> from proving that the axiomatisation correctly captures the meaning of
> the language.

The axiomatization of RDF, RDF-S, and DAML+OIL in [3] is large because
we made minimal assumptions about the underlying logic and about the
interpretation of properties.  That is, we assumed only classical FOL
with no "holds" predicate and no set theory.  So, the axiomatization
includes many axioms that would not need to be there if we had assumed a
set theory.  If we had assumed that properties are predicates, a "holds"
predicate, and set theory, then the number of axioms would be
dramatically smaller and each axiom would be shorter.  With those
assumptions, which correspond to the assumptions made when specifying a
model theory, the axiomatic semantics would be directly analogous to the
model theory in size and complexity.

The advantages of the FOL axiomatization are as follows as expressed in
our papers:

"First, the translations enable the use of traditional FOL automatic
theorem provers and problem solvers to answer queries and search for
logical inconsistencies in theories represented in the new languages.

Second, unlike standard descriptions of model-theoretic semantics, since
the constraints on the mappings are represented as axioms in a language
for which automatic reasoning tools are available, those constraints can
be subjected to critique using those tools to discover inconsistencies
and redundancies, and to determine whether they entail (only) intended
consequences.  Tools to support such critiques are particularly
important for the semantic specifications of languages that are still in
the development process (as is DAML+OIL), since they can help the
developers debug and understand the consequences of proposed language
changes.

Third, although the current versions of these languages could be
translated into a subset of FOL (e.g., into a description logic), the
development plan for DAML+OIL is to significantly expand its expressive
power in order to more fully support the expected representational
demands of Semantic Web ontologies.  The use of FOL translations and FOL
reasoning methods are expected to be accommodative, supportive, and
increasingly necessary as the expressive power of the language is
expanded."

Richard

Received on Saturday, 17 August 2002 20:04:17 UTC