Take the 2-minute tour ×

I'm looking for a tool (GUI preferred but CLI would work) that allows me to input math expressions and then perform manipulations of them but restricts me to only mathematically valid operations. Also, the tool must be able to save a session and later prove that the given set of saved operations is valid.

Note: I am Not looking for a system to generate proofs, only that check that the steps I manually specify are valid.

I have used ACL2 for similar operations and it does well for some cases but it is very hard to use for everything else.

This little project is my motivation. It is a D template type that allows for equation solving. Given this equation:

(A * B) = C + D / F;

Any one of the symbols can be set as unknown and evaluating that expression will result an an assignment to that variable. It works by building expression trees into the type and then using rewrite rules to convert it to something that can be eventuated for the unknown type.

What I need is some way to validate the rewrite rule. They can be validated by testing the assertion that given some relation is true, another one is also.

share|improve this question
What kind of maths? Abstract algebra, linear algebra, functional analysis...? –  Pontus Gagge Apr 10 '09 at 19:48
@BCS, I've got to admit the source code etc didn't make your intention just pellucidly obvious. Do you suppose you could summarize a little bit what your goals are? –  Charlie Martin Apr 10 '09 at 23:09
@Charlie :b, you have a point. –  BCS Apr 11 '09 at 17:33
Okay, I think you may well want to look more at PVS. I've never used it, thought, just read some of the docs. –  Charlie Martin Apr 12 '09 at 7:09
add comment

5 Answers

Several American proof assistants were mentioned already (usually with LISP syntax), so here is a Europe-centric list to complement that:

All of them are notorious for TTY interfaces, but Coq and Isabelle provide good support for the Proof General / Emacs interface. Moreover, Coq comes with CoqIDE, which is based on OCaml/GTK an the on-board text widget. Recent Isabelle includes the Isabelle/jEdit Prover IDE, which is based on jEdit and augmented by semantic markup provided by the prover in real-time as the user types.

share|improve this answer
Some people use CoqIDE with Coq as well. –  toyvo Mar 1 '13 at 12:49
I've updated my answer accordingly, to include CoqIDE. –  Makarius Mar 8 '13 at 10:48
add comment

ACL2 is notorious -- we used to say it was an expert system, and so could only be used by experts, who had to learn from Warren Hunt, J Moore, or Bob Boyer. The thing you need to do in ACL2 is really really understand how the proof system itself works; then you can "hint" it in directions that reduce the search space.

There are several other systems that can help with this kind of thing, though, depending on what you're trying to do.

If you want to work with continuous math or number theory, the ideal is Mathematica. Problem is you can buy a used car for the same amount of money (unless you can qualify for an academic license, a far better deal.)

Something similar, and free, is Open Maxima, which is an extension of Macsyma. That page also points to several others like Axiom, that I've got no experience with.

For mathematical logic operations, there's PVS from SRI. They've got some other cool stuff like model-checking in the same framework.

share|improve this answer
Unless ACL2 just gives up after some set time I never ran into search space size problems. It just failed to find proofs without a lot of lemmas. –  BCS Apr 10 '09 at 19:58
Sure, but that's still a problem of limiting the search space; it's just smart enough to not CONS too much for memory. The lemmae, along with organizing your clauses to get the optimal search, are the "hints" I'm thinking about. –  Charlie Martin Apr 10 '09 at 21:06
I've wished for an ACL2 UI for feeding it exactly what to do and that dumps ACL2 code with hints that instruct the proof engine to do exactly the right thing at each step. YMMV, but I've never found getting ACL2 to do stuff for me to be faster than doing it my self. More accurate, yes, faster no. –  BCS Apr 11 '09 at 23:43
Who could wish or a better UI than an EMACS buffer? But seriously, ACL2 isn't meant to be easier; Bob and J just feel a machine-checked proof is more trustworthy in a strict sense. For easier go for Mathematica. –  Charlie Martin Apr 12 '09 at 7:07
add comment

There's ongoing research in this area, it's called "Theorem proving in computer algebra".

People are trying to merge the ease of use and power of computer algebra systems like Mathematica, Maple, ... with the logical rigor of proof systems. The problems are:

  • Computer algebra systems are not rigorous. They tend to forget side conditions such as that a divisor must not be 0.

  • The proof systems are hard and tedious to use (as you have discovered).

share|improve this answer
As it happens, the n/0 issue is not a problem for my given cases as the result of ignoring that is exactly what I want to happen. –  BCS Apr 11 '09 at 21:34
add comment

In addition to what Charlie Martin's links, you may also want to check out Maple. My experience with such software is about 5 years old, but I recall at the time finding Maple to be much more intuitive than Mathematica.

share|improve this answer
Yup I would go with Maple over Mathematica any day –  Ankur Apr 11 '09 at 17:43
As per my edit, I'm not looking for a system to do the work for me (as IIRC maple is) but a system to just check my work. –  BCS Apr 11 '09 at 23:32
add comment

Your Answer


