Subject: RE: [sv-ac] negate rhs of implication
From: Armoni, Roy (roy.armoni@intel.com)
Date: Thu Mar 06 2003 - 09:43:00 PST
I would like to second John's proposal.
Roy
-----Original Message-----
From: John Havlicek [mailto:john.havlicek@motorola.com]
Sent: Thursday, March 06, 2003 7:10 PM
To: sv-ac@eda.org
Subject: [sv-ac] negate rhs of implication
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:44:08 PST