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
References in zbMATH (referenced in 12 articles )
Showing results 1 to 12 of 12.
- Lyaletski, Alexander: Evidence algorithm and inference search in first-order logics (2015)
- Geuvers, Herman; Nederpelt, Rob: N. G. de Bruijn’s contribution to the formalization of mathematics (2013)
- Letichevsky, A.A.; Lyaletski, A.V.; Morokhovets, M.K.: Glushkov’s evidence algorithm (2013)
- Cramer, Marcos; Koepke, Peter; Schröder, Bernhard: Parsing and disambiguation of symbolic mathematics in the Naproche system (2011)
- Autexier, Serge; Dietrich, Dominik: A tactic language for declarative proofs (2010)
- Cramer, Marcos; Koepke, Peter; Kühlwein, Daniel; Schröder, Bernhard: Premise selection in the Naproche system (2010)
- Lyaletski, Alexander; Verchinine, Konstantin: Evidence algorithm and system for automated deduction: a retrospective view. (In honor of 40 years of the EA announcement) (2010)
- Geuvers, H.: Proof assistants: history, ideas and future (2009)
- Verchinine, Konstantin; Lyaletski, Alexander; Paskevich, Andrei; Anisimov, Anatoly: On correctness of mathematical texts from a logical and practical point of view (2008)
- Verchinine, Konstantin; Lyaletski, Alexander; Paskevich, Andrei: System for automated deduction (SAD): A tool for proof verification (2007)
- Lyaletski, Alexander; Paskevich, Andrey; Verchinine, Konstantin: SAD as a mathematical assistant -- how should we go from here to there? (2006)
- Lyaletski, Alexander; Paskevich, Andrey; Verchinine, Konstantin: Theorem proving and proof verification in the system SAD (2004)