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

Hi,

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.

(A similar argument follows for Rule 2)

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

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

thanks,
ankesh

Received on Monday, 21 March 2011 08:30:18 UTC