MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Is there an software package aimed at verfication of simple equational proofs?

I am hoping to avoid the usual overhead involved with First Order Logic or Higher Order Logic verification systems.

[Apologies for the 'software question', but formal verification usually involves this. :) References to papers that might point me in the right direction would of course be appreciated.]

share|cite|improve this question
The best I can come up with are search phrases: term rewriting systems, unification, and Stanley Burris. I don't know if Prof. Burris is still active, but he is the first person I would ask about your question. Gerhard "Ask Me About System Design" Paseman, 2011.07.25 – Gerhard Paseman Jul 26 '11 at 4:09
up vote 5 down vote accepted

SMT (Satisfaction Modulo Theories) solving is pretty much the go-to technology for this these days, and works shockingly well in practice, often even on undecidable theories. Here are links to a few such projects (though there are many, many more implementations).

The SMT-LIB webpage[1] is a central library organizing the efforts of many of these efforts as well as containing a specification of a common language for SMT solvers to take as input.


share|cite|improve this answer
Thanks for this. Do you know if Stanley Burris is involved with any of these? Gerhard "Ask Me About System Design" Paseman, 2011.07.26 – Gerhard Paseman Jul 26 '11 at 7:48
Looking at his webpage, he certainly could be, but I don't actually know -- this kind of theorem proving is (a) a huge and extremely active area, and (b) just outside my own expertise. SMT is a very applied field, and as a result they are happy to use any mathematics from any area to make their programs run faster. – Neel Krishnaswami Jul 26 '11 at 9:33
I'll take a look at these, thanks. Still, these support full first order logic, not just equational logic. Is FOL the natural level of generality here? – Rex Butler Aug 1 '11 at 23:58

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.