- From: Bijan Parsia <bparsia@cs.man.ac.uk>
- Date: Wed, 3 Oct 2007 19:22:10 +0100
- To: Matthew Pocock <matthew.pocock@ncl.ac.uk>
- Cc: ewallace@cme.nist.gov, public-owl-dev@w3.org
On 3 Oct 2007, at 18:12, Matthew Pocock wrote: > On Wednesday 03 October 2007, Bijan Parsia wrote: >> Quick check reveals to me that you got why more elaborate key >> reasoning is hard (i.e., why we don't want to have to work with >> unnamed individuals or unknown key values and restrictions on key >> properties). I took Evan to be asking about why we can't have "check" >> semantics for keys (i.e., missing keys are a violation). > > Ah, my bad. No worries. > So - is the "check" semantics equivalent to raising "inconsistent" > if the values of the key for all relevant individuals are not > entailed by the > ontology? No. At least, I don't think so. Here, the check is *whether* you have a *known* key. The kind of thing you can express with the K and A operators. > That is, given an ontology o, some individual i, a key k, and a > value v (all in the interpretation of o), > > i in (k some Thing) => exists v s.t. o |= k(i, v) Oh, I see. The issue would be that it has to be the *same* v in all models. I.e., if i k (4 or 5), then there's one model where it's 4 and one where it's 5. So it has *a* key in all models, but you don't know what it is. (I'm confused whether v is a variable or a constant in your example, given the quantifier.) Even this is a little tendentious since I'm sorta working off an MKNFy account. When you have the ground abox statement i k v, obviously, in every model k contains the pair (i,v). Cheers, Bijan.
Received on Wednesday, 3 October 2007 18:21:15 UTC