[Date Index] [Thread Index] [Author Index]

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)