Re: Apparent inconsistency regarding equality in RIF-PRD

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 6202A