Skip to content

nick8325/twee

Folders and files

NameName
Last commit message
Last commit date

Latest commit

12dd39a · Feb 14, 2025
Feb 14, 2025
Feb 2, 2024
Jul 2, 2021
Jul 19, 2021
Feb 14, 2025
Jul 19, 2021
Jul 22, 2015
Sep 15, 2022
Sep 16, 2017
Jun 13, 2020
Apr 15, 2015
Feb 23, 2023
Feb 14, 2025
Jun 9, 2024

Repository files navigation

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.

About

An equational theorem prover based on Knuth-Bendix completion

Resources

License

Stars

Watchers

Forks

Packages

No packages published