search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
90 stars 18 forks source link
interactive-theorem-proving lambda-calculus meta-theory

readme

Quick Start

The easiest way to install Abella is using OPAM (version 2.1+).

  1. Go to the topmost directory of the clone of this repository, i.e., the location of this very README.md file.
  2. Run: opam pin abella . (note the final period)
  3. When prompted by OPAM, say yes to install Abella.
  4. Whenever you do a git pull, also do: opam reinstall abella.

To uninstall Abella using OPAM, do:

  1. Run: opam remove abella.
  2. Then run: opam unpin abella.

More Information

Use the following walkthrough for an introduction to using Abella:

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

More information on Abella is available at

https://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