Dear Carlo, If the scopenote text describe the a world or a model for the theory, it is true. More formalistic: If I add this second move to a knowledge base, then there are no formal way to detect that the knowledge base is inconsistent?
Best, Christian-Emil ________________________________ From: Crm-sig <crm-sig-boun...@ics.forth.gr> on behalf of Carlo Meghini via Crm-sig <crm-sig@ics.forth.gr> Sent: 19 October 2022 14:53 To: crm-sig@ics.forth.gr Subject: Re: [Crm-sig] ISSUE: shortcuts in P50 has current keeper, P52 has current owner, P55 has current location Dear Christian-Emil I don't think that the axiom contradicts the scopenote text. In those worlds where there is a move w taking x away from y and w is after z (so the antecedent is false), P55(x,y) (the consequent) is false as well but the axiom still holds. Carlo Il 19/10/22 13:23, Christian-Emil Smith Ore via Crm-sig ha scritto: In the scope notes of the "current" properties it is written that, say, P55 has current location, P55(x,y) is the case if and only if the physical object x is not moved from the place y at a later date than it was moved to y. Expressed in ordinary FOL (without any requirement of open world this will be 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 is, P55(x,y) if and only if there exists a move z such that x was moved to y in this move invent and it does not exist any other move event moving x away from y where the move event z ended before (or with) the start of the move event w. Under an open world view we do not postulate the existence of such a z or require that the knowledge base should contain information about such a (anonymous) event. Therefore the equivalence is weakened to P55(x,y) ⇐ (∃z) [ [E9(z) ˄ P25i(x,z) ˄ P26(z,y)] ˄ ¬ (∃w) [E9(w) ˄ P25i(x,w) ˄ P27(w,y)˄ P182(z,w)]] postulating the existence of the shortcut if there exists a move z such that x was moved to y in this move invent and it does not exist any other move event moving x away from y where the move event z ended before (or with) the start of the move event w. This implication is true also in the case the premise is false, that is, there exists a newer move event taking x away from y. Therefore our knowledge base will be consistent even in this case which contradicts the scopenote text. So that is why I suggested an additional weaker axiom: Ff the shortcut P55(x,y) exists and there is information about the move event moving x to y, then there cannot be information about any other move event moving x away from y at a later point in time. May be I am wrong. Best, Christian-Emil ________________________________ From: Crm-sig <crm-sig-boun...@ics.forth.gr><mailto:crm-sig-boun...@ics.forth.gr> on behalf of Wolfgang Schmidle via Crm-sig <crm-sig@ics.forth.gr><mailto:crm-sig@ics.forth.gr> Sent: 19 October 2022 07:48 To: crm-sig@ics.forth.gr<mailto:crm-sig@ics.forth.gr> Subject: [Crm-sig] ISSUE: shortcuts in P50 has current keeper, P52 has current owner, P55 has current location The shortcuts given in the scope notes / FOLs of P50 has current keeper, P52 has current owner, P55 has current location are wrong. It is unclear how to correct them, or if they can be corrected at all. > Am 18.10.2022 um 21:55 schrieb Martin Doerr via Crm-sig > <crm-sig@ics.forth.gr><mailto:crm-sig@ics.forth.gr>: > > Dear both, > > I think the discussion was that the "current" status cannot be inferred, but > it is based on a local "closed world" knowledge, and can only be "true" until > the time of the last respective update. So, I think the "no other move" since > time X, or "no other move without back move" since time X exceeds the scope > of logic. > Isn't it? > > I fear the "if and only if" statements are wrong anyway. Better you raise an > issue. I fear we have not understood circumstances that can lead to a custody > or loosing etc., including death, heirs etc. > > Best, > > Martin > > On 10/18/2022 7:44 PM, Christian-Emil Smith Ore via Crm-sig wrote: >> 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><mailto:wolfgang.schmi...@uni-koeln.de> >> Sent: 18 October 2022 17:47 >> To: Christian-Emil Smith Ore >> Cc: crm-sig@ics.forth.gr<mailto: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><mailto: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><mailto:crm-sig-boun...@ics.forth.gr> on >> > behalf of Wolfgang Schmidle via Crm-sig >> > <crm-sig@ics.forth.gr><mailto:crm-sig@ics.forth.gr> >> > Sent: 16 October 2022 14:37 >> > To: crm-sig@ics.forth.gr<mailto: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<mailto:Crm-sig@ics.forth.gr> >> > http://lists.ics.forth.gr/mailman/listinfo/crm-sig >> > _______________________________________________ >> > Crm-sig mailing list >> > Crm-sig@ics.forth.gr<mailto:Crm-sig@ics.forth.gr> >> > http://lists.ics.forth.gr/mailman/listinfo/crm-sig >> >> >> >> _______________________________________________ >> Crm-sig mailing list >> >> Crm-sig@ics.forth.gr<mailto:Crm-sig@ics.forth.gr> >> http://lists.ics.forth.gr/mailman/listinfo/crm-sig > > > -- > ------------------------------------ > Dr. Martin Doerr > > Honorary Head of the > Center for Cultural Informatics > > Information Systems Laboratory > Institute of Computer Science > Foundation for Research and Technology - Hellas (FORTH) > > N.Plastira 100, Vassilika Vouton, > GR70013 Heraklion,Crete,Greece > > Vox:+30(2810)391625 > Email: > mar...@ics.forth.gr<mailto:mar...@ics.forth.gr> > > Web-site: > http://www.ics.forth.gr/isl > _______________________________________________ > Crm-sig mailing list > Crm-sig@ics.forth.gr<mailto:Crm-sig@ics.forth.gr> > http://lists.ics.forth.gr/mailman/listinfo/crm-sig _______________________________________________ Crm-sig mailing list Crm-sig@ics.forth.gr<mailto:Crm-sig@ics.forth.gr> http://lists.ics.forth.gr/mailman/listinfo/crm-sig _______________________________________________ Crm-sig mailing list Crm-sig@ics.forth.gr<mailto:Crm-sig@ics.forth.gr> http://lists.ics.forth.gr/mailman/listinfo/crm-sig -- Carlo Meghini Istituto di Scienza e Tecnologie dell'Informazione [ISTI] Consiglio Nazionale delle Ricerche [CNR] Area della Ricerca di Pisa Via G. Moruzzi 1, 56124 Pisa
_______________________________________________ Crm-sig mailing list Crm-sig@ics.forth.gr http://lists.ics.forth.gr/mailman/listinfo/crm-sig
