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 (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).

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Konstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich
• Keywords: Abstract Notion, Automated Reasoning, CADE 2007, Mathematical Texts, Proof Assistant