Deduce: An Educational Functional Program Proof Checker

2025-03-24
Deduce: An Educational Functional Program Proof Checker

Deduce is an automated proof checker designed for education, helping students learn to prove the correctness of functional programs, deepen their understanding of logic, and improve their mathematical proof-writing skills. It's aimed at students with basic programming skills (Java, Python, or C++) and some exposure to logic from a discrete mathematics course. Deduce provides resources ranging from installation and code writing to a reference manual and cheat sheet, with an example proof of a linear search algorithm to illustrate its use.