Anlauff M., Jähnichen S., Simons M. (1996) A Support System for Formal Mathematical Reasoning In: Naftalin M., Denvir T., Bertran M. (eds) FME'94: Industrial Benefits of Formal Methods (Lecture notes of Computer Science, Vol. 873, pp. 421-440). Berlin: Springer Verlag.
© Springer Verlag

Abstract Requirements for tools which support the creation and the intelligible presentation of formal deductions are investigated. They are contrasted with requirements which emphasize the interactive construction of correct proofs. As an example, the design and the implementation of a set of support tools for Deva is described. Deva is a typed functional language and has been used in a number of case-studies on formal program development. The use of this toolset is illustrated by impressions of a working session.