Mathematics in Prover

[RalphW]

I'm just getting started using Prover and trying to do some of the things I used to do in Otter. I can't seem to figure out how to do the basic math analogs of $SUM, $MOD, $DIV,etc in Prover. Was this not implemented or is there something special I should be doing to get Prover to do a math evaluation. By the way, I am using the GUI version of Prover. Thanks for any help.

[mccune]

The most recent version of Prover9 has a "production mode" that does state-space searches with evaluable operations (built-in arithmetic, etc.). Unfortuately, the GUI uses an older version of Prover9 which does not have those capabilities.

The current Prover9 manual http://www.cs.unm.edu/~mccune/prover9/manual/2009-02A/ describes the new production mode and has several examples.

Bill