I tried to say that P55(x,y) ⇐ (∃z) [ [E9(z) ˄ P25i(x,z) ˄ P26(z,y)] ˄ ¬ (∃w) [E9(w) ˄ P25i(x,w) ˄ P27(w,y)˄ P182(z,w)]]
is not sufficient since the above implication is true if the premise is false. So if there exist a newer move ( (∃w) [E9(w) ˄ P25i(x,w) ˄ P27(w,y)˄ P182(z,w)]] is true) it is consistent with P55(x,y). The question is what should the additional axiom be ? The following is too strong since we do not require knowledge about a move P55(x,y) ⇒ (∃z) [ [E9(z) ˄ P25i(x,z) ˄ P26(z,y)] ˄ ¬ (∃w) [E9(w) ˄ P25i(x,w) ˄ P27(w,y)˄ P182(z,w)]] That was what I thought. Best, Christian-Emil ________________________________ From: Wolfgang Schmidle <wolfgang.schmi...@uni-koeln.de> Sent: 18 October 2022 17:47 To: Christian-Emil Smith Ore Cc: crm-sig@ics.forth.gr Subject: Re: [Crm-sig] Deducing the current custody / ownership / location Dear Christian-Emil, I am not sure I understand your additional axiom. How would it be expressed in normal language? Are you saying "if the knowledge base knows that x has current location y and that were was at least one Move of x, then there must be a Move of x to y after which there is no more Move of x away from y"? Best, Wolfgang > Am 17.10.2022 um 16:04 schrieb Christian-Emil Smith Ore via Crm-sig > <crm-sig@ics.forth.gr>: > > Dear Wolfgang, > It is clear (at least to me) that the FOLs in the 'current' properties are > too weak. A complicating factor is that the FOL describes what we explicitly > know, that is, the status in the knowledge system. In a closed world system, > all shortcuts will imply at least one instance of the corresponding long > path. This is not the case in an open world view, I think. > > P55(x,y) ⇐ (∃z) [ [E9(z) ˄ P25i(x,z) ˄ P26(z,y)] > ˄ ¬ (∃w) [E9(w) ˄ P25i(x,w) ˄ P27(w,y)˄ > P182(z,w)]] > > If the premise in the FOL above is false, then P55(x,y) is trivially true. > This is ok if [E9(z) ˄ P25i(x,z) ˄ P26(z,y)] is false, but it is not ok if > (∃z) [ [E9(z) ˄ P25i(x,z) ˄ P26(z,y)] ˄ (∃w) [E9(w) ˄ P25i(x,w) ˄ P27(w,y)˄ > P182(z,w)]] > is true. > > We need an additional axiom, something like > (∃z) [P55(x,y) ˄ [E9(z) ˄ P25i(x,z) ˄ P26(z,y)] ⇒ ¬ (∃w) [E9(w) ˄P25i(x,w) > ˄ P27(w,y)˄ P182(z,w)]]] > ? > Best, > Christian-Emil > > From: Crm-sig <crm-sig-boun...@ics.forth.gr> on behalf of Wolfgang Schmidle > via Crm-sig <crm-sig@ics.forth.gr> > Sent: 16 October 2022 14:37 > To: crm-sig@ics.forth.gr > Subject: [Crm-sig] Deducing the current custody / ownership / location > > Dear All, > > I am trying to understand how one can infer the current custody / ownership / > location of a Physical Thing / Object. > > Let's assume that there has been a E10 Transfer of Custody / E8 Acquisition / > E9 Move to an Actor or Place y. If there was no later event at all, it is > inferred in the scope notes of P50 has current keeper / P52 has current owner > / P55 has current location that y is, in fact, the current keeper / owner / > location. For example, the scope note of "P52 has current owner" says: "This > property is a shortcut for the more detailed path from E18 Physical Thing > through P24i changed ownership through, E8 Acquisition, P22 transferred title > to to E39 Actor, if and only if this acquisition event is the most recent." > > There is a stronger-sounding but actually weaker requirement that there was > no later event that included a "P28 custody surrendered by / P23 transferred > title from / P27 moved from" y. The owner / location scope notes use the > stronger requirement, the keeper scope note uses the weaker requirement. It > would be good to explain in the respective scope notes the reasoning behind > this difference. > > The FOL encodes the weaker requirement in all three cases. I assume the > discrepancy between scope notes and FOL is an oversight. (This was actually > my starting point.) > > The scope notes not only say "if" but "if and only if". Is there a way to > encode the "only if" part in FOL? This seems to be quite tricky. For example, > if there were three Moves: 1. from somewhere to A, 2. from A to B, 3. from B > back to A, then one can infer that A is the current location, but only Move 3 > (and not Move 1) is actually the long form of the shortcut "P55 has current > location". On the other hand, it does not follow from Move 1 and 2 that A is > not the current location. > > Should we worry about negative statements and incomplete knowledge in our > knowledge base? Or do we assume here that if there has been such an event, > then the knowledge base knows about it? (Or equivalently, if the knowledge > base does not know of any such event, then there was indeed none?) Of course > one can infer e.g. the current location based on a possibly incomplete list > of Moves in a given knowledge base, but whose opinion would it represent? Can > one still claim that the inferred statement is the opinion of the knowledge > base maintainers? > > In particular, what happens if an object disappears or gets destroyed? One > may infer the last keeper / owner / location before the destruction, but both > the scope notes and the FOL will happily argue that the destroyed object > nonetheless has a current owner / keeper / location. Perhaps the destruction > implies an implicit Transfer Of Custody where the custody has been > surrendered, but there is probably no implicit Acquisition or Move. E64 End > of Existence and E6 Destruction offer no concrete help, although E64 says: > "It may be used for temporal reasoning about things … ceasing to exist". > > I assume this has already been discussed somewhere, but the discussion didn't > find its way into the scope notes. > > Best, > Wolfgang > > > _______________________________________________ > Crm-sig mailing list > Crm-sig@ics.forth.gr > http://lists.ics.forth.gr/mailman/listinfo/crm-sig > _______________________________________________ > Crm-sig mailing list > Crm-sig@ics.forth.gr > http://lists.ics.forth.gr/mailman/listinfo/crm-sig
_______________________________________________ Crm-sig mailing list Crm-sig@ics.forth.gr http://lists.ics.forth.gr/mailman/listinfo/crm-sig