The AFFIRM theorem prover: proof forests and management of large proofs. The AFFIRM theorem prover is an interative, natural-deduction system centered around abstract data types. Since long proofs are often required to verity algorithms, we describe a model (called the ”proof forest”) which helps the user to visualize and manage the potentially large number of theorems and subgoals that can arise.