Naproche has been developed as a natural proof assistant since 2017, based on two older projects on proof checking with natural language input: the Evidence Algorithm project which was initiated by Victor Glushkov, leading eventually to the SAD system by Andrei Paskevich, and the original Naproche initiative with a stronger linguistic orientation.
Naproche 0 (2003–2015)
Evidence Algorithms and SAD (1960s–2008)
Naproche-SAD and the current Naproche (since 2017)
- Daniel Kühlwein, Marcos Cramer, Peter Koepke, and Bernhard Schröder (2007); The Naproche system.
- Konstantin Verchinine, Alexander Lyaletski, and Andrei Paskevich (2007); System for Automated Deduction (SAD): A tool for proof verification; in Automated Deduction – CADE‑21
- Andrei Paskevich (2007); The syntax and semantics of the ForTheL language; (technical report, translated from Andrei Paskevich’s thesis)