Sciweavers

Share
CADE
2007
Springer

System for Automated Deduction (SAD): A Tool for Proof Verification

12 years 2 days ago
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).
Konstantin Verchinine, Alexander V. Lyaletski, And
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Konstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich
Comments (0)
books