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

Date: Sat, 17 Aug 2002 17:03:37 -0700

Message-ID: <3D5EE459.DA3D96A@ksl.stanford.edu>

To: www-rdf-logic@w3.org

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

Date: Sat, 17 Aug 2002 17:03:37 -0700

Message-ID: <3D5EE459.DA3D96A@ksl.stanford.edu>

To: www-rdf-logic@w3.org

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

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." RichardReceived on Saturday, 17 August 2002 20:04:17 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:38:24 UTC
*