@hackage twee-lib2.1

An equational theorem prover

  • Installation

  • Dependencies (8)

  • Dependents (2)

    @hackage/quickspec, @hackage/twee

    • Package Flags

      static
       (off by default)

      Build a static binary.

      static-cxx
       (off by default)

      Build a binary which statically links against libstdc++.

      llvm
       (off by default)

      Build using LLVM backend for faster code.

      bounds-checks
       (off by default)

      Use bounds checks for all array operations.

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 in this repository, and then in the executable subdirectory. You will most likely need the latest git version of Jukebox, from https://github.com/nick8325/jukebox, too - and things may break from time to time.

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.