Subject: Re: [sv-ac] negate rhs of implication
From: Joseph Lu (Juin-Yeu.Lu@sun.com)
Date: Thu Mar 06 2003 - 10:05:04 PST
I would third John's proposal.
Regards,
--Joseph
>Date: Thu, 6 Mar 2003 11:10:27 -0600 (CST)
>To: sv-ac@eda.org
>Subject: [sv-ac] negate rhs of implication
>From: John Havlicek <john.havlicek@motorola.com>
>
>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 - 10:09:53 PST