9

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.

Makarius
  • 2,165
  • 18
  • 20
BCS
  • 75,627
  • 68
  • 187
  • 294

6 Answers6

7

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.

Makarius
  • 2,165
  • 18
  • 20
6

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
  • 110,348
  • 25
  • 193
  • 263
  • 1
    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 07:07
2

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
  • 55,348
  • 14
  • 97
  • 151
  • 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
1

The lean prover is interactive through a JS gui.

Michael Barton
  • 8,868
  • 9
  • 35
  • 43
  • It also has an Emacs mode. [Here](http://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf) are slides describing `lean-mode`. – Anton Trunov Oct 29 '16 at 12:34
1

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
  • 5,873
  • 3
  • 23
  • 29
  • Yup I would go with Maple over Mathematica any day – Ankur Apr 11 '09 at 17:43
  • 1
    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
0

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
  • 136,269
  • 10
  • 221
  • 346