Re: RDF Semantics: corrections(was: Re: RDF Semantics: two issues, connected to OWL)

[Pat, I'm cc'ing www-archive as it's easier that way to point back]


>>>  Im a bit puzzled by it. You say:
>>>  "I am not expressing an inconsistency derivation as
>>>  {graph} => { } as we can't constructively prove false.
>>>  Instead I express it as
>>>  {graph} => {F1 log:inconsistentWith F2}"
>>>
>>>  but what are F1 and F2? Why would saying they are
>>>  inconsistent with one another constitute a contradiction?
>>>
>>>  AmI missing some earlier assumptions?
>>
>> Possibly (I'm always too implicit; always...)
>>
>> Let's take an example
>>
>> Assume we have a machine which we observe
>> and we collect following facts.n3
>>
>> ###
>> :machine022 a :ptMachine.
>> :machine022 :vmVersion 1.305.
>> ###
>>
>> Assume also that we have an assumed recommendation rec.n3
>>
>> ###
>> {?X a :ptMachine} => {?X :vmVersion 1.4}.
>>
>> # @@ inconsistency detection
>> {?X a :ptMachine. ?X :vmVersion ?V. ?V math:lessThan 1.4} =>
>>    {facts.log:semantics log:inconsistentWith rec.log:semantics}.
>> ###
>>
>> Then we can find
>>
>> ###
>>   {[iw:Variable "?X"; = :machine022] a :ptMachine.
>>    [iw:Variable "?X"; = :machine022] :vmVersion [iw:Variable "?V"; =
1.305].
>>    [iw:Variable "?V"; = 1.305] math:lessThan 1.4} =>
>> {facts.log:semantics log:inconsistentWith rec.log:semantics}.
>> ###
>>
>> So either facts.n3 is false or rec.n3 is false
>> but we don't say which one.
>> In a practical case we will upgrade that machine
>> and then collect
>>
>> ###
>> :machine022 a :ptMachine.
>> :machine022 :vmVersion 1.4.
>> ###
>>
>> and don't detect that inconsistency anymore :)
>>
>>
>> In general we try to prove which (sub)graphs
>> are inconsistent with which other (sub)graphs
>> and just show the evidence for that (could
>> be quite complicated proof trees...)
>
> Ah, I see. Yes, this will get to be complicated.
> Part of the complication arises because you are
> allowing sentence to refer to sets of other
> sentences, which takes us outside normal logical
> territory to the place where paradoxes lurk.

That's right; we indeed start with the assumption
that A is the case and that B is the case
and then arrive at a conclusion that their
conjunction is not the case...

> Not sure what I can say about this. One
> observation is that if A and B are each
> consistent but (A & B) is contradictory then A
> entails not-B and vice versa.

OK

> Was there a particular question you had that I
> can focus on?

Well, the backbround was an asking of your opinion
about the last message of last year in www-archive
http://lists.w3.org/Archives/Public/www-archive/2003Dec/0047.html
Is there an aternative way of *proving* inconsistencies ??
(our usage of log:inconsistentWith is what
euler uses for the OWL test cases and also
in some observer component that we test)


> (Sorry, the Xmas/NY break was a
> little hectic this year and may have erased some
> of my memory.)

:)

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Thursday, 15 January 2004 18:02:25 UTC