- From: Pat Hayes <phayes@ihmc.us>
- Date: Mon, 12 Nov 2007 09:46:00 -0600
- To: "Michael Schneider" <schneid@fzi.de>
- Cc: "Owl Dev" <public-owl-dev@w3.org>, <alanruttenberg@gmail.com>
>Hi Pat! Hi Michael > >Pat Hayes wrote on Saturday, November 10: > >>>OWL-DL-1.0 allows me to state that a class :C is the >>intersection of classes >>>:D1 and :D2. When I have to write such an axiom in RDF >>syntax, I generally >>>do it by means of Turtle in the following way: >>> >>> (1) :C a owl:Class . >>> (2) :D1 a owl:Class . >>> (3) :D2 a owl:Class . >>> (4) :C owl:equivalentClass [ a owl:Class ; >>> owl:intersectionOf ( :D1 :D2 ) >>> ]. >>> >>>where (4) is just a convenient Turtle shortcut for writing >>> >>> (4a) _:X a owl:Class . >>> (4b) :C owl:equivalentClass _:X . >>> (4c) _:X owl:intersectionOf ( :D1 :D2 ) . >>> >>>So we actually have a bNode "_:X" in our OWL-DL-1.0 ontology above. >> >>Note however that you could have done a >>translation with a URIref instead of a bnode > >Yes, this really seems to be an alternative. It took me a while to consider, >whether this is really ok from a semantical point of view (not just a >syntactical trick), but I am now pretty convinced. You might want to check >my considerations: > >The bNode says, that there exists /some/ resource, but I do not know which >one. But because it is sure that there /is/ at least one such resource, I >should be allowed to "capture" this unknown resource by introducing some new >(i.e. not used elsewhere) URI ':Y' , which denotes this unknown resource. > >To see this, let's assume that we have a model M for the graph G, which >contains the bNode '_:X'. And let's further assume that G' is the new graph, >in which the bNode '_:X' has been replaced by the URI ':Y'. Then I can use >the model M as a starting point to build all possible interpretations M'_i, >wherein URI ':Y' denotes some resource r_i of the universe. Two different >interpretations M'_i interprete ':Y' by two different resource r_i in the >universe, and for each such resource r_i there is some coresponding >interpretation M'_i. I all other aspects, the interpretations M'_i equal the >original model M. Under these conditions, at least one of all these >interpretations M'_i must be a model for G', because in one of these >interpretations the URI ':Y' will denote a "correct" resource (we know that >there exists one such resource, and I tried them all!). So this means that >for every model for G there is a coresponding model for G', which is >"approximately equivalent" to G. > >The URI ':Y' must of course really be new. If I take an URI which is already >in use elsewhere, then there are already restrictions on this URI given by >class assertions and properties assigned to this URI. Now, when I denote >':Y' by one of the correct resources (one of the resources which exist >acording to the bNode in G), then it might happen that such an >interpretation becomes un-true due to the restrictions existing on the >chosen URI. And in the worst case it may happen that we do not find any >"approximatly equivalent" model for G'. > >>(invent some random "skolem" URI for the purpose) > >Erm, can you please explain this term to me? Certainly. It comes from the dark ages of resolution theorem-proving. Part of the process of putting sentences into clausal normal form involves eliminating any existential quantifiers (since all variables in clauses are universal). This is (was?) done by replacing any existential occurring inside some universals binding variables x1,...xn by a function applied to those universal variables, called a Skolem function (often written skolem). So for example (forall (x) (and (P a x)(forall (y)(or (Q x y) (exists (z)(R z)))))) gives the two clauses (P a x) (Q x y)(R (f x y)) where f is a skolem function. A skolem constant is just a skolem function with no arguments, which corresponds to a 'plain' existential outside any universals. If A is a sentence and B is its skolemization, then A and B are not FO equivalent, but they have the property that (A entails C) iff (B entails C) when C does not contain any of the skolem functions. So, in particular, one is consistent iff the other is. The argument you give above is a reprise of the standard proof. One observation that isn't often made is that if we think of skolemization in classical 2nd-order logic, and treat the skolem function itself as existentially bound, then the two are exactly logically equivalent: (forall (x) (and (P a x)(forall (y)(or (Q x y) (exists (z)(R z)))))) |=2=| (exists (f) (forall (x) (and (P a x)(forall (y)(or (Q x y) (R (f x y))))))) >I have seen several people >using this term in the WG list recently, but I have never heard about it >before. In Wikipedia I just found some "Skolem Normal Form" (also new to >me), but I do not see whether this has something to do with our discussion >here. See above. > >>>Now OWL-DL-1.0 has both a "direct semantics" and an "RDF compatible >>>semantics", and for the DL sublanguage of OWL-1.0 they are >>intended to be >>>equivalent. This allows me to interprete the above OWL-DL-1.0 >>ontology by >>>using RDF compatible OWL-DL semantics. And because bNodes are >>interpreted in >>>RDF as /existential variables/, the meaning of axiom (4) is >>(in natural >>>language): >>> >>> "There exists some class ?X, >>> to which class :C is equivalent, > >> and which is the intersection of the classes :D1 and :D2." >>> >>>So this statement is actually a quantification about a >>/class/ variable. But > >>I thought that OWL-DL was a First Order Logic dialect, where > >all universal >>>and existential quantifications must be asserted about /individual/ >>>variables only? >> >>Well, just for clarification, OWL-Full and RDFS >>are also first-order, > >Ah, I never thought about this for OWL-Full (well, I have just started to >think a bit more deeply about OWL-Full), but after a few considerations >about the existing constructs in OWL (property restrictions, sub class >relationships, etc.) it looks plausible to me that even OWL-Full is a first >order system. Interesting! For translation of all the OWLs into CL, see http://www.ihmc.us/users/phayes/CL/SW2SCL.html and http://philebus.tamu.edu/cmenzel/Papers/AxiomaticSemantics.pdf > >>but allow quantification >>over classes. > >Hm, this second part of your statement confuses me. As a test of my >understanding of this situation, shouldn't one better say: > > "but allow quantification about individuals, > which may also be used as classes (i.e. class extensions) > or properties in the same ontology." > >? Modify that to "which may also BE classes.." and its saying the exact same thing I said. Notice Im not identifying classes with sets: this identification is unique to OWL-DL and is not done in RDFS or OWL-Full or Common Logic. Its important not to think of "individual" as a taxonomic classifier. In Tarskian semantics, "individual" just means something in the universe. A first-order universe can contain ANYTHING. > I do not see any constructs in OWL which really allow me to quantify about >classes (except via bNodes in RDF style ontologies). Well, in OWL-Full, a class may contain classes. So suppose A and B are classes containing classes, and you say that A is a subclass of B. Then you have made a quantified statement about classes, in effect. (At any rate, that is what you get if you translate this back into quantified logic.) > As I understand it, an >example for a higher order statement would be something like > > FORALL C1 C2: EquivalentClasses(C1 C2) ==> SubClassOf(C1 C2) > >This is actually a built-in rule in OWL, but I have no means to explicitly >express such a rule within an OWL-Full ontology. owl:EquivalentClasses owl:subPropertyOf owl:SubClassOf . > /This/ would really be >quantification about classes, but I do not see that OWL-Full allows me to do >such a kind of higher-order quantification in any form. > >>One can quantify over >>reasonably-sized universes of classes (or indeed >>anything else) in first-order frameworks. > >This confuses me even more, because I thought that it is the distinguishing >property of first order systems to exclusively allow quantification about >individuals? Well, yes, but that is vacuous, since "individual" in FO model theory simply means "things you are quantifying over". But there is nothing in the classical statement of FO model theory which prevents these things being of any particular kind: they can be sets (class extensions), or sets of tuples (relational extensions) or anything else. Exactly what makes a logic or theory "first-order" has been investigated, and there is a lovely result: its first-order iff it satisfies the Compactness and downward Loewenheim-Skolem lemmas. Less technically, iff both of: (1) if S entails A then some finite subset of S entails A (2) if A is satisfiable then it has a countable model Modify 'countable' in (2) to 'finite', the finite model property, and you get a characterization of the decideable fragments of FO logic, including DLs. >Well you will certainly know better, perhaps there are >sometimes ways to map class quantifications to equivalent individual >quantifications, so this requirement can be relaxed somewhat, is it this? No. Its deeper than this. Take some sentence of ordinary FO logic, say (forall (x)(if (P x)(Q x)) and ask, what does the quantifier range over? And the correct answer is, whatever is in the universe of discourse. And then ask, what kind of things can be in such a universe? and the correct answer is, ANYTHING at all. There are *no* restrictions on the nature of things in a FO universe of quantification. In particular, one classical FO theory might quantify over the relations (classes and properties) in another FO theory. The classical FO semantic theory allows this. What it conventionally does not allow is to have these two theories merged into one theory: it conventionally forbids using the same name in a single theory to denote both individuals and relations. But this is an essentially syntactic restriction, not a semantic one; and it can be removed without doing any essential damage to either the syntax, the proof theory or the semantics of FO logic. The result is what is now called ISO Common Logic. >But I won't ask you for further explanation of this, because this would >certainly go too far in this thread. > >>(What >>one cannot quantify over is the set of all >>mathematically definable classes, but nobody >>wants to do that.) >> >>But your point can still be made, since OWL-DL is >>a *segregated* first-order language which does >>not permit individuals and classes to be >>intermixed, and prohibits quantification over the >>latter. But see below. >> >>>And in an RDF-mapped OWL-DL-1.0 ontology, I am not allowed >>>to regard such a class variable as an individual variable, >>because in OWL-DL >>>the OWL universe is strictly separated. >> >>True, but what is the problem? That variable only >>arises in the RDF translation: it is not a >>variable in OWL-DL itself. The direct semantic >>meaning of the intersection statement is clear, >>and mentions three classes. The RDF meaning of >>the OWL/RDF is also clear, and also mentions (the >>same) three classes, but uses two names (the URI >>":C" and the bnode) to refer to one of them. So? >>The fact that the RDF uses a name in a way that >>is syntactically prohibited in the DL says >>nothing about their semantic equivalence. > >I am not sure if I understand this. Does your argumentation go in the >direction that the "intended" axiom > > "Class :C is equivalent to > the intersection of the classes :D1 and :D2" > >is equivalent to the existentially quantified formulation > > "There exists some class ?X, > to which class :C is equivalent, > and which is the intersection of the classes :D1 and :D2." > >? So in this case the existential quantification does no harm, because it is >"fully backed" by the other - equivalent - formulation, which does not >contain any bNode. Is this the idea? This would at least sound reasonable to >me, but perhaps you mean something different. Well, all that is true, but it isn't what I meant here. It would do no harm in any case. Your observation which started this thread noted that one of the OWL-DL semantic conditions, when translated into conventional logic (or into RDF, but thats not really important) involves what appears to be a non-first-order quantification. OK, so maybe its really first-order after all: but in any case, so what? Even if it were really non-FO, that does not itself make OWL-DL non-FO. Take conventional FOL and look at a statement of the truth conditions for the universal quantifier. That involves a second-order quantification, but that fact does not in itself make FOL second-order. In OWL/RDF there are two distinct languages involved: RDF and its semantics, and OWL and its semantics. The extra semantic constraints which make OWL/RDF equivalent to 'abstract' OWL are conditions which when added to the RDF semantics, produce truth-conditions which are equivalent (on the OWL-DL-syntactically legal subcase) to the abstract semantics. Nothing in that says that these extra conditions have to be stated in any particular (FO or SO) 'style' in order for the language being defined to be of any particular class. Pat > >>Pat > >Well, you see, a lot of questions and difficulties in understanding on my >side. It turns out that I am just starting to learn the basics of OWL. :-) > >Regards, >Michael > >-- >Dipl.-Inform. Michael Schneider >FZI Forschungszentrum Informatik Karlsruhe >Abtl. Information Process Engineering (IPE) >Tel : +49-721-9654-726 >Fax : +49-721-9654-727 >Email: Michael.Schneider@fzi.de >Web : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555 > >FZI Forschungszentrum Informatik an der Universität Karlsruhe >Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe >Tel.: +49-721-9654-0, Fax: +49-721-9654-959 >Stiftung des bürgerlichen Rechts >Az: 14-0563.1 Regierungspräsidium Karlsruhe >Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi Studer >Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus -- --------------------------------------------------------------------- IHMC (850)434 8903 or (650)494 3973 home 40 South Alcaniz St. (850)202 4416 office Pensacola (850)202 4440 fax FL 32502 (850)291 0667 cell phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes
Received on Monday, 12 November 2007 15:46:18 UTC