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
