zbMATH — the first resource for mathematics

System for automated deduction (SAD): A tool for proof verification. (English) Zbl 1213.68576
Pfenning, Frank (ed.), Automated deduction – CADE-21. 21st international conference on automated deduction, Bremen, Germany, July 17–20, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73594-6/pbk). Lecture Notes in Computer Science 4603. Lecture Notes in Artificial Intelligence, 398-403 (2007).
Summary: 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).
For the entire collection see [Zbl 1122.68008].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI