/abella

An interactive theorem prover based on lambda-tree syntax

Primary LanguageOCamlGNU General Public License v3.0GPL-3.0

Quick Start

Compile Abella by running "make" from the root directory. This will create the binary "abella" (on Unix-like systems, including Mac OS X), or "abella.exe" (on Windows). This binary can be freely copied anywhere.

Use the following walkthrough for an introduction to using Abella:

http://abella-prover.org/walkthrough.html

More Information

More information on Abella is available at

http://abella-prover.org/

Bugs, Feature Requests, and Issues

Please report all bugs, feature requests, and issues on the GitHub issue tracker for Abella, available from:

https://github.com/abella-prover/abella/issues

Discussion of Abella and its uses happens on this mailing list.

http://groups.google.com/group/abella-theorem-prover