Computer-Assisted Proofs in Analysis and Programming in Logic: A case Study. - Hans Koch; Alain Schenkel; Peter Wittwer (SIAM Rev., 1996)