INKA Inductive Theorem Prover
First-order theorem prover with induction based on the explicit induction paradigm. It is based on a full first-order calculus, a special variant of the resolution calculus with paramodulation.