Re: Logical expressions in Mathematica
- To: mathgroup at yoda.ncsa.uiuc.edu
- Subject: Re: Logical expressions in Mathematica
- From: gabriel at athens.ees.anl.gov (John Gabriel)
- Date: Tue, 23 Oct 90 11:13:54 CDT
There are a number of traps in simplification of large logical expressions by any symbolic algebra package. Of these, the biggest is that the "obvious" elementary operators do not give rise to a Church-Rosser set of reduction rules. I think I'm right in saying that AND and XOR give Church Rosser rewriting rules if used alone - i.e. first turn everything into AND and XOR and only then begin to simplify. The rewriting algorithms in Boyer & Moore's theorem prover are the outcome of many years of work, and perhaps you should mail a question to boyer at cli.com before venturing too far into the jungle on your own. For more information on rewriting, Church-Rosser, and canonical forms - if a reduction is not canonical then it's not very useful - see Alan Bundy's book on Computer Modelling of Mathematics or a similar title, mine's at home so I can't quote chapter and verse. Also, you have a Net doppelganger wos at mcs.anl.gov. People who have worked with him have done a good deal on this, and he could probably point you at somebody. Brian Smith, now at the Dept. of CS at U. of New Mexico Albuquerque is also a good source of advice. John Gabriel (gabriel at ees.anl.gov)