Manual

The basic way to run twee is as follows:

twee name_of_problem.p

The problem must be in TPTP FOF or CNF or TFF format; you can find a worked example on the main page and lots of test problems here. Twee accepts any problem which after clausification consists only of unit equalities and Horn clauses. In practice this means that the input problem can freely use quantification, both universal and existential, in any combination.

The input file can have any number of conjectures. Twee will then solve each of them one at a time and report the final result. If the conjecture has an existential quantifier, twee will give you a witness, if possible.

The input file can use multiple types, although this slightly reduces the efficiency of the prover, and twee does not understand any built-in theories such as arithmetic. Currently, using types also litters the proof with terms of the form $to_foo(t), which are used internally to keep track of types. When reading the proof you should read $to_foo(t) as simply t.

Verbosity

The --quiet flag disables all progress output.

The --no-proof flag suppresses printing the final proof.

Different strategies

If twee fails to prove your conjecture, you might have more luck with a different strategy. Here are a couple to try:

• --no-flatten-goal - disable twee’s support for goal-directed search
• --lhs-weight 1 - adjust the scoring of critical pairs

Infix operators

As an extension to TPTP syntax, twee supports infix operators. For example, you can write

cnf(commutativity, axiom, X+Y = Y+X).

which is equivalent to

cnf(commutativity, axiom, '+'(X,Y) = '+'(Y, X)).

You can find a longer example here.

Operators may not include characters such as & and | that are used in TPTP connectives. This rules out quite a lot of useful characters. However, twee supports Unicode input, so you can often find a suitable Unicode character to use (see here for the more common ones).

TPTP support

Twee respects the TPTP environment variable for finding problems and axioms. For example, twee BOO067-1.p will find $TPTP/Problems/BOO/BOO067-1.p. You can add extra search directories using the --root option, which takes a comma-separated list of directories and can be passed multiple times.

The --tstp flag causes twee to print SZS status lines in the official syntax. The flags --tstp --formal-proof cause it to print a CNFRefutation in the formal TSTP format when it proves the conjecture.

Resource limits

Twee has several options for stopping the proof search after a certain resource bound is reached.

--max-term-size n discards any rewrite rule whose left-hand side is longer than n symbols.

--max-cps n stops twee after it has considered n critical pairs.

--max-cp-depth n discards any critical pair whose “distance” to the axioms is more than n. For example, --max-cp-depth 1 only generates critical pairs directly from the axioms, --max-cp-depth 2 generates critical pairs from those critical pairs, and so on.

If any of these modes are specified, twee will print GaveUp rather than Satisfiable when it runs out of critical pairs to try.

Expert options

There are also several options for tweaking heuristics and so on. You can get a brief description of them with twee --expert-help. Apart from that, they remain undocumented for now :)