Subject: [sv-ac] negate rhs of implication
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Mar 06 2003 - 09:10:27 PST
All:
As the freeze is on, here is another issue I would like to
raise.
The (unclocked) semantics for implication is as follows:
w |= r => s
iff
for every j >= 0 such that w^{0,j} |== r, there exists
k >= j such that w^{j,k} |== s.
If we negate this, we get
w |= not(r => s)
iff
there exists j >= 0 such that w^{0,j} |== r and
for all k >= j, not(w^{j,k} |== s).
It has been argued that this semantics is not as useful
as
for every j >= 0 such that w^{0,j} |== r, for every
k >= j, not(w^{j,k} |== s),
which corresponds to the syntax
w |= r => (not s).
Therefore, I would like to raise as issue for consideration
that we allow negation of the rhs of an implication.
Notice that if negation of rhs is allowed, then there
is typically no need to write something like "not(r => (not s))",
since
w |= not(r => (not s))
iff there exists j >= 0 such that w^{0,j} |== r
and there exists k >= j such that w^{k,j} |== s
which is usually equivalent to
w |= r ;[0] s
Best regards,
John Havlicek
This archive was generated by hypermail 2b28 : Thu Mar 06 2003 - 09:11:19 PST