A tiny proof checker in Prolog
The Prolog code for this post is available on GitHub . I am crazy enough to teach Hoare logic (axiomatic semantics) in the first course for our CS students. For instance, consider the following program (in some simple imperative language), which is supposed to compute quotient q and remainder r according to Euclidian division for operands x and y : q = 0; r = x; while (r >= y) { r = r - y; q = q + 1; } Given natural numbers x and y , the postcondition of the program is this: x == q*y + r && q >= 0 && r>=0 && r < y The precondition is this is: x >= 0 && y > 0 We are supposed to prove the "triple" consisting of precondition, program, and postcondition. Let's face it, verification according to Hoare logic is not easily understood by beginners. Many of my students aren't mathematically / logically fit, when they enter the curriculum. So it is a pain in the neck for them to listen and for ...