@hackage twee2.6.1
An equational theorem prover
Installation
Dependencies (0)
- ansi-terminal >=0.9
- base <5
- containers
- jukebox >=0.5.9
- pretty
- split Show all…
Dependents (1)
@hackage/acme-everything
Package Flags
static
(off by default)
Build a static binary.
static-cxx
(off by default)
Build a binary which statically links against libstdc++.
parallel
(off by default)
Build a special parallel version of Twee.
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.