Propositional logic

I am now teaching Fitch-style propositional logic proofs with and, or and not. I had some fun last night and wrote a fun little proof generator in perl (or, perhaps more precisely, modperl). This morning I'm going to teach the students the simple brute-force method that the code uses (basically, just go through all the possible combinations of truth values), which I assume is pretty standard. While the method tends to generate proofs that are unduly long, I think there is a value in having a method that is guaranteed to work even if one is suffering from prover's block. Besides, the algorithm makes it intuitively clear why truth-table completeness holds for propositional logic.

I was going to post a link to a web service that runs the prover. But I then thought that a student at another institution might cheat with it (even though the proofs generated have a somewhat identifiable look, and there is always the risk of bugs in my code), and so I didn't do it. If you're a faculty member, or are someone I know and trust, and are curious to see the code run, email me and I might send you a private link. Of course, someone determined on cheating can use the source code that I posted, but I bet there is other source code posted online that does things like that.

[The code in the link continues to evolve. For instance, it now does some easy simplifications optionally. - Note added later]