System for automated deduction (SAD): A tool for proof verification. In this paper a proof assistant called SAD is presented. SAD deals with mathematical texts that are formalized in the ForTheL language (a brief description of which is also given) and checks their correctness. We give a short description of SAD and a series of examples that show what can be done with it. Note that abstract notion of correctness on which the implementation is based, can be formalized with the help of a calculus (not presented here).

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element