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

Date: Sun, 17 Jun 2001 22:50:25 +0100 (BST)

Message-ID: <15149.9761.204926.392370@excalibur.cs.man.ac.uk>

To: pat hayes <phayes@ai.uwf.edu>

Cc: Jerome.Euzenat@inrialpes.fr (Je'ro^me Euzenat), www-rdf-logic@w3.org

Date: Sun, 17 Jun 2001 22:50:25 +0100 (BST)

Message-ID: <15149.9761.204926.392370@excalibur.cs.man.ac.uk>

To: pat hayes <phayes@ai.uwf.edu>

Cc: Jerome.Euzenat@inrialpes.fr (Je'ro^me Euzenat), www-rdf-logic@w3.org

On June 12, pat hayes writes: > >Hi all, > > > >In his message (RE: rdf as a base for other languages) of 7/06/01, > >pat hayes wrote: > >>> >I agree that would be a desirable goal. BTW, the 'A-/T-box' > >>> >terminology was originally used to distinguish assertions from > >>> >definitions (of concept vocabulary) , which isnt quite exactly the > >>> >same as the ground-fact/rule distinction. > >>> > >>>Could you elucidate the distinction between definitions and > >>>assertions, and explain how this differs from ground-fact/rule? > >> > >>Ah, now I have painted myself into a corner, since I never fully > >>understood the definition/assertion distinction myself, though it > >>seemed central to many folk (and still does). Although to be fair, > >>the idea of a definition is a pretty common one in mathematics and > >>life generally, in spite of its having no obvious logical content. > >>The intuition as I understand it is that saying that Foo is defined > >>by a certain assertion (eg a biconditional, say, but it could have > >>any logical form) is saying more than simply that the assertion is > >>true of Foo; it is saying that this condition is in some sense 'all > >>there is' to the meaning of Foo; that it completely defines the > >>meaning. This is not to say, of course, that the definition > >>completely specifies all the facts involving Foo, since the whole > >>point, usually, of defining concepts is so that they can be handily > >>used to state new facts. But it does imply a distinction between > >>the facts about Foo that are definitional in nature - that specify > >>the meaning of Foo, and moreover do so in some sense completely, ie > >>comprise a full account of that meaning - and facts about Foo that > >>are merely facts, which are stated using 'Foo' but which are not, > >>as it were, constitutive of the actual meaning. So for example, if > >>the defining condition were simply an assertion about the concept, > >>then to assert something that contradicts that definition would > >>simply generate a contradiction; but if it is taken to be > >>definitional, then one knows immediately that the contradicting > >>assertion must be false. > >> > >>...] Certainly it cannot be identified with anything as simple as a > >>syntactic distinction like ground-fact/quantified rule. Some > >>ontology folk argue that making the distinction logically requires > >>the use of a modal logic, so that definitions are not just true but > >>necessarily true, or that the terms so defined are 'rigid' (have > >>the same denotation in every possible world.) I have rather a > >>jaundiced view of this approach, but that is a topic which probably > >>goes beyond the purview of this mailing list. But in any case, many > >>Krep systems have tried to provide some way to make the > >>distinction. (KIF for example has an elaborate syntax for defining > >>relations, functions and so on.) The A-box/T-box distinction was > >>one such attempt. The key operational point, as I understand it, is > >>that while both the Tbox and the Abox consist of assertions, those > >>in the Tbox are cast in stone and cannot be altered, whereas those > >>in the Abox are mere data, which if they seem to contradict those > >>in the Tbox must be faulty. > > > >Hum. > >If one consider the use of these terms in description logics, this > >is a bit more precise. The TBox defines a terminology, i.e. assign > >terms (which are interpreted as sets) to names, while the ABox > >asserts formulas generally about individuals. > > That is often said, but it doesn't make strict logical sense. There > is no model-theoretic notion of 'defines a terminology'; every > assertion made using a terminology constrains the set of satisfying > models in the same way, whether it is classified as a 'definition' or > an 'assertion'. In any case, those ABox formulas 'about' individuals > use set names as well, so they are just as much 'about' the sets as > the statements in the TBox are; and there is no clear distinction > between statements about sets and statements which quantify over > individuals; eg A intersects B is equivalent to (exists (?x)(?x in A > and ?x in B)). So the only difference here seems to be that the ABox > is allowed to refer to individuals by name while the TBox isn't; but > since any name can be replaced by an existential quantifier, that > doesn't seem to amount to anything either. The DL distinction between Tbox and Abox has changed over the years. In the days when reasoning algorithms where less well understood, the split was more or less into that part of the KB for which (something like) sound and complete (subsumption) reasoning could be performed (the Tbox) and the part for which it could not (the Abox). Nowadays, the distinction is simply the type of axioms: the Tbox consists of (class) concept inclusion axioms (and/or equivalence) - e.g., "C subsumes D" while the Abox consists of individual/tuple membership axioms - e.g., "x is an instance of C" or "<x,y> is an instance of R". For most DLs this is a useful distinction as a simpler algorithm can be used for reasoning with a Tbox alone (no individual names). In the older style DLs mentioned above (e.g., Classic), Tbox axioms are often called "Definitions" because they are restricted to being unique acyclic name introductions, i.e., little more than macros that can be expanded in such a way that the Tbox becomes irrelevant, and all subsumption questions can be answered by a simple algorithm that makes no reference to the Tbox. Even today, where Tboxes are assumed to contain arbitrary inclusion axioms, it is useful in practice to divide the Tbox into a set of "definition" axioms and the remaining "general" axioms, which set is made as small as possible by applying a rewriting optimisation known as absorption. Tableaux algorithms can then exploit the definitional part of the Tbox by using a lazy expansion technique. (see Horrocks and Tobies, "Reasoning with Axioms: Theory and Practice", KR-2000). > >The ABox can use the names assigned in the TBox, while the TBox > >usually do not refer to those interpreted as individuals in the ABox > >(but this is evolving). > >This meets the mathematical delimitation between definitions and > >assertions (no?!). It is true that some recently described DLs include "nominals" (individuals/extensionally defined concepts). In this case the Tbox/Abox distinction is meaningless: it is easy to capture old style Abox membership axioms with concept inclusion axioms. > As far as I know, there is no *mathematical* way to distinguish > definitions and assertions. The distinction seems to be more one of > attitude than of mathematics: if you find a contradiction in the > definitions, you say there is an error, or that something is wrong > with the model; if you find a contradiction in the assertions, you > just say that some of the facts are wrong; if you find a > contradiction between them, you change the assertions rather than the > definitions. Its like the difference between a plant and a weed, > which is central in gardening, but meaningless in botany. (Logic is > like botany.) > > Another way of putting it is that a definition is an assertion which > is *not allowed* to be false, by fiat. (This is what makes > definitions potentially dangerous, by the way, since this unbending > refusal to be false can produce paradoxes, a la Russell.) > > The way you characterise it in terms of TBox defining 'set' > terminology and the ABox describing 'individual' facts is > interesting, but doesnt seem to me to capture the basic idea fully, > for several reasons. First, individual names can be defined as well > as set names; second, it doesnt capture the fact that enough > individual facts can contradict some set-terminology definitions (eg > suppose S is defined in the TBox to be a class with at most two > members, and then in the ABox we are told that c, d and e are all > distinct and all in S.) Actually, in most DLs it is impossible to fix a non-zero upper bound on the cardinality of a concept. (This would be true in DAML+OIL if it were not for the ONE-OF constructor, which is equivalent to nominals.) So without an Abox it is impossible e.g., to have an unsatisfiable KB (as the empty domain is always a model) or to assert non-subsumption. > >Logically this can be cleanly defined by separating the languages. > >In model theoretic terms, this means that all terms are interpreted > >as sets (and all assertions can be reduced to inclusion between > >these sets). > >There is an important consequence on that separation (that held at > >least in first DL languages): the terminology itself cannot be found > >inconsistent. This is because, it only deals with sets (e.g. the set > >of things with more than four legs and less than two legs) and the > >worst that can happen to them is to be empty (but having a whole > >theory about plenty of empty sets is not inconsistent). > > One can say contradictory things about sets, though, just as easily > as one can say them about individuals. (Proof sketch: take a > contradiction about individuals and replace every individual by its > singleton set plus an assertion that it is nonempty.) See above - without an Abox (or nominals) there is no way to assert that the interpretation of a concept is nonempty. Even with an Abox there is no way to assert that it is a singleton. Nominals do however add the possibility of fixing the cardinality of a concept (or in some cases even of the interpretation domain). > >On the contrary the ABox can be inconsistent, just because it > >asserts things (e.g. that there exists something with four legs > >belonging to the set of things with at most three legs). > > Well, that is the same as saying that those sets have a nonempty > intersection, which can be said entirely in set-talk. Not in a standard Tbox. > >Nowadays, the terminologies are rather theories like you noted with > >assertions of equivalence (or subsumption) between terms (e.g. the > >set of individual with more than four legs is equivalent to the set > >of individuals with less that two legs). One could prove that no > >element belonging to the first set can belong to the second one and > >vice versa. But this does not make the theory inconsistent because > >it has at least one model: the one in which no individual exists (in > >that model both sets are empty and indeed equivalent). > > > >If I am not wrong, the ONE-OF construct in DAML-OIL does only break > >the rule that the TBox cannot talk about individual terms. > > I wasnt aware that DAML used the TBox/ABox distinction. I think Jerome is right. Without the ONE-OF construct, DAML+OIL could be seen as a Tbox with "raw" RDF acting as an Abox. > >But it still does not assert anything about the considered > >individual terms (because all assertions are in the context of a > >term and if that term is interpreted as the empty set, nothing can > >be said about the considered individual terms). > > > >Moreover, even the TBox cast-in-iron statement can be challenged. If > >I remember Nebel's thesis, he used the terms Terminology for TBox > >and World description for ABox. This clearly seems to denote the > >opposite standpoint: if the terminology cannot account correctly for > >the world description then, this is the Terminology which will be > >wrong. > >But this is not a definitive position: one can take one view or > >another depending of the considered application (or depending if > >(s)he is platonist or aristotlelist, for using the big words). The > >view presented by Pat is more rigorous since a world description can > >be inconsistent in itself (without Terminology) while the > >Terminology cannot. > > Well, it *can*, logically; but the TBox rules require that it shall > never be so, rather in the way that a church defines itself to be > hallowed ground. As I said above, I think that the old distinctions were in reality pragmatic rather than anything else, even if this pragmatism was seasoned with a little philosophy. IanReceived on Sunday, 17 June 2001 18:11:44 UTC

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