Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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|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
add comment

1 Answer 1

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.

[1] http://combination.cs.uiowa.edu/smtlib/

share|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? –  Skolem Aug 1 '11 at 23:58
add comment

Your Answer

 
discard

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.