From: Jos De_Roo <jos.deroo@agfa.com>

Date: Thu, 15 Jan 2004 23:58:35 +0100

To: "pat hayes <phayes" <phayes@ihmc.us>

Cc: www-archive@w3.org

Message-ID: <OFF8FAA52B.AC240F90-ONC1256E1C.006C6D55-C1256E1C.007E36CB@agfa.be>

Date: Thu, 15 Jan 2004 23:58:35 +0100

To: "pat hayes <phayes" <phayes@ihmc.us>

Cc: www-archive@w3.org

Message-ID: <OFF8FAA52B.AC240F90-ONC1256E1C.006C6D55-C1256E1C.007E36CB@agfa.be>

[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

*
This archive was generated by hypermail 2.4.0
: Friday, 17 January 2020 22:32:21 UTC
*