StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>Note: I flagged this to be moved to the Computer Science site because they are much more on top of ATP over there.</p> <p>It would be nice if you could include what you have looked at and why it does not help you. Then we can figure out what might be better for you. Also, if you have to write a program, then knowing what languages you know will help. Most of what I do with this is done in a functional language such as OCaml or F#, or a logic language such as Prolog or Mercury.</p> <p>Have you seen "<a href="http://www.cl.cam.ac.uk/~jrh13/atp/" rel="nofollow">Handbook of Practical Logic and Automated Reasoning</a>" <a href="http://www.worldcat.org/oclc/244767230" rel="nofollow">(WorldCat)</a> by John Harrison. I included the <a href="http://www.worldcat.org/oclc/244767230" rel="nofollow">(WorldCat)</a> link so you can find the book in a local library as opposed to waiting to buy it which will eat up most of your time.</p> <p>If you look you will find the <a href="http://www.cl.cam.ac.uk/~jrh13/atp/" rel="nofollow">OCaml</a> code at the bottom of the page, and F# <a href="https://github.com/jack-pappas/fsharp-logic-examples/" rel="nofollow">here</a> and Haskell <a href="http://code.google.com/p/haskellatp/issues/searchtips" rel="nofollow">here</a>.</p> <p>In case you haven't see the <a href="http://en.wikipedia.org/wiki/Automated_theorem_proving" rel="nofollow">ATP</a> or <a href="http://en.wikipedia.org/wiki/Proof_assistant" rel="nofollow">Proof Assistant</a> at Wikipedia, you might get a lead to some code and papers.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload