T&A Boxes (was: RE: rdf as a base for other languages)

>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 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?!).

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

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

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

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

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

Pat

---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Tuesday, 12 June 2001 11:48:11 UTC