Previews and demos

Contents

Video intro

Reasoning forward

Here is the classic proof that the Greek philosopher Socrates is mortal, starting from true statements. They are already asserted to be true — without proof. The descriptions for steps 1 and 2 show that they have been asserted.

In step 1, x is a variable, and the proof will substitute the constant Socrates for x there.

Reasoning backward

In Prooftoys, reasoning “backward” means reasoning based on a stated goal. The proof starts with a statement, known to be true, that is like the goal statement, but with some unwanted assumptions. The process eliminates excess assumptions until what remains is the actual goal statement.

The demo is a step-by-step walkthrough demo of of the Country Music Theorem.

Prooftoys generates an initial statement from a goal statement by including the desired conclusion as an assumption. This is guaranteed to make it true, and Prooftoys proves it for you behind the scenes.