twee-lib

An equational theorem prover based on Knuth-Bendix completion


Keywords
library, theorem-provers, Propose Tags , , Index, Quick Jump, Data.Label, Twee, Twee.Base, Twee.CP, Twee.Constraints, Twee.Equation, Twee.Index, Twee.Join, Twee.KBO, Twee.Pretty, Twee.Profile, Twee.Proof, Twee.Rule, Twee.Rule.Index, Twee.Task, Twee.Term, Twee.Utils, More info, twee-lib-2.4.2.tar.gz, browse, Package description, package maintainers, edit package information
License
BSD-3-Clause
Install
cabal install twee-lib-2.4.2

Documentation

This is twee, an equational theorem prover.

The version in this git repository is likely to be unstable! To install the latest stable version, run:

cabal install twee

If you have LLVM installed, you can get a slightly faster version by running:

cabal install twee -fllvm

If you really want the latest unstable version, run cabal install src/ . in this repository.

Afterwards, run twee nameofproblem.p. The problem should be in TPTP format (http://www.tptp.org). You can find a few examples in the tests directory. All axioms and conjectures must be equations, but you can freely use quantifiers. If it succeeds in proving your problem, twee will print a human-readable proof.

For the official manual, see http://nick8325.github.io/twee.