Twee, an equational theorem prover

Twee is a theorem prover for equational logic. It takes as input two sets of equations, the axioms and the conjectures, and tries to prove the conjectures from the axioms. See the installation page for how to get a copy; you may also want to look at the short manual.

The input problems should be written in TPTP format. Here is an example problem from group theory. We state that there is an associative binary function f with a right identity and right inverse:

fof(right_identity, axiom,
    ![X]: f(X, e) = X).
fof(right_inverse, axiom,
    ![X]: f(X, i(X)) = e).
fof(associativity, axiom,
    ![X, Y, Z]: f(X, f(Y, Z)) = f(f(X, Y), Z)).

Then we state the conjecture that the right inverse is also a left inverse:

fof(left_inverse, conjecture,
    ![X]: f(i(X),X) = e).

We can put this problem into a file, say group.p, and run twee group.p. Twee spits out the following proof; at the bottom it says Theorem which tells us the conjecture is true.

Goal 1 (left_inverse): f(i(X), X) = e.
Proof:
  f(i(X), X)
= { by axiom 1 (right_identity) }
  f(i(X), f(X, e))
= { by axiom 2 (right_inverse) }
  f(i(X), f(X, f(i(X), i(i(X)))))
= { by axiom 3 (associativity) }
  f(i(X), f(f(X, i(X)), i(i(X))))
= { by axiom 2 (right_inverse) }
  f(i(X), f(e, i(i(X))))
= { by axiom 3 (associativity) }
  f(f(i(X), e), i(i(X)))
= { by axiom 1 (right_identity) }
  f(i(X), i(i(X)))
= { by axiom 2 (right_inverse) }
  e

RESULT: Theorem (the conjecture is true).