An interactive theorem prover based on lambda-tree syntax
OCaml Standard ML Ruby Emacs Lisp
Clone or download
Pull request Compare This branch is 11 commits ahead, 275 commits behind abella-prover:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
emacs
examples
src
.gitignore
.ocamlinit
COPYING
Makefile
PLUGINREADME
README
TACTREADME
_tags
myocamlbuild.ml

README

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