From: Ian Horrocks <horrocks@cs.man.ac.uk>

Date: Mon, 19 Aug 2002 11:48:47 +0100

Message-ID: <15712.52495.145253.769319@merlin.oaklands.net>

To: Richard Fikes <fikes@KSL.Stanford.EDU>

Cc: www-rdf-logic@w3.org

Date: Mon, 19 Aug 2002 11:48:47 +0100

Message-ID: <15712.52495.145253.769319@merlin.oaklands.net>

To: Richard Fikes <fikes@KSL.Stanford.EDU>

Cc: www-rdf-logic@w3.org

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 > > RichardReceived on Monday, 19 August 2002 06:51:12 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:38 UTC
*