A proof checker meant for education
Teaching correctness proofs of functional programs to students.
What is Deduce?
Deduce is an automated proof checker meant for use in education to help students:
- Ease their way into proving the correctness of programs.
- Deepening their understanding of logic.
- Improve their ability to write mathematical proofs.
Who can use Deduce?
The intended audience is students with (roughly) the following background knowledge and skills:
- Basic programming skills in a mainstream language such as Java, Python, or C++
- Some exposure to logic, as one would learn in a course on Discrete Mathematics
Get Started
Get started by installing the necessary prerequisites and downloading the Deduce source code.
You can also find handy information on setting up your Deduce workspace.
Write Deduce Code
Go through a series of examples to familiarize yourself with Deduce functional programming.
Check your understanding with exercises to test your knowledge of the language.
Prove Your Programs
Follow a detailed tutorial to learn how to write logical proofs using Deduce effectively.
Explore all of the features of the Deduce proof language in this comprehensive guide.
Need Help?
The Deduce Reference manual provides an alphabetical list of all the features in Deduce.
The Cheat Sheet gives some advice regarding proof strategy and which Deduce keyword to use next in a proof.
Example Proof
As a taster for what it looks like to write programs and proofs in Deduce, the following is an implementation of the Linear Search algorithm and a proof that item y does not occur in the list xs at a position before the index returned by search(xs, y)
Credits
This open-source software is brought to you by the volunteer work of the following people.
- Matei Cloteaux
- Shulin Gonsalves
- Calvin Josenhans
- Jeremy Siek