Re: ?s on operational semantics of atomic actions in RIF-PRD

Hi Ankesh,

Ankesh wrote, on Fri, 18 Mar 2011 16:49:37 -0400:
>
> The semantics of the Assert atomic action is described as follows at 
[1]:
>
> Rule 1 says that *all the condition formulas that were satisfied before 
an
> assertion will be satisfied after*, and that, in addition, the condition
> formulas that are satisfied by the asserted ground formula will be 
satisfied
> after the assertion. No other condition formula will be satisfied after 
the
> execution of the action.
>
> where, Rule 1 is formally defined as:
> ¦Á is Assert(¦Õ), where ¦Õ is a ground atomic formula, and *w' = w ¡È {¦Õ}*;
>
> I am guessing that "condition formulas" refers to formulas described at 
[2]..
> In that case an assertion could change the satisfaction of negation 
formula,
> right? ie. a negation formula may be satisfied in w but not in w'. Does 
this
> violate the description above. Kindly explain.
> 
> [1] 
http://www.w3.org/TR/rif-prd/#Operational_semantics_of_atomic_actions

> [2] http://www.w3.org/TR/rif-prd/#Formulas


You are perfectly right and the text explanation of the formal definition 
is wrong: it applies only to atomic condition formulas, not general ones.

We will correct the wording in the 2nd edition.

> (A similar argument follows for Rule 2)

Indeed.

> Furthermore, the formal definition doesn't mention conditional formula 
while
> the description (referred above) does. Is something missing there?

Nothing is really missing, but the formal definitions are not rigorous 
enough, as they confuse the states of the fact base and the sets of ground 
atomic formulas that represent them. This will be clarified in the revised 
edition.

Thanx for your comment.

Cheers,

Christian

IBM
9 rue de Verdun
94253 - Gentilly cedex - FRANCE
Tel./Fax: +33 1 49 08 29 81


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