From: Christian De Sainte Marie <csma@fr.ibm.com>

Date: Mon, 9 Jul 2012 17:54:04 +0200

To: Jesse Weaver <weavej3@rpi.edu>

Cc: Adrian.Paschke@gmx.de, Ankesh <ankesh@cs.rpi.edu>, cawelty@gmail.com, public-rif-wg@w3.org, sandro@w3.org, team-rif-chairs@w3.org

Message-ID: <OF6538E5F9.5F83353C-ONC1257A33.004114FC-C1257A36.00575C8F@fr.ibm.com>

Date: Mon, 9 Jul 2012 17:54:04 +0200

To: Jesse Weaver <weavej3@rpi.edu>

Cc: Adrian.Paschke@gmx.de, Ankesh <ankesh@cs.rpi.edu>, cawelty@gmail.com, public-rif-wg@w3.org, sandro@w3.org, team-rif-chairs@w3.org

Message-ID: <OF6538E5F9.5F83353C-ONC1257A33.004114FC-C1257A36.00575C8F@fr.ibm.com>

Hi Jesse, The semantics of equality formulas, in PRD, is not specified wrt a state of the fact base, but wrt the value of the terms on both side of the equality: t1 = t2 iff sigma(t1) and sigma(t2) have the same value. So, no need for equality facts, and no problem with transitivity, symetry or reflexivity. The case of lists is missing, though (since uninterpreted (logically defined) terms are not allowed in RIF-PRD, a ground term either has an atomic value or it is a ground list): I believe this is oversight, and the intent was that ground lists List(a1...an) = List(b1..bm) iff n=m and Ai=bi for all i. I will propose a correction/clarification in the 2nd edition. Cheers, Christian IBM 9 rue de Verdun 94253 - Gentilly cedex - FRANCE Tel./Fax: +33 1 49 08 29 81 From: Jesse Weaver <weavej3@rpi.edu> To: team-rif-chairs@w3.org Cc: cawelty@gmail.com, Christian De Sainte Marie/France/IBM@IBMFR, sandro@w3.org, Ankesh <ankesh@cs.rpi.edu>, public-rif-wg@w3.org, Adrian.Paschke@gmx.de Date: 05/07/2012 21:22 Subject: Apparent inconsistency regarding equality in RIF-PRD RIF Chairs, In short, if a=b and b=c, then intuitively, it should hold that a=c, but the operational semantics do not seem to ensure such. By definition of atomic formula (section 2.1.2) and informal definition of fact (section 2.2.2), a set of facts may include ground, equality, atomic formulas. Consider then the following set of facts where t_1, t_2, and t_3 are different ground terms: \Phi = {t_1=t_2, t_2=t_3}. By (operational) definition of state of the fact base (section 2.2.2), \Phi represents a state of the fact base. According to the interpretation of condition formulas (section 12.2), I_{truth}(I(x=y)) iff I(x)=I(y). Intuitively, then, it should hold that since t_1=t_2 \in \Phi implies I(t_1)=I(t_2), and since t_2=t_3 \in \Phi implies I(t_2)=I(t_3), by transitivity of mathematical equality, I(t_1)=I(t_3). However, there exists no ground substitution that matches t_1=t_3 to \Phi, and since ground, equality, atomic formulas cannot be inferred by rules (they are not syntactically allowed as the target of an assert action; see definition of atomic action, section 3.1.1), then there is also no subsequent state in which there exists a ground substitution that matches t_1=t_3 to the state's associated set of facts. This seems like an inconsistency. A similar argument can be made for the simpler (but perhaps less interesting and less obvious) case of when \Phi = {t_1=t_2}, where t_1 and t_2 are different ground terms. Then no ground substitution exists that matches t_2=t_1 to \Phi or to any subsequently inferred sets of facts. I can think of a number of ways to resolve this apparent inconsistency, but I wish to know: have I correctly determined an inconsistency, and if so, what were the intended (consistent) semantics (or definitions)? Jesse Weaver Ph.D. Student, Patroon Fellow Tetherless World Constellation Rensselaer Polytechnic Institute http://www.cs.rpi.edu/~weavej3/index.xhtml Sauf indication contraire ci-dessus:/ Unless stated otherwise above: Compagnie IBM France Siège Social : 17 avenue de l'Europe, 92275 Bois-Colombes Cedex RCS Nanterre 552 118 465 Forme Sociale : S.A.S. Capital Social : 645.605.931,30 ? SIREN/SIRET : 552 118 465 03644 - Code NAF 6202AReceived on Monday, 9 July 2012 15:54:58 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 9 July 2012 15:54:59 GMT
*