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 ==============================================================================