Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. - Ulrich Kühler; Claus-Peter Wirth (RTA, 1997)

A tactic-based inductive theorem prover for data types with partial operations. - Ulrich Kühler (Infix, 2000)

How to Prove Inductive Theorems? QUODLIBET! - Jürgen Avenhaus; Ulrich Kühler; Tobias Schmidt-Samoa; Claus-Peter Wirth (CADE, 2003)