most recent 30 from http://mathoverflow.net 2013-05-19T08:15:52Z http://mathoverflow.net/feeds/question/71265 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/71265/formal-verification-of-simple-equational-proofs-as-in-universal-algebra Skolem 2011-07-25T22:10:48Z 2011-07-26T07:03:37Z

<p>Is there an software package aimed at verfication of simple equational proofs? </p> <p>I am hoping to avoid the usual overhead involved with First Order Logic or Higher Order Logic verification systems.</p> <p>[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.]</p>

http://mathoverflow.net/questions/71265/formal-verification-of-simple-equational-proofs-as-in-universal-algebra/71294#71294 Neel Krishnaswami 2011-07-26T07:03:37Z 2011-07-26T07:03:37Z

<p>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). </p> <ul> <li>CVC3: <a href="http://cs.nyu.edu/acsys/cvc3/" rel="nofollow">http://cs.nyu.edu/acsys/cvc3/</a> </li> <li>OpenSMT: <a href="http://verify.inf.unisi.ch/opensmt" rel="nofollow">http://verify.inf.unisi.ch/opensmt</a></li> <li>Z3: <a href="http://research.microsoft.com/en-us/um/redmond/projects/z3/" rel="nofollow">http://research.microsoft.com/en-us/um/redmond/projects/z3/</a></li> <li>STP: <a href="http://sites.google.com/site/stpfastprover/" rel="nofollow">http://sites.google.com/site/stpfastprover/</a></li> </ul> <p>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.</p> <p>[1] <a href="http://combination.cs.uiowa.edu/smtlib/" rel="nofollow">http://combination.cs.uiowa.edu/smtlib/</a></p>