Re: Semantics, in particular DAML+OIL semantics

Richard,

No one (not me at least) is saying that the "axiomatic semantics" is
not interesting/useful, but it is hard to see how it can live up to
the claims being made for it - often, it must be said, by people other
than yourself.

On August 17, Richard Fikes writes:
> 
> 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.

Well, it may be easily understood, but it is still an extension.

> > 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.

What you seem to be saying here is that by assuming the existence of
an *axiomatisation* of set theory, your axiomatisation could be
simpler. This is not hard to believe. It is *not*, however, the same
as the case of a model theory, which uses set theory directly and not
via an axiomatisation.

Another important point is that your axiomatisation makes heavy use of
lists and a number of list predicates without a complete specification
of their meaning. Adding a complete axiomatisation of lists and list
predicates would presumably add significantly to the 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.

This is of theoretical interest, but of limited practical value. The
additional complexity introduced by the axiomatisation itself, and the
fact that many important optimisations would be rendered useless,
would mean that reasoning with this kind of axiomatisation using a FOL
theorem prover would be hopelessly inefficient. 

Even reasoning with DAML+OIL/OWL via a direct translation into FOL
(i.e., classes as unary predicates) is problematical due to the
counting quantifiers (cardinality restrictions), which cannot be
efficiently handled by state of the art FOL implementations. I note
that in your axiomatisation this problem is "hidden" by the use of "No
Repeats Lists" and list predicates such as "length" for which a
complete axiomatisation is not provided.

To be honest, this part of the axiomatisation is a good example of my
complaint in that it is very hard to understand, and very hard to see
how it works. Note that I am not claiming that it doesn't work, simply
that it is very hard to be sure what the consequences of these axioms
would be and if they correspond to the simple conditions given in the
model theoretic semantics.

> 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.

Is the axiomatisation intended to be a specification of the intended
semantics of the logic, or an implementation of a reasoner for the
logic? You seem to want it to be both. In particular, you seem to
suggest using the axiomatisation as implementation to check the
axiomatisation as specification. By definition, the two should always
agree.

You say that this process can be used to "discover inconsistencies and
redundancies, and to determine whether they entail (only) intended
consequences". If this is useful, then it can only be because the
axiomatisation is sufficiently complex as to be likely to contain
errors - which is the very point I was making, and which in my view
makes such an axiomatisation unsuitable as the basic specification of
the intended meaning of the language. Moreover, how do you know what
really are the intended consequences if not by appeal to a simple
declarative specification of the semantics? This is exactly what a
model theoretic semantics provides.

Finally, you say that tools are used to determine whether the
axiomatisation entails "(only) intended consequences". As FOL is
undecidable, the best you can do is fail to find any unintended
consequences. Failure to find unintended consequences does not mean
that the axiomatisation is correct, simply that you either didn't try
the right test yet, or that your FOL prover is incomplete for some
(unintended) consequences. Similarly, failure to find an intended
consequence does not mean that the axiomatisation is incorrect as it
may be that your FOL prover is incomplete for this consequence.

This situation might be acceptable, even inevitable, for an
implementation, but is highly undesirable for a semantic
specification.

> 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."

I completely agree that FOL translation and theorem proving could be a
very useful tool as the expressive power of DAML+OIL is extended. I do
not see, however, how this argues in favour of an FOL axiomatisation
being the basic specification of the semantics of the language.

Regards, Ian




> 
> Richard

Received on Monday, 19 August 2002 06:51:12 UTC