MathGroup Archive 1990

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

Search the Archive

Re: Logical expressions in Mathematica

  • To: mathgroup at
  • Subject: Re: Logical expressions in Mathematica
  • From: gabriel at (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 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 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

  • Prev by Date: Re: math coprocessors
  • Next by Date: Re: math coprocessors
  • Previous by thread: Logical expressions in Mathematica
  • Next by thread: Re: Ignorance