@hackage twee2.0

An equational theorem prover

  • Installation

  • Dependencies (7)

  • 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++.

      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, a prover for equational problems.

To install, run cabal install.

Afterwards, invoke as 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 types and quantifiers.

Twee is experimental software, use at your own risk!