Version 2.0 (April 1995)

In this version we use substitution tree indexing for (forward) reduction and subsumption. This makes the system substantially faster on larger examples.

We have made clausal rewriting more powerful such that more theories can be finitely saturated

We support equivalences between (nonequational) atoms $A, B$, written $A\mathrel{\mbox{{\tt ==}}}B$. Equivalences may also occur on literal positions in clauses, cf. in command.

Imprint | Data Protection