SNARK

SNARK (SRI's New Automated Reasoning Kit) is described as "an automated theorem-proving program" being developed in Common Lisp. Its principal inference rules are resolution and paramodulation. SNARK's style of theorem proving is similar to Otter's."

SNARK is available here under the Mozilla Public License.

Application Theorem Provers

CLiki pages can be edited by anyone at any time. Imagine a fearsomely comprehensive disclaimer of liability. Now fear, comprehensively