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

Improve this question
$\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$
    – Gerhard Paseman
    Commented Jul 26, 2011 at 4:09

1 Answer 1

Reset to default
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/

Improve this answer
$\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$
    – Gerhard Paseman
    Commented 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$
    – Neel Krishnaswami
    Commented 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
    Commented Aug 1, 2011 at 23:58

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .