views:

271

answers:

4

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.

+4  A: 

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.

Charlie Martin
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
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
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
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
+1  A: 

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.

Not Sure
Yup I would go with Maple over Mathematica any day
Ankur
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
A: 

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).

starblue
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
A: 

An old and unmaintained system is 'Ontic':

http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html

Rainer Joswig