Date: Mon, 19 Feb 1996 12:48:18 -0600 (CST)
From: Daniel Lichtblau
To: rusin@vesuvius.math.niu.edu (Dave Rusin)
Subject: Re: Verifying Tautologys?
In sci.math.symbolic article <4gaa5j$c89@muir.math.niu.edu> you
wrote:
> In article <312449D1.63D5@bham.ac.uk>,
> A.Situnayake wrote:
> >Hi' I have just started a Computer Science course and am currently
> >looking at Boolean Algebra, could you tell me how to verify
Tautology's
> >using boolean algebra ( I can manage it using Truth Tables :-) )
> >e.g (p->q)^(q->r)->(p->r)
>
> In article <4g7lj4$hm3@dickerdack.sci.kun.nl>,
> Mark van Hoeij wrote:
> >There is also a different method (idea of H. Derksen), as follows:
> >These boolean expressions can be written as elements of the ring:
> >
> > F2[p,q,r]/(p^2-p, q^2-q, r^2-r)
> >
> >where 1=true and 0=false (you can switch this).
> ...
> >In principle this approach is not more efficient than just trying
all
> >true/false combinations for all variables p,q,r, because the
dimension as
> >a F2 vector space of this ring is 2^(number of variables).
>
> Maybe in worst-case situations it is that slow, but this seems like
a
> dandy method, coupled with the use of Groebner bases. The question
is
> whether or not a given polynomial belongs to the ideal of
> F2[p,q,r] generated by (p^2-p,q^2-q,r^2-r). This can be determined
> by use of the division algorithm for polynomial rings. You never
need
> to plug in different values for p, q, and r. Am I missing
something?
> This seems quite efficient.
>
> dave
>
You do not even need the division algorithm, in this special case.
You can simply remove all exponents (in Mathematica, this would by
via
expr /. a_^b_Integer->a
which you can translate to your language-of-choice). For efficiency,
interleave expansion of pairs of factors with this replacement. This
is something of a polynomial-product-modulo-ideal operation. You have
a tautology iff the result is one.
As noted, the result may well have size up to 2^(#variables), hence
this is exponential.
Daniel Lichtblau
Wolfram Research, Inc.
==============================================================================
Date: Mon, 19 Feb 96 13:10:47 CST
From: rusin (Dave Rusin)
To: danl@wolfram.com
Subject: Re: Verifying Tautologys?
Oh I get it: the exponential search of the truth-table space is exchanged for
the possibly exponential cost of expanding the expression, after which
verification is trivial. Sorry to be dense; some of us think of "simpifying"
an expression as more or less automatic -- the thing to do before the
real work starts. I tend to forget the cost of that expansion.
thanks
dave
==============================================================================
Date: Mon, 19 Feb 1996 13:33:00 -0600 (CST)
From: Daniel Lichtblau
To: rusin@math.niu.edu (Dave Rusin)
Subject: Re: Verifying Tautologys?
> exponential search of the truth-table space is exchanged for
>the possibly exponential cost of expanding the expression
True. Though I think the former is typically worse than the latter.
Danl
==============================================================================