W3C home > Mailing lists > Public > public-rif-wg@w3.org > July 2012

Re: Apparent inconsistency regarding equality in RIF-PRD

From: Christian De Sainte Marie <csma@fr.ibm.com>
Date: Fri, 6 Jul 2012 11:14:10 +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: <OF847F15FF.3E34ED4A-ONC1257A33.0031E4E2-C1257A33.0032BFC0@fr.ibm.com>
Hi Jesse,

Thanx for the feedback (which could not be more appropriately timed: 
indeed, we are preparing a revised edition to correct the errors found in 
the first edition :-)

I will examine the three problems that you have found re equality, 
subclasses and action variables and let you know.



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, 
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 

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

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 6202A 
Received on Friday, 6 July 2012 09:15:00 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:48:00 UTC