3
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ 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 $\endgroup$ Jul 26, 2011 at 4:09

1 Answer 1

5
$\begingroup$

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/

$\endgroup$
3
  • $\begingroup$ 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 $\endgroup$ Jul 26, 2011 at 7:48
  • $\begingroup$ 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. $\endgroup$ Jul 26, 2011 at 9:33
  • $\begingroup$ 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? $\endgroup$
    – Rex Butler
    Aug 1, 2011 at 23:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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