@hackage / twee

An equational theorem prover

Latest2.6.1

About

Metadata

  • Last updated , by NickSmallbone
  • License BSD-3-Clause

  • Maintained by: nicsma@chalmers.se

  • Lottery factor: 1

Links

Installation

Package Flags

Use the -f option with cabal commands to enable 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.

Readme

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.